--- /dev/null
+implementation module testable\r
+\r
+/*\r
+ GAST: A Generic Automatic Software Test-system\r
+ \r
+ testable: the test algorithm for logical properties\r
+\r
+ Pieter Koopman, 2002-2010\r
+ Radboud Universty, Nijmegen\r
+ The Netherlands\r
+ pieter@cs.ru.nl\r
+*/\r
+\r
+import StdEnv, MersenneTwister, genLibTest /*, StdTime*/ , gen\r
+\r
+derive gLess Result\r
+instance == Result where (==) x y = x===y\r
+\r
+newAdmin :: Admin\r
+newAdmin = {res=Undef, labels=[], args=[], name=[]}\r
+\r
+class TestArg a | genShow{|*|}, ggen{|*|} a\r
+\r
+//class Testable a where evaluate :: a RandomStream Admin -> [Admin]\r
+\r
+//instance Testable Bool where evaluate b rs result = [{result & res = if b OK CE, args = reverse result.args}]\r
+instance Testable Bool where evaluate b rs result=:{args} = [{result & args = reverse args, res = if b OK CE}]\r
+\r
+instance Testable Result where evaluate r rs result=:{args} = [{result & args = reverse args, res = r}]\r
+\r
+instance Testable Property\r
+where evaluate (Prop p) rs result = p rs result\r
+\r
+instance Testable (a->b) | Testable b & TestArg a \r
+where evaluate f rs admin\r
+ # (rs,rs2) = split rs\r
+ = forAll f (generateAll rs) rs2 admin\r
+\r
+instance Testable [a] | Testable a \r
+where\r
+// evaluate [] rs admin=:{args} = [{admin & args = reverse args, res = OK}] \r
+ evaluate list rs admin = diagonal [ evaluate x (genRandInt seed) admin \\ x<-list & seed<-rs ]\r
+// evaluate list rs admin = flatten [ evaluate x (genRandInt seed) admin \\ x<-list & seed<-rs ]\r
+\r
+:: Property = Prop (RandomStream Admin -> [Admin])\r
+\r
+prop :: a -> Property | Testable a\r
+prop p = Prop (evaluate p)\r
+\r
+forAll :: !(a->b) ![a] RandomStream !Admin -> [Admin] | Testable b & TestArg a\r
+forAll f [] rs r=:{args} = [{r & args = reverse args, res = OK}] // to handle empty sets of values\r
+forAll f list rs r = diagonal [apply f a (genRandInt seed) r \\ a<-list & seed<-rs ]\r
+\r
+apply :: !(a->b) a RandomStream !Admin -> [Admin] | Testable b & TestArg a\r
+apply f a rs r = evaluate (f a) rs {r & args = [show1 a:r.args]}\r
+\r
+diagonal :: [[a]] -> [a]\r
+diagonal list = f 1 2 list []\r
+where\r
+ f n m [] [] = []\r
+ f 0 m xs ys = f m (m+1) (rev ys xs) []\r
+ f n m [] ys = f m (m+1) (rev ys []) []\r
+ f n m [[x:r]:xs] ys = [x: f (n-1) m xs [r:ys]]\r
+ f n m [[]:xs] ys = f (n-1) m xs ys\r
+ \r
+ rev [] accu = accu\r
+ rev [x:r] accu = rev r [x:accu]\r
+\r
+generateAll :: !RandomStream -> [a] | ggen{|*|} a\r
+generateAll rnd = ggen{|*|} 2 rnd\r
+\r
+derive gEq Result\r
+derive bimap [], (,), (,,), (,,,), (,,,,), (,,,,,)\r
+\r
+//--- Random ---//\r
+\r
+split :: !RandomStream -> (RandomStream,RandomStream)\r
+split [r,s:rnd]\r
+ # seed = r*s\r
+ | seed==0\r
+ = split rnd\r
+ = (rnd, genRandInt seed)\r
+\r
+(>>=) infix 0 :: (a -> (b,a)) (b a -> d) -> a -> d\r
+(>>=) f g = \st = let (r,st1) = f st in g r st1\r
+\r
+result :: b -> a -> (b,a)\r
+result b = \a = (b,a)\r
+\r
+//--- testing ---//\r
+\r
+:: Config\r
+ = { maxTests :: Int\r
+ , maxArgs :: Int\r
+ , every :: Int Admin [String] -> [String]\r
+ , fails :: Int\r
+ , randoms :: [Int]\r
+ }\r
+\r
+verboseConfig\r
+ = { maxTests = NrOfTest\r
+ , maxArgs = 2*NrOfTest\r
+ , every = verboseEvery\r
+ , fails = 1\r
+ , randoms = aStream\r
+ }\r
+verboseEvery n r c = [blank,toString n,":":showArgs r.args c]\r
+\r
+traceConfig\r
+ = { maxTests = 100\r
+ , maxArgs = 1000\r
+ , every = traceEvery\r
+ , fails = 1\r
+ , randoms = aStream\r
+ }\r
+traceEvery n r c = ["\n",toString n,":":showArgs r.args c]\r
+\r
+blank :: String\r
+blank =: { createArray len ' ' & [0] = '\r', [len-1] = '\r' } where len = 81\r
+\r
+countConfig\r
+ = { maxTests = 100\r
+ , maxArgs = 10000\r
+ , every = countEvery\r
+ , fails = 1\r
+ , randoms = aStream\r
+ }\r
+countEvery n r c = [toString n,"\r": c]\r
+\r
+quietConfig\r
+ = { maxTests = 1000\r
+ , maxArgs = 10000\r
+ , every = animate2 // \n r c = if (n rem 10000 == 0) [".":c] c\r
+ , fails = 1\r
+ , randoms = aStream\r
+ }\r
+\r
+animate n r c\r
+ | n rem Steps == 0\r
+ = case (n/Steps) rem 4 of\r
+ 0 = ["\r|":c]\r
+ 1 = ["\r/":c]\r
+ 2 = ["\r-":c]\r
+ 3 = ["\r\\":c]\r
+ = ["??":c]\r
+ = c\r
+\r
+Steps =: 1000\r
+\r
+animate2 n r c\r
+ | n rem Steps == 0\r
+ = ["\r \r",toString n," ":c]\r
+ = c\r
+\r
+Test :: [Testoption] !p -> [String] | Testable p\r
+Test options p = (\config.testConfig config.randoms {config & randoms = []} p) (foldl handleOption verboseConfig options)\r
+where\r
+ handleOption c (Tests i) = {c & maxTests = i, maxArgs = 2*i}\r
+ handleOption c (Fails i) = {c & fails = i}\r
+ handleOption c (Args i) = {c & maxArgs = i}\r
+ handleOption c (RandomSeed i) = {c & randoms = genRandInt i}\r
+ handleOption c (RandomList r) = {c & randoms = r}\r
+ handleOption c Verbose = {c & every = verboseEvery}\r
+ handleOption c Concise = {c & every = countEvery}\r
+ handleOption c Quiet = {c & every = animate2}\r
+\r
+TestList :: [Testoption] ![p] -> [String] | Testable p\r
+TestList options ps = flatten (map (Test options) ps)\r
+\r
+test :: !p -> [String] | Testable p\r
+test p = testn NrOfTest p\r
+\r
+testn :: !Int !p -> [String] | Testable p\r
+testn n p = verbosen n aStream p\r
+\r
+testnm :: !Int !Int !p -> [String] | Testable p\r
+testnm n m p = testConfig aStream { verboseConfig & maxTests = n, maxArgs = 100*n, fails = m } p\r
+\r
+ttestn :: !Int !p -> [String] | Testable p\r
+ttestn n p = testConfig aStream { traceConfig & maxTests = n, maxArgs = 100*n } p\r
+\r
+ttestnm :: !Int !Int !p -> [String] | Testable p\r
+ttestnm n m p = testConfig aStream { traceConfig & maxTests = n, maxArgs = 100*n, fails = m } p\r
+\r
+verbose :: !RandomStream !p -> [String] | Testable p\r
+verbose rs p = testConfig rs verboseConfig p\r
+\r
+verbosen :: !Int !RandomStream !p -> [String] | Testable p\r
+verbosen n rs p = testConfig rs { verboseConfig & maxTests = n, maxArgs = 100*n } p\r
+\r
+concise :: !RandomStream !p -> [String] | Testable p\r
+concise rs p = testConfig rs countConfig p\r
+\r
+concisen :: !Int !RandomStream !p -> [String] | Testable p\r
+concisen n rs p = testConfig rs { countConfig & maxTests = n, maxArgs = 100*n } p\r
+\r
+quiet :: !RandomStream !p -> [String] | Testable p\r
+quiet rs p = testConfig rs quietConfig p\r
+\r
+quietn :: !Int !RandomStream !p -> [String] | Testable p\r
+quietn n rs p = testConfig rs { quietConfig & maxTests = n, maxArgs = 100*n } p\r
+\r
+quietnm :: !Int !Int !RandomStream !p -> [String] | Testable p\r
+quietnm n m rs p = testConfig rs { quietConfig & maxTests = n, maxArgs = 100*n, fails = m } p\r
+\r
+aStream :: RandomStream\r
+aStream = genRandInt 1957 //1964\r
+\r
+gather :: [Admin] -> [[String]]\r
+gather list = [r.args \\ r<- list]\r
+\r
+testConfig :: RandomStream Config p -> [String] | Testable p\r
+testConfig rs {maxTests,maxArgs,every,fails} p = analyse (evaluate p rs newAdmin) maxTests maxArgs 0 0 0 [] []\r
+where\r
+ analyse :: ![.Admin] !Int !Int !Int !Int !Int ![(String,Int)] ![String] -> [String]\r
+ analyse [] ntests nargs 0 0 0 labels name = [blank:showName name [" Proof: success for all arguments": conclude ntests nargs 0 0 labels]]\r
+ analyse [] ntests nargs nrej 0 0 labels name = [blank:showName name [" Proof: Success for all not rejected arguments,": conclude ntests nargs nrej 0 labels]]\r
+ analyse [] ntests nargs nrej nund 0 labels name \r
+ | ntests==maxTests = [blank:showName name [" Undefined: no success nor counter example found, all tests rejected or undefined ": conclude ntests nargs nrej nund labels]]\r
+ = [blank:showName name [" Success for arguments, ": conclude ntests nargs nrej nund labels]]\r
+ analyse [] ntests nargs nrej nund ne labels name = [blank:showName name [toString ne," counterexamples found,": conclude ntests nargs nrej nund labels]]\r
+ analyse _ 0 nargs nrej nund 0 labels name = [blank:showName name [" Passed": conclude 0 nargs nrej nund labels]]\r
+ analyse _ 0 nargs nrej nund ne labels name = [blank:showName name [toString ne," counterexamples found,": conclude 0 nargs nrej nund labels]]\r
+ analyse _ ntests 0 nrej nund 0 labels name \r
+ | ntests==maxTests = [blank:showName name [" No tests performed, maximum number of arguments (",toString maxArgs,") generated": conclude ntests 0 nrej nund labels]]\r
+ = [blank:showName name [" Passed: maximum number of arguments (",toString maxArgs,") generated": conclude ntests 0 nrej nund labels]]\r
+ analyse _ ntests 0 nrej nund ne labels name = [blank:showName name [toString ne," counterexamples found,": conclude 0 0 nrej nund labels]]\r
+ analyse [res:rest] ntests nargs nrej nund ne labels name \r
+ = every (maxTests-ntests+1) res\r
+ ( case res.res of\r
+ OK = analyse rest (ntests-1) (nargs-1) nrej nund ne (admin res.labels labels) res.name\r
+ Pass = analyse rest (ntests-1) (nargs-1) nrej nund ne (admin res.labels labels) res.name // NOT YET CORRECT ?\r
+ CE = ["\r":showName res.name ["Counterexample ",toString (ne+1)," found after ",toString (maxTests-ntests+1)," tests:":showArgs res.args ["\n":more]]]\r
+ where\r
+ more | ne+1<fails\r
+ = analyse rest (ntests-1) (nargs-1) nrej nund (ne+1) labels res.name\r
+ = showName res.name [toString (ne+1)," counterexamples found,": conclude (ntests-1) nargs nrej nund labels]\r
+ Rej = analyse rest ntests (nargs-1) (nrej+1) nund ne labels res.name\r
+ Undef = analyse rest ntests (nargs-1) nrej (nund+1) ne labels res.name\r
+ = abort "Error in Gast: analyse; missing case for result\n"\r
+ )\r
+\r
+ conclude ntests nargs nrej nund labels\r
+ # n = maxTests-ntests\r
+ rest = showLabels n (sort labels)\r
+ rest = case nrej of\r
+ 0 = rest\r
+ 1 = [" one case rejected":rest]\r
+ = [" ",toString nrej," cases rejected":rest]\r
+ rest = case nund of\r
+ 0 = rest\r
+ 1 = [" one case undefined":rest]\r
+ = [" ",toString nund," cases undefined":rest]\r
+ | n==0\r
+ = rest\r
+ = [" after ",toString n," tests":rest]\r
+\r
+ admin :: ![String] ![(String,Int)] -> [(String,Int)]\r
+ admin [] accu = accu\r
+ admin [label:rest] accu = admin rest (insert label accu)\r
+\r
+ insert :: !String ![(String,Int)] -> [(String,Int)]\r
+ insert label [] = [(label,1)]\r
+ insert label [this=:(old,n):rest]\r
+ | label==old\r
+ = [(old,n+1):rest]\r
+ = [this:insert label rest]\r
+\r
+ showLabels :: !Int ![(String,Int)] -> [String]\r
+ showLabels ntests [] = ["\n"]\r
+ showLabels 0 [(lab,n):rest] = ["\n",lab,": ",toString n:showLabels 0 rest]\r
+ showLabels ntests [(lab,n):rest] = ["\n",lab,": ",toString n," (",toString (toReal (n*100)/toReal ntests),"%)":showLabels ntests rest]\r
+\r
+ showName l c = s (reverse l) c\r
+ where\r
+ s [] c = c\r
+ s [l] c = [l," ":c]\r
+ s [a:x] c = [a,".":s x c]\r
+\r
+cr :== "\r"\r
+\r
+showArgs :: ![String] [String] -> [String]\r
+showArgs [] c = c // ["\n":c] // c\r
+showArgs [a:rest] c = [" ",a: showArgs rest c]\r