a3/code/Gast/testable.icl

   1 implementation module testable
   2
   3 /*
   4         GAST: A Generic Automatic Software Test-system
   5
   6         testable: the test algorithm for logical properties
   7
   8         Pieter Koopman, 2002-2010
   9         Radboud Universty, Nijmegen
  10         The Netherlands
  11         pieter@cs.ru.nl
  12 */
  13
  14 import StdEnv, MersenneTwister, genLibTest /*, StdTime*/ , gen
  15
  16 derive gLess Result
  17 instance == Result where (==) x y = x===y
  18
  19 newAdmin :: Admin
  20 newAdmin = {res=Undef, labels=[], args=[], name=[]}
  21
  22 class TestArg a | genShow{|*|}, ggen{|*|} a
  23
  24 //class Testable a where evaluate :: a RandomStream Admin -> [Admin]
  25
  26 //instance Testable Bool where evaluate b rs result = [{result & res = if b OK CE, args = reverse result.args}]
  27 instance Testable Bool where evaluate b rs result=:{args} = [{result & args = reverse args, res = if b OK CE}]
  28
  29 instance Testable Result where evaluate r rs result=:{args} = [{result & args = reverse args, res = r}]
  30
  31 instance Testable Property
  32 where evaluate (Prop p) rs result = p rs result
  33
  34 instance Testable (a->b) | Testable b & TestArg a
  35 where evaluate f rs admin
  36                 # (rs,rs2) = split rs
  37                 = forAll f (generateAll rs) rs2 admin
  38
  39 instance Testable [a] | Testable a
  40 where
  41 //      evaluate []   rs admin=:{args} = [{admin & args = reverse args, res = OK}]
  42         evaluate list rs admin = diagonal [ evaluate x (genRandInt seed) admin \\ x<-list & seed<-rs ]
  43 //      evaluate list rs admin = flatten [ evaluate x (genRandInt seed) admin \\ x<-list & seed<-rs ]
  44
  45 :: Property = Prop (RandomStream Admin -> [Admin])
  46
  47 prop :: a -> Property | Testable a
  48 prop p = Prop (evaluate p)
  49
  50 forAll :: !(a->b) ![a] RandomStream !Admin -> [Admin] | Testable b & TestArg a
  51 forAll f []   rs r=:{args} = [{r & args = reverse args, res = OK}]                              // to handle empty sets of values
  52 forAll f list rs r = diagonal [apply f a (genRandInt seed) r \\ a<-list & seed<-rs ]
  53
  54 apply :: !(a->b) a RandomStream !Admin -> [Admin] | Testable b & TestArg a
  55 apply f a rs r = evaluate (f a) rs {r & args = [show1 a:r.args]}
  56
  57 diagonal :: [[a]] -> [a]
  58 diagonal list = f 1 2 list []
  59 where
  60         f n m [] [] = []
  61         f 0 m xs ys = f m (m+1) (rev ys xs) []
  62         f n m [] ys = f m (m+1) (rev ys []) []
  63         f n m [[x:r]:xs] ys = [x: f (n-1) m xs [r:ys]]
  64         f n m [[]:xs] ys = f (n-1) m xs ys
  65
  66         rev []    accu = accu
  67         rev [x:r] accu = rev r [x:accu]
  68
  69 generateAll :: !RandomStream -> [a] | ggen{|*|} a
  70 generateAll rnd = ggen{|*|} 2 rnd
  71
  72 derive gEq Result
  73 derive bimap [], (,), (,,), (,,,), (,,,,), (,,,,,)
  74
  75 //--- Random ---//
  76
  77 split :: !RandomStream -> (RandomStream,RandomStream)
  78 split [r,s:rnd]
  79         # seed = r*s
  80         | seed==0
  81                 = split rnd
  82                 = (rnd, genRandInt seed)
  83
  84 (>>=) infix 0 :: (a -> (b,a)) (b a -> d) -> a -> d
  85 (>>=) f g = \st = let (r,st1) = f st in g r st1
  86
  87 result :: b -> a -> (b,a)
  88 result b = \a = (b,a)
  89
  90 //--- testing ---//
  91
  92 :: Config
  93  =      { maxTests      :: Int
  94         , maxArgs       :: Int
  95         , every         :: Int Admin [String] -> [String]
  96         , fails         :: Int
  97         , randoms       :: [Int]
  98         }
  99
 100 verboseConfig
 101  =      { maxTests      = NrOfTest
 102         , maxArgs       = 2*NrOfTest
 103         , every         = verboseEvery
 104         , fails         = 1
 105         , randoms       = aStream
 106         }
 107 verboseEvery n r c = [blank,toString n,":":showArgs r.args c]
 108
 109 traceConfig
 110  =      { maxTests      = 100
 111         , maxArgs       = 1000
 112         , every         = traceEvery
 113         , fails         = 1
 114         , randoms       = aStream
 115         }
 116 traceEvery n r c = ["\n",toString n,":":showArgs r.args c]
 117
 118 blank :: String
 119 blank =: { createArray len ' ' & [0] = '\r', [len-1] = '\r' } where len = 81
 120
 121 countConfig
 122  =      { maxTests      = 100
 123         , maxArgs       = 10000
 124         , every         = countEvery
 125         , fails         = 1
 126         , randoms       = aStream
 127         }
 128 countEvery n r c = [toString n,"\r": c]
 129
 130 quietConfig
 131  =      { maxTests      = 1000
 132         , maxArgs       = 10000
 133         , every         = animate2 // \n r c = if (n rem 10000 == 0) [".":c] c
 134         , fails         = 1
 135         , randoms       = aStream
 136         }
 137
 138 animate n r c
 139         | n rem Steps == 0
 140                 = case (n/Steps) rem 4 of
 141                         0 = ["\r|":c]
 142                         1 = ["\r/":c]
 143                         2 = ["\r-":c]
 144                         3 = ["\r\\":c]
 145                           = ["??":c]
 146                 = c
 147
 148 Steps =: 1000
 149
 150 animate2 n r c
 151         | n rem Steps == 0
 152                 = ["\r       \r",toString n," ":c]
 153                 = c
 154
 155 Test :: [Testoption] !p -> [String] | Testable p
 156 Test options p = (\config.testConfig config.randoms {config & randoms = []} p) (foldl handleOption verboseConfig options)
 157 where
 158         handleOption c (Tests i)                = {c & maxTests = i, maxArgs = 2*i}
 159         handleOption c (Fails i)                = {c & fails = i}
 160         handleOption c (Args i)                 = {c & maxArgs = i}
 161         handleOption c (RandomSeed i)   = {c & randoms = genRandInt i}
 162         handleOption c (RandomList r)   = {c & randoms = r}
 163         handleOption c Verbose                  = {c & every = verboseEvery}
 164         handleOption c Concise                  = {c & every = countEvery}
 165         handleOption c Quiet                    = {c & every = animate2}
 166
 167 TestList :: [Testoption] ![p] -> [String] | Testable p
 168 TestList options ps = flatten (map (Test options) ps)
 169
 170 test :: !p -> [String] | Testable p
 171 test p = testn NrOfTest p
 172
 173 testn :: !Int !p -> [String] | Testable p
 174 testn n p = verbosen n aStream p
 175
 176 testnm :: !Int !Int !p -> [String] | Testable p
 177 testnm n m p = testConfig aStream { verboseConfig & maxTests = n, maxArgs = 100*n, fails = m } p
 178
 179 ttestn :: !Int !p -> [String] | Testable p
 180 ttestn n p = testConfig aStream { traceConfig & maxTests = n, maxArgs = 100*n } p
 181
 182 ttestnm :: !Int !Int !p -> [String] | Testable p
 183 ttestnm n m p = testConfig aStream { traceConfig & maxTests = n, maxArgs = 100*n, fails = m } p
 184
 185 verbose  :: !RandomStream !p -> [String] | Testable p
 186 verbose rs p = testConfig rs verboseConfig p
 187
 188 verbosen :: !Int !RandomStream !p -> [String] | Testable p
 189 verbosen n rs p = testConfig rs { verboseConfig & maxTests = n, maxArgs = 100*n } p
 190
 191 concise :: !RandomStream !p -> [String] | Testable p
 192 concise rs p = testConfig rs countConfig p
 193
 194 concisen   :: !Int !RandomStream !p -> [String] | Testable p
 195 concisen n rs p = testConfig rs { countConfig & maxTests = n, maxArgs = 100*n } p
 196
 197 quiet :: !RandomStream !p -> [String] | Testable p
 198 quiet rs p = testConfig rs quietConfig p
 199
 200 quietn   :: !Int !RandomStream !p -> [String] | Testable p
 201 quietn n rs p = testConfig rs { quietConfig & maxTests = n, maxArgs = 100*n } p
 202
 203 quietnm   :: !Int !Int !RandomStream !p -> [String] | Testable p
 204 quietnm n m rs p = testConfig rs { quietConfig & maxTests = n, maxArgs = 100*n, fails = m } p
 205
 206 aStream :: RandomStream
 207 aStream = genRandInt 1957 //1964
 208
 209 gather :: [Admin] -> [[String]]
 210 gather list = [r.args \\ r<- list]
 211
 212 testConfig :: RandomStream Config p -> [String] | Testable p
 213 testConfig rs {maxTests,maxArgs,every,fails} p = analyse (evaluate p rs newAdmin) maxTests maxArgs 0 0 0 [] []
 214 where
 215         analyse :: ![.Admin] !Int !Int !Int !Int !Int ![(String,Int)] ![String] -> [String]
 216         analyse [] ntests nargs 0    0    0  labels name = [blank:showName name [" Proof: success for all arguments": conclude ntests nargs 0 0 labels]]
 217         analyse [] ntests nargs nrej 0    0  labels name = [blank:showName name [" Proof: Success for all not rejected arguments,": conclude ntests nargs nrej 0 labels]]
 218         analyse [] ntests nargs nrej nund 0  labels name
 219                 | ntests==maxTests      = [blank:showName name [" Undefined: no success nor counter example found, all tests rejected or undefined ": conclude ntests nargs nrej nund labels]]
 220                                                         = [blank:showName name [" Success for arguments, ": conclude ntests nargs nrej nund labels]]
 221         analyse [] ntests nargs nrej nund ne labels name = [blank:showName name [toString ne," counterexamples found,": conclude ntests nargs nrej nund labels]]
 222         analyse _  0      nargs nrej nund 0  labels name = [blank:showName name [" Passed": conclude 0 nargs nrej nund labels]]
 223         analyse _  0      nargs nrej nund ne labels name = [blank:showName name [toString ne," counterexamples found,": conclude 0 nargs nrej nund labels]]
 224         analyse _  ntests 0     nrej nund 0  labels name
 225                 | ntests==maxTests      = [blank:showName name [" No tests performed, maximum number of arguments (",toString maxArgs,") generated": conclude ntests 0 nrej nund labels]]
 226                                                         = [blank:showName name [" Passed: maximum number of arguments (",toString maxArgs,") generated": conclude ntests 0 nrej nund labels]]
 227         analyse _  ntests 0     nrej nund ne labels name = [blank:showName name [toString ne," counterexamples found,": conclude 0 0 nrej nund labels]]
 228         analyse [res:rest] ntests nargs nrej nund ne labels name
 229                 = every (maxTests-ntests+1) res
 230                   (     case res.res of
 231                          OK     = analyse rest (ntests-1) (nargs-1) nrej nund ne (admin res.labels labels) res.name
 232                          Pass   = analyse rest (ntests-1) (nargs-1) nrej nund ne (admin res.labels labels) res.name // NOT YET CORRECT ?
 233                          CE             = ["\r":showName res.name ["Counterexample ",toString (ne+1)," found after ",toString (maxTests-ntests+1)," tests:":showArgs res.args ["\n":more]]]
 234                                           where
 235                                                 more | ne+1<fails
 236                                                         = analyse rest (ntests-1) (nargs-1) nrej nund (ne+1) labels res.name
 237                                                         = showName res.name [toString (ne+1)," counterexamples found,": conclude (ntests-1) nargs nrej nund labels]
 238                          Rej    = analyse rest ntests (nargs-1) (nrej+1) nund     ne labels res.name
 239                          Undef  = analyse rest ntests (nargs-1) nrej     (nund+1) ne labels res.name
 240                                         = abort "Error in Gast: analyse; missing case for result\n"
 241                   )
 242
 243         conclude ntests nargs nrej nund labels
 244                 # n    = maxTests-ntests
 245                   rest = showLabels n (sort labels)
 246                   rest = case nrej of
 247                                         0 = rest
 248                                         1 = [" one case rejected":rest]
 249                                           = [" ",toString nrej," cases rejected":rest]
 250                   rest = case nund of
 251                                         0 = rest
 252                                         1 = [" one case undefined":rest]
 253                                           = [" ",toString nund," cases undefined":rest]
 254                 | n==0
 255                         = rest
 256                         = [" after ",toString n," tests":rest]
 257
 258         admin :: ![String] ![(String,Int)] -> [(String,Int)]
 259         admin [] accu = accu
 260         admin [label:rest] accu = admin rest (insert label accu)
 261
 262         insert :: !String ![(String,Int)] -> [(String,Int)]
 263         insert label [] = [(label,1)]
 264         insert label [this=:(old,n):rest]
 265          | label==old
 266                 = [(old,n+1):rest]
 267                 = [this:insert label rest]
 268
 269         showLabels :: !Int ![(String,Int)] -> [String]
 270         showLabels ntests [] = ["\n"]
 271         showLabels 0      [(lab,n):rest] = ["\n",lab,": ",toString n:showLabels 0 rest]
 272         showLabels ntests [(lab,n):rest] = ["\n",lab,": ",toString n," (",toString (toReal (n*100)/toReal ntests),"%)":showLabels ntests rest]
 273
 274         showName l c = s (reverse l) c
 275         where
 276                 s [] c = c
 277                 s [l] c = [l," ":c]
 278                 s [a:x] c = [a,".":s x c]
 279
 280 cr :== "\r"
 281
 282 showArgs :: ![String] [String] -> [String]
 283 showArgs []       c = c // ["\n":c] // c
 284 showArgs [a:rest] c = [" ",a: showArgs rest c]