Testable.icl 16.2 KB
Newer Older
1
implementation module Gast.Testable
Bas Lijnse's avatar
Bas Lijnse committed
2 3 4 5

/*
	GAST: A Generic Automatic Software Test-system
	
6
	testable: the test algorithm for logical properties
Bas Lijnse's avatar
Bas Lijnse committed
7

8
	Pieter Koopman, 2002-2010
Bas Lijnse's avatar
Bas Lijnse committed
9 10 11 12 13
	Radboud Universty, Nijmegen
	The Netherlands
	pieter@cs.ru.nl
*/

Camil Staps's avatar
Camil Staps committed
14 15
import StdEnv

16
from Data.Func import $
Camil Staps's avatar
Camil Staps committed
17
import Data.Functor
18
from Data.List import instance Functor [], concatMap
Camil Staps's avatar
Camil Staps committed
19 20 21 22
import qualified Data.Map as Map
import Math.Random
import Testing.TestEvents
import Text
Camil Staps's avatar
Camil Staps committed
23
import Text.GenJSON
24
import Text.GenPrint
Camil Staps's avatar
Camil Staps committed
25 26 27 28 29
import Text.Language

import Gast.Gen
import Gast.GenLibTest
import Gast.ThunkNames
Bas Lijnse's avatar
Bas Lijnse committed
30 31 32 33 34

derive gLess Result
instance == Result where (==) x y = x===y

newAdmin :: Admin
35
newAdmin = { res=Undef, labels=[], args=[], argsRepresentation = [], failedAssertions = []
36
           , namePath = []
37 38
           , recFieldValueNrLimits = 'Map'.newMap
           }
Bas Lijnse's avatar
Bas Lijnse committed
39

40
instance Testable Bool where
41 42
    evaluate b genState result=:{Admin| args, argsRepresentation} =
        [{result & args = reverse args, argsRepresentation = reverse argsRepresentation, res = if b OK CE}]
Camil Staps's avatar
Camil Staps committed
43
	testname b = "Bool"
Bas Lijnse's avatar
Bas Lijnse committed
44

45
instance Testable Result where
46 47
    evaluate r genState result=:{Admin| args, argsRepresentation} =
        [{result & args = reverse args, argsRepresentation = reverse argsRepresentation, res = r}]
Camil Staps's avatar
Camil Staps committed
48
	testname r = "Result"
Bas Lijnse's avatar
Bas Lijnse committed
49 50

instance Testable Property
Camil Staps's avatar
Camil Staps committed
51 52 53
where
	evaluate (Prop _ p) genState result = p genState result
	testname (Prop n _) = n
Bas Lijnse's avatar
Bas Lijnse committed
54

