+++ /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
repositories / tt2015.git / blobdiff