1 implementation module testable
4 GAST: A Generic Automatic Software Test-system
6 testable: the test algorithm for logical properties
8 Pieter Koopman, 2002-2010
9 Radboud Universty, Nijmegen
14 import StdEnv, MersenneTwister, genLibTest /*, StdTime*/ , gen
17 instance == Result where (==) x y = x===y
20 newAdmin = {res=Undef, labels=[], args=[], name=[]}
22 class TestArg a | genShow{|*|}, ggen{|*|} a
24 //class Testable a where evaluate :: a RandomStream Admin -> [Admin]
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}]
29 instance Testable Result where evaluate r rs result=:{args} = [{result & args = reverse args, res = r}]
31 instance Testable Property
32 where evaluate (Prop p) rs result = p rs result
34 instance Testable (a->b) | Testable b & TestArg a
35 where evaluate f rs admin
37 = forAll f (generateAll rs) rs2 admin
39 instance Testable [a] | Testable a
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 ]
45 :: Property = Prop (RandomStream Admin -> [Admin])
47 prop :: a -> Property | Testable a
48 prop p = Prop (evaluate p)
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 ]
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]}
57 diagonal :: [[a]] -> [a]
58 diagonal list = f 1 2 list []
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
67 rev [x:r] accu = rev r [x:accu]
69 generateAll :: !RandomStream -> [a] | ggen{|*|} a
70 generateAll rnd = ggen{|*|} 2 rnd
73 derive bimap [], (,), (,,), (,,,), (,,,,), (,,,,,)
77 split :: !RandomStream -> (RandomStream,RandomStream)
82 = (rnd, genRandInt seed)
84 (>>=) infix 0 :: (a -> (b,a)) (b a -> d) -> a -> d
85 (>>=) f g = \st = let (r,st1) = f st in g r st1
87 result :: b -> a -> (b,a)
95 , every :: Int Admin [String] -> [String]
101 = { maxTests = NrOfTest
102 , maxArgs = 2*NrOfTest
103 , every = verboseEvery
107 verboseEvery n r c = [blank,toString n,":":showArgs r.args c]
116 traceEvery n r c = ["\n",toString n,":":showArgs r.args c]
119 blank =: { createArray len ' ' & [0] = '\r', [len-1] = '\r' } where len = 81
128 countEvery n r c = [toString n,"\r": c]
133 , every = animate2 // \n r c = if (n rem 10000 == 0) [".":c] c
140 = case (n/Steps) rem 4 of
152 = ["\r \r",toString n," ":c]
155 Test :: [Testoption] !p -> [String] | Testable p
156 Test options p = (\config.testConfig config.randoms {config & randoms = []} p) (foldl handleOption verboseConfig options)
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}
167 TestList :: [Testoption] ![p] -> [String] | Testable p
168 TestList options ps = flatten (map (Test options) ps)
170 test :: !p -> [String] | Testable p
171 test p = testn NrOfTest p
173 testn :: !Int !p -> [String] | Testable p
174 testn n p = verbosen n aStream p
176 testnm :: !Int !Int !p -> [String] | Testable p
177 testnm n m p = testConfig aStream { verboseConfig & maxTests = n, maxArgs = 100*n, fails = m } p
179 ttestn :: !Int !p -> [String] | Testable p
180 ttestn n p = testConfig aStream { traceConfig & maxTests = n, maxArgs = 100*n } p
182 ttestnm :: !Int !Int !p -> [String] | Testable p
183 ttestnm n m p = testConfig aStream { traceConfig & maxTests = n, maxArgs = 100*n, fails = m } p
185 verbose :: !RandomStream !p -> [String] | Testable p
186 verbose rs p = testConfig rs verboseConfig p
188 verbosen :: !Int !RandomStream !p -> [String] | Testable p
189 verbosen n rs p = testConfig rs { verboseConfig & maxTests = n, maxArgs = 100*n } p
191 concise :: !RandomStream !p -> [String] | Testable p
192 concise rs p = testConfig rs countConfig p
194 concisen :: !Int !RandomStream !p -> [String] | Testable p
195 concisen n rs p = testConfig rs { countConfig & maxTests = n, maxArgs = 100*n } p
197 quiet :: !RandomStream !p -> [String] | Testable p
198 quiet rs p = testConfig rs quietConfig p
200 quietn :: !Int !RandomStream !p -> [String] | Testable p
201 quietn n rs p = testConfig rs { quietConfig & maxTests = n, maxArgs = 100*n } p
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
206 aStream :: RandomStream
207 aStream = genRandInt 1957 //1964
209 gather :: [Admin] -> [[String]]
210 gather list = [r.args \\ r<- list]
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 [] []
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
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]]]
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"
243 conclude ntests nargs nrej nund labels
244 # n = maxTests-ntests
245 rest = showLabels n (sort labels)
248 1 = [" one case rejected":rest]
249 = [" ",toString nrej," cases rejected":rest]
252 1 = [" one case undefined":rest]
253 = [" ",toString nund," cases undefined":rest]
256 = [" after ",toString n," tests":rest]
258 admin :: ![String] ![(String,Int)] -> [(String,Int)]
260 admin [label:rest] accu = admin rest (insert label accu)
262 insert :: !String ![(String,Int)] -> [(String,Int)]
263 insert label [] = [(label,1)]
264 insert label [this=:(old,n):rest]
267 = [this:insert label rest]
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]
274 showName l c = s (reverse l) c
278 s [a:x] c = [a,".":s x c]
282 showArgs :: ![String] [String] -> [String]
283 showArgs [] c = c // ["\n":c] // c
284 showArgs [a:rest] c = [" ",a: showArgs rest c]