55
instance Testable (a->b) | Testable b & genShow{|*|} a & ggen{|*|} a & TestArg a  
56
where
Camil Staps's avatar
Camil Staps committed
57 58 59 60
	evaluate f genState admin = forAll f (generateAll genState`) genState` admin
	where
		genState` = {GenState| genState & recFieldValueNrLimits = admin.Admin.recFieldValueNrLimits}
	testname f = thunk_name_to_string f
Bas Lijnse's avatar
Bas Lijnse committed
61 62 63

instance Testable [a] | Testable a  
where
64
	evaluate list genState admin = diagonal [ evaluate x genState admin \\ x<-list ] // copy the genState
Camil Staps's avatar
Camil Staps committed
65
	testname xs = "[" +++ join "," (map testname xs) +++ "]"
Bas Lijnse's avatar
Bas Lijnse committed
66 67

prop :: a -> Property | Testable a
Camil Staps's avatar
Camil Staps committed
68
prop p = Prop (testname p) (evaluate p)
Bas Lijnse's avatar
Bas Lijnse committed
69

70
forAll :: !(a->b) ![a] GenState !Admin -> [Admin] | Testable b & TestArg a
71
forAll f []   genState r=:{Admin| args} = [{r & args = reverse args, res = OK}] // to handle empty sets of values
72
forAll f list genState r = diagonal [apply f a genState r \\ a<-list ] // copy the genState
Bas Lijnse's avatar
Bas Lijnse committed
73

74
apply :: !(a->b) a GenState !Admin -> [Admin] | Testable b & TestArg a
75
apply f a genState r =
76
    evaluate (f a) genState {Admin| r & args = [show1 a:r.Admin.args], argsRepresentation = [printToString a : r.Admin.argsRepresentation]}
Bas Lijnse's avatar
Bas Lijnse committed
77

78
diagonal :: ![[a]] -> [a]
Bas Lijnse's avatar
Bas Lijnse committed
79 80 81 82 83 84 85 86 87 88 89
diagonal list = f 1 2 list []
where
	f n m [] [] = []
	f 0 m xs ys = f m (m+1) (rev ys xs) []
	f n m [] ys = f m (m+1) (rev ys []) []
	f n m [[x:r]:xs] ys = [x: f (n-1) m xs [r:ys]]
	f n m [[]:xs] ys = f (n-1) m xs ys
	
	rev []    accu = accu
	rev [x:r] accu = rev r [x:accu]

90 91
generateAll :: !GenState -> [a] | ggen{|*|} a // & genType{|*|} a
generateAll genState = l where l = ggen{|*|} genState // {genState & currType = hd (genType{|*|} [] [] l) }
Bas Lijnse's avatar
Bas Lijnse committed
92 93 94 95 96 97

derive gEq Result
derive bimap [], (,), (,,), (,,,), (,,,,), (,,,,,)

//--- testing ---//

98 99 100 101 102 103
:: Config =
	{ maxTests :: Int
	, maxArgs  :: Int
	, fails    :: Int
	, randoms  :: [Int]
	, genState :: GenState
Bas Lijnse's avatar
Bas Lijnse committed
104 105
	}

106 107 108 109 110 111 112 113 114 115 116 117
printEvents :: PrintConfig [GastEvent] -> [String]
printEvents pc [ge:ges] = case s of
	"" -> printEvents pc ges
	s  -> [s:printEvents pc ges]
where
	s = case ge of
		GE_TestStarted n               -> pc.beforeStartOutput n
		GE_TestFinished n r ces labels -> pc.resultOutput n r ces labels
		GE_CounterExample ce           -> pc.counterExampleOutput ce
		GE_Tick n adm                  -> pc.everyOutput n adm
printEvents _ [] = []

118 119 120 121
defaultTestConfig =
	{ maxTests = 1000
	, maxArgs  = 2000
	, fails    = 1
122 123 124
	, randoms  = aStream
	, genState = genState
	}
125

126 127
verbosePrintConfig =
	{ everyOutput          = verboseEvery
Camil Staps's avatar
Camil Staps committed
128
	, counterExampleOutput = humanReadableCEOutput True False
129 130 131 132
	, beforeStartOutput    = noBeforeOutput
	, resultOutput         = humanReadableResOutput True
	}
verboseEvery n r = blank <+ n <+ ":" <+ join " " r.Admin.args
133

134 135
tracePrintConfig =
	{ everyOutput          = traceEvery
Camil Staps's avatar
Camil Staps committed
136
	, counterExampleOutput = humanReadableCEOutput False False
137 138
	, beforeStartOutput    = noBeforeOutput
	, resultOutput         = humanReadableResOutput True
Bas Lijnse's avatar
Bas Lijnse committed
139
	}
140
traceEvery n r = n <+ ":" <+ join " " r.Admin.args <+ "\n"
Bas Lijnse's avatar
Bas Lijnse committed
141 142 143 144

blank :: String
blank =: { createArray len ' ' & [0] = '\r', [len-1] = '\r' } where len = 81

Camil Staps's avatar
Camil Staps committed
145 146 147
countPrintConfig n =
	{ everyOutput          = countEvery n
	, counterExampleOutput = humanReadableCEOutput True True
148 149
	, beforeStartOutput    = noBeforeOutput
	, resultOutput         = humanReadableResOutput True
150
	}
151 152 153 154 155 156 157
countEvery :: !Int !Int Admin -> String
countEvery steps n r
| n rem steps == 0 = toString n +++ "\r"
| otherwise        = ""

quietPrintConfig =
	{ everyOutput          = noEveryOutput
Camil Staps's avatar
Camil Staps committed
158
	, counterExampleOutput = noCounterExampleOutput
159
	, beforeStartOutput    = noBeforeOutput
Camil Staps's avatar
Camil Staps committed
160
	, resultOutput         = humanReadableResOutput False
Bas Lijnse's avatar
Bas Lijnse committed
161 162
	}

163 164 165 166 167 168
testEventsPrintConfig =
	{ everyOutput          = noEveryOutput
	, counterExampleOutput = noCounterExampleOutput
	, beforeStartOutput    = jsonEventStart
	, resultOutput         = jsonEventEnd
	}
169

170 171 172 173 174 175 176 177 178
noCounterExampleOutput :: CounterExampleRes -> String
noCounterExampleOutput _ = ""

noBeforeOutput :: !String -> String
noBeforeOutput _ = ""

noEveryOutput :: !Int Admin -> String
noEveryOutput n _ = ""

Camil Staps's avatar
Camil Staps committed
179 180 181 182 183
humanReadableCEOutput :: Bool Bool CounterExampleRes -> String
humanReadableCEOutput newLine showArgs {maxTests, nTests, nE, args, name, failedAssertions} = concat $
	if showArgs [(maxTests-nTests+1) <+ ":" <+ join " " args] [] ++
	if newLine ["\n"] [] ++
	[ showName True name
184 185 186 187
	, "Counterexample "
	, toString (nE+1)
	, " found after "
	, pluralisen English (maxTests-nTests+1) "test"
Camil Staps's avatar
Camil Staps committed
188
	, ": "
189
	, join " " args
Camil Staps's avatar
Camil Staps committed
190
	, "\n"
191 192
	: concatMap showFailedAssertion failedAssertions
	]
193
where
194
	showFailedAssertion :: !(!FailedAssertion, !String, !String) -> [String]
Camil Staps's avatar
Camil Staps committed
195
	showFailedAssertion (ExpectedRelation _ rel _, x, y) = ["not (", x, " ", toString rel, " ", y, ")\n"]
196 197 198

humanReadableResOutput :: Bool String TestsResult [CounterExampleRes] [(String, Int)] -> String
humanReadableResOutput addWhite name {maxTests, nRej, resultType} _ labels = withBlank $ showName True name +++ resStr
199
where
200
	resStr = case resultType of
Camil Staps's avatar
Camil Staps committed
201
		Proof nTests -> "Proof: " +++ msgStr +++ conclude nTests 0 labels
202 203
		with
			msgStr = if (nRej == 0) "success for all arguments" "success for all non-rejected arguments"
Camil Staps's avatar
Camil Staps committed
204
		PassedTest maxArgs nTests nUnd allArgsGenerated -> msgStr +++ conclude nTests nUnd labels
205 206 207 208 209
		with
			msgStr
			| allArgsGenerated = "Passed: success for arguments"
			| nTests == 0      = "Passed"
			| otherwise        = "Passed: maximum number of arguments (" <+ maxArgs <+ ") generated"
Camil Staps's avatar
Camil Staps committed
210 211 212
		CounterExpls nTests nUnd nE -> pluralisen English nE "counterexample" +++ " found" +++ conclude nTests nUnd labels
		Undefined nUnd -> "Undefined: no success nor counterexample found, all tests rejected or undefined" +++ conclude maxTests nUnd labels
		NoTests maxArgs nTests nUnd -> "No tests performed, maximum number of arguments (" <+ maxArgs <+ ") generated" +++ conclude nTests nUnd labels
213 214 215 216 217

	withBlank x
	| addWhite  = blank +++ x
	| otherwise = x

Camil Staps's avatar
Camil Staps committed
218 219
	conclude :: Int Int [(String, Int)] -> String
	conclude ntests nund labels
220
		# n    = maxTests-ntests
Camil Staps's avatar
Camil Staps committed
221
		# rest = showLabels n (sort labels)
222 223 224 225 226 227 228 229 230 231
		# rest = case nRej of
			0 -> rest
			n -> [", ", pluralisen English n "case", " rejected": rest]
		# rest = case nund of
			0 -> rest
			n -> [", ", pluralisen English n "case", " undefined": rest]
		| n==0
			= concat rest
			= concat [" after ",pluralisen English n "test":rest]

Camil Staps's avatar
Camil Staps committed
232 233 234 235
	showLabels :: !Int ![(String,Int)] -> [String]
	showLabels ntests [] = ["\n"]
	showLabels 0      [(lab,n):rest] = ["\n",lab,": ",toString n:showLabels 0 rest]
	showLabels ntests [(lab,n):rest] = ["\n",lab,": ",toString n," (",toString (toReal (n*100)/toReal ntests),"%)":showLabels ntests rest]
236 237 238 239 240 241

jsonEventStart :: !String -> String
jsonEventStart name = toString (toJSON {StartEvent | name=name}) +++ "\n"

jsonEventEnd :: String TestsResult [CounterExampleRes] [(String, Int)] -> String
jsonEventEnd name res counterExamples labels = toString (toJSON endEvent) +++ "\n"
242
where
243 244 245 246 247
	endEvent =
		{ name    = showName False name
		, event   = eventType
		, message = concat
			[ humanReadableResOutput False name res counterExamples labels
Camil Staps's avatar
Camil Staps committed
248
			: map (humanReadableCEOutput False False) counterExamples
249 250 251 252 253 254 255 256
			]
		}

	eventType = case res.resultType of
		Proof _            -> Passed
		PassedTest _ _ _ _ -> Passed
		CounterExpls _ _ _ -> Failed $ Just $ CounterExamples $
			(\ce ->
Camil Staps's avatar
Camil Staps committed
257
				{ counterExample   = map GPrint ce.CounterExampleRes.argsRepresentation
258 259 260 261 262 263 264 265
				, failedAssertions = fst3 <$> ce.CounterExampleRes.failedAssertions
				}
			) <$> counterExamples
		Undefined _        -> Failed Nothing
		NoTests _ _ _      -> Failed Nothing

showName :: Bool String -> String
showName quoteName l = if quoteName ("\"" <+ l <+ "\" ") l
266

267 268
toPrintConfig :: ([PrintOption] -> PrintConfig)
toPrintConfig = foldl handleOption verbosePrintConfig
269
where
Camil Staps's avatar
Camil Staps committed
270 271 272 273
	handleOption pc Verbose          = verbosePrintConfig
	handleOption pc Trace            = tracePrintConfig
	handleOption pc (Concise n)      = countPrintConfig n
	handleOption pc Quiet            = quietPrintConfig
274
	handleOption pc OutputTestEvents =
275 276 277 278 279
		{ pc
		& everyOutput          = noEveryOutput
		, counterExampleOutput = noCounterExampleOutput
		, resultOutput         = jsonEventEnd
		, beforeStartOutput    = jsonEventStart
280
		}
281 282

derive genShow Testoption, GenType
283 284 285 286

Test :: ![Testoption] !p -> [GastEvent] | Testable p
Test options p = testConfig config.randoms {config & randoms = []} p
where
287
	config = foldl handleOption defaultTestConfig options
288 289 290 291 292 293 294 295

	handleOption c (Tests i)      = {c & maxTests = i, maxArgs = 2*i}
	handleOption c (Fails i)      = {c & fails = i}
	handleOption c (Args i)       = {c & maxArgs = i}
	handleOption c (RandomSeed i) = {c & randoms = genRandInt i}
	handleOption c (RandomList r) = {c & randoms = r}
	handleOption c (MaxDepth i)   = {c & genState = {c.genState & maxDepth = i}}
	handleOption c (Skew s)
296 297 298 299
	| s > 0     = {c & genState = {c.genState & mode = SkewGeneration {skewl = 1, skewr = s}}}
	| s < 0     = {c & genState = {c.genState & mode = SkewGeneration {skewl = ~s, skewr = 1}}}
	| otherwise = {c & genState = {c.genState & mode = SkewGeneration {skewl = 1, skewr = 1}}}
	handleOption c Bent = {c & genState = {c.genState & mode = BentGeneration}}
300 301 302
	handleOption _ o = abort ("Test: unknown option \"" +++ show1 o +++ "\"\n")

TestList :: ![Testoption] ![p] -> [GastEvent] | Testable p
303 304
TestList options ps = flatten (map (Test options) ps)

Bas Lijnse's avatar
Bas Lijnse committed
305
test :: !p -> [String] | Testable p
306
test p = testn 1000 p
Bas Lijnse's avatar
Bas Lijnse committed
307 308 309 310 311

testn :: !Int !p -> [String] | Testable p
testn n p = verbosen n aStream p

testnm :: !Int !Int !p -> [String] | Testable p
312
testnm n m p = printEvents verbosePrintConfig $ testConfig aStream { defaultTestConfig & maxTests = n, maxArgs = 100*n, fails = m } p
Bas Lijnse's avatar
Bas Lijnse committed
313 314

ttestn :: !Int !p -> [String] | Testable p
315
ttestn n p = printEvents verbosePrintConfig $ testConfig aStream { defaultTestConfig & maxTests = n, maxArgs = 100*n } p
Bas Lijnse's avatar
Bas Lijnse committed
316 317

ttestnm :: !Int !Int !p -> [String] | Testable p
318
ttestnm n m p = printEvents verbosePrintConfig $ testConfig aStream { defaultTestConfig & maxTests = n, maxArgs = 100*n, fails = m } p
Bas Lijnse's avatar
Bas Lijnse committed
319 320

verbose  :: !RandomStream !p -> [String] | Testable p
321
verbose rs p = printEvents verbosePrintConfig $ testConfig rs defaultTestConfig p
Bas Lijnse's avatar
Bas Lijnse committed
322 323

verbosen :: !Int !RandomStream !p -> [String] | Testable p
324
verbosen n rs p = printEvents verbosePrintConfig $ testConfig rs { defaultTestConfig & maxTests = n, maxArgs = 100*n } p
Bas Lijnse's avatar
Bas Lijnse committed
325 326

concise :: !RandomStream !p -> [String] | Testable p
Camil Staps's avatar
Camil Staps committed
327
concise rs p = printEvents (countPrintConfig 100) $ testConfig rs defaultTestConfig p
Bas Lijnse's avatar
Bas Lijnse committed
328 329

concisen   :: !Int !RandomStream !p -> [String] | Testable p
Camil Staps's avatar
Camil Staps committed
330
concisen n rs p = printEvents (countPrintConfig 100) $ testConfig rs { defaultTestConfig & maxTests = n, maxArgs = 100*n } p
Bas Lijnse's avatar
Bas Lijnse committed
331 332

quiet :: !RandomStream !p -> [String] | Testable p
333
quiet rs p = printEvents quietPrintConfig $ testConfig rs defaultTestConfig p
Bas Lijnse's avatar
Bas Lijnse committed
334 335

quietn   :: !Int !RandomStream !p -> [String] | Testable p
336
quietn n rs p = printEvents quietPrintConfig $ testConfig rs { defaultTestConfig & maxTests = n, maxArgs = 100*n } p
Bas Lijnse's avatar
Bas Lijnse committed
337 338

quietnm   :: !Int !Int !RandomStream !p -> [String] | Testable p
339
quietnm n m rs p = printEvents quietPrintConfig $ testConfig rs { defaultTestConfig & maxTests = n, maxArgs = 100*n, fails = m } p
Bas Lijnse's avatar
Bas Lijnse committed
340

341
testEvents :: !RandomStream !p -> [String] | Testable p
342
testEvents rs p = printEvents testEventsPrintConfig $ testConfig rs defaultTestConfig p
Bas Lijnse's avatar
Bas Lijnse committed
343

344
testEventsn :: !Int !RandomStream !p -> [String] | Testable p
345
testEventsn n rs p = printEvents testEventsPrintConfig $ testConfig rs { defaultTestConfig & maxTests = n, maxArgs = 100*n } p
Bas Lijnse's avatar
Bas Lijnse committed
346

347 348 349 350
testConfig :: RandomStream Config p -> [GastEvent] | Testable p
testConfig rs {maxTests,maxArgs,fails,genState} p
	# res = evaluate p genState newAdmin
	= [GE_TestStarted (testname p):analyse res maxTests maxArgs 0 0 0 [] []]
Bas Lijnse's avatar
Bas Lijnse committed
351
where
352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369
	analyse :: ![.Admin] !Int !Int !Int !Int !Int [CounterExampleRes] ![(String,Int)] -> [GastEvent]
	analyse results nTests nArgs nRej nUnd nE counterExamples labels =
		case analyse` results nTests nArgs nRej nUnd nE of
			// testing of property finished
			Just resType -> [GE_TestFinished
				(testname p)
				{maxTests = maxTests, nRej = nRej, resultType = resType}
				counterExamples
				labels]
			// continue with testing property
			Nothing ->
				let [res:rest] = results in
				[GE_Tick (maxTests-nTests+1) res:case res.res of
					OK   -> analyse rest (nTests-1) (nArgs-1) nRej nUnd nE counterExamples (admin res.labels labels)
					Pass -> analyse rest (nTests-1) (nArgs-1) nRej nUnd nE counterExamples (admin res.labels labels) // NOT YET CORRECT ?
					CE   -> [GE_CounterExample counterExample:more]
					with
						counterExample =
370 371 372 373 374 375 376
							{ maxTests           = maxTests
							, nTests             = nTests
							, nE                 = nE
							, args               = res.Admin.args
							, argsRepresentation = res.Admin.argsRepresentation
							, name               = let n = testname p in join "." [n:dropWhile ((==) n) (reverse res.namePath)]
							, failedAssertions   = res.Admin.failedAssertions
377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393
							}
						more | nE+1<fails
							= analyse rest (nTests-1) (nArgs-1) nRej nUnd (nE+1) [counterExample: counterExamples] (admin res.labels labels)
							= [GE_TestFinished
								(testname p)
								{ maxTests   = maxTests
								, nRej       = nRej
								, resultType = CounterExpls (nTests - 1) nUnd (nE + 1)
								}
								[counterExample: counterExamples]
								(admin res.labels labels)]
					Rej   -> analyse rest nTests (nArgs-1) (nRej+1) nUnd     nE counterExamples labels
					Undef -> analyse rest nTests (nArgs-1) nRej     (nUnd+1) nE counterExamples labels
					_     -> abort "Error in Gast: analyse; missing case for result\n"
				]

	// there should always be a result for empty result lists!
394 395 396
	analyse` :: ![.Admin] !Int !Int !Int !Int !Int -> Maybe ResultType
	analyse` [] ntests nargs nrej 0    0  = Just $ Proof ntests
	analyse` [] ntests nargs nrej nund 0
397 398
	| ntests==maxTests                    = Just $ Undefined nund
	| otherwise                           = Just $ PassedTest maxArgs ntests nund True
399 400 401
	analyse` [] ntests nargs nrej nund ne = Just $ CounterExpls ntests nund ne
	analyse` _  0      nargs nrej nund 0  = Just $ PassedTest maxArgs 0 nund False
	analyse` _  0      nargs nrej nund ne = Just $ CounterExpls 0 nund ne
402 403 404
	analyse` _  ntests 0     nrej nund 0
	| ntests == maxTests                  = Just $ NoTests maxArgs ntests nund
	| otherwise                           = Just $ PassedTest maxArgs ntests nund False
405
	analyse` _  ntests 0     nrej nund ne = Just $ CounterExpls ntests nund ne
406
	analyse` _  _      _     _    _    _  = Nothing
Bas Lijnse's avatar
Bas Lijnse committed
407 408 409 410 411 412 413 414 415 416 417

	admin :: ![String] ![(String,Int)] -> [(String,Int)]
	admin [] accu = accu
	admin [label:rest] accu = admin rest (insert label accu)

	insert :: !String ![(String,Int)] -> [(String,Int)]
	insert label [] = [(label,1)]
	insert label [this=:(old,n):rest]
	 | label==old
		= [(old,n+1):rest]
		= [this:insert label rest]