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

/*
	GAST: A Generic Automatic Software Test-system
	
6
	stdProperty: opertors on logical properties
Bas Lijnse's avatar
Bas Lijnse committed
7 8 9 10 11 12 13

	Pieter Koopman, 2004..2008
	Radboud Universty, Nijmegen
	The Netherlands
	pieter@cs.ru.nl
*/

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

import Data.Func
Bas Lijnse's avatar
Bas Lijnse committed
17
from Math.Random import genRandInt
18
import System.OS
Camil Staps's avatar
Camil Staps committed
19 20 21 22 23 24
import Testing.TestEvents
import Text
import Text.JSON

import Gast.Testable
import Gast.ThunkNames
Bas Lijnse's avatar
Bas Lijnse committed
25 26 27 28

instance ==> Bool
where
	(==>) c p
Camil Staps's avatar
Camil Staps committed
29 30
		| c	= Prop ("Bool ==> " +++ testname p) (evaluate p)
			= Prop ("Bool ==> " +++ testname p) (\rs r = [{r & res = Rej}])
Bas Lijnse's avatar
Bas Lijnse committed
31 32 33

instance ==> Property
where
Camil Staps's avatar
Camil Staps committed
34
	(==>) c=:(Prop n _) p = Prop (n +++ " ==> " +++ testname p) imp
Bas Lijnse's avatar
Bas Lijnse committed
35 36 37 38 39 40 41 42 43 44
	where
		imp rs r
		# r1 = testAnalysis r (evaluate c rs r)
		= case  r1.res of
			OK	= evaluate p rs r1
				= [{r & res = Rej}]

class (\/) infixr 2 a b	:: !a b -> Property	//	Conditional or  of arg1 and arg2
class (/\) infixr 3	a b :: !a b -> Property	//	Conditional and of arg1 and arg2

Camil Staps's avatar
Camil Staps committed
45
instance /\ Bool     Bool      where (/\) x y = prop x /\ prop y
Bas Lijnse's avatar
Bas Lijnse committed
46 47 48
instance /\ Property Bool      where (/\) x y = x /\ prop y
instance /\ Bool     Property  where (/\) x y = prop x /\ y
instance /\ Property Property
Camil Staps's avatar
Camil Staps committed
49
where (/\) x y = Prop ("(" +++ testname x +++ " /\\ " +++ testname y +++ ")") (and x y)
Bas Lijnse's avatar
Bas Lijnse committed
50
	  where
51 52 53
		and x y genState r 
			# r1 = testAnalysis r (evaluate x genState r)
			  r2 = testAnalysis r (evaluate y genState r)
Bas Lijnse's avatar
Bas Lijnse committed
54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81
			= case (r1.res,r2.res) of // collect labels  !! 
				(CE   ,_    )	= [r1] // to fix the evaluation order
				(_    ,CE   )	= [r2]
				(Undef,_    )	= [r2]
				(Rej  ,OK   )	= [r2]
								= [r1]
/*
				(OK   ,OK   )	= [r1]
				(OK   ,Rej  )	= [r1]
				(OK   ,Undef)	= [r1]
				(OK   ,CE   )	= [r2]
				(Rej  ,OK   )	= [r2]
				(Rej  ,Rej  )	= [r1]
				(Rej  ,Undef)	= [r1]
				(Pass ,CE   )	= [r2]
				(Pass ,OK   )	= [r1]
				(Pass ,Rej  )	= [r1]
				(Pass ,Undef)	= [r1]
				(Pass ,CE   )	= [r2]
				(Undef,OK   )	= [r2]
				(Undef,Rej  )	= [r2]
				(Undef,Undef)	= [r2]
				(Undef,CE   )	= [r2]
				(CE   ,OK   )	= [r1]
				(CE   ,Rej  )	= [r1]
				(CE   ,Undef)	= [r1]
				(CE   ,CE   )	= [r1]
*/
Camil Staps's avatar
Camil Staps committed
82
instance \/ Bool     Bool      where (\/) x y = prop x \/ prop y
Bas Lijnse's avatar
Bas Lijnse committed
83 84 85
instance \/ Property Bool      where (\/) x y = x \/ prop y
instance \/ Bool     Property  where (\/) x y = prop x \/ y
instance \/ Property Property
86
where
Camil Staps's avatar
Camil Staps committed
87
    (\/) x y = Prop ("(" +++ testname x +++ " \\/ " +++ testname y +++ ")") (or x y)
88 89 90 91
    where
        or x y genState r = case testAnalysis r (evaluate x genState r) of
            r=:{res=OK}   -> [r]
            r=:{res=Pass} -> case testAnalysis r (evaluate y genState r) of
Bas Lijnse's avatar
Bas Lijnse committed
92 93
									r2=:{res=OK} = [r2]
												 = [r]
94
            r             -> evaluate y genState r
Bas Lijnse's avatar
Bas Lijnse committed
95

96
(<==>) infix 1 :: !a !b -> Property	| Testable a & Testable b		//	True if properties are equivalent
Bas Lijnse's avatar
Bas Lijnse committed
97
(<==>) p q 
98 99 100
		# r  = newAdmin
		  b  = testAnalysis r (evaluate p genState r)
		  c  = testAnalysis r (evaluate q genState r)
Bas Lijnse's avatar
Bas Lijnse committed
101 102 103 104 105 106
		= prop (b.res == c.res) // can this be improved?

(===>) infix 1 :: Bool Bool -> Bool
(===>) p q = (not p) || q 

ExistsIn :: (x->p) [x] -> Property | Testable p & TestArg x
Camil Staps's avatar
Camil Staps committed
107
ExistsIn f l = Prop ("ExistsIn " +++ thunk_name_to_string f +++ " " +++ thunk_name_to_string l) p
Bas Lijnse's avatar
Bas Lijnse committed
108 109 110
where p rs r = [exists r [testAnalysis r (evaluate (f a) rs r)\\a <- l] MaxExists]

Exists :: (x->p) -> Property | Testable p & TestArg x
Camil Staps's avatar
Camil Staps committed
111
Exists f = Prop ("Exists " +++ thunk_name_to_string f) p
112 113 114 115 116 117 118 119 120
where
    p genState r =
        [ exists
            r
            [ testAnalysis r (evaluate (f a) genState r)
            \\ a <- generateAll {GenState| genState & recFieldValueNrLimits = r.Admin.recFieldValueNrLimits}
            ]
            MaxExists
        ]
Bas Lijnse's avatar
Bas Lijnse committed
121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151
exists r []				n = {r & res = CE}
exists r _				0 = {r & res = Undef}
exists _ [r=:{res}:x]	n = case res of
								OK	= r
								Pass	= r
										= exists r x (n-1)

noCE r []              n = {r & res = OK}
noCE r _               0 = {r & res = Pass}
noCE _ [r=:{res=CE}:x] n = r
noCE _ [r=:{res=OK}:x] n = noCE {r&res=Pass} x (n-1)
noCE r [_:x]           n = noCE r x (n-1)

testAnalysis :: Admin [Admin] -> Admin // maakt van een lijst resultaten een enkel resultaat
testAnalysis r l = analysis l MaxExists Undef OK
where
	analysis []    n min max = {r & res = max}
	analysis _     0 min max = {r & res = min}
	analysis [s:x] n min max
	 = case s.res of
		CE		= s
		OK		= analysis x (n-1) Pass max
		Pass	= analysis x (n-1) Pass Pass
		Undef	= analysis x (n-1) min  max
		Rej		= case min of
					OK  	= analysis x (n-1) OK   max
					Pass	= analysis x (n-1) Pass max
							= analysis x (n-1) Rej  max
				= abort "Unknow result in testAnalysis"

ForAll :: !(x->p) -> Property | Testable p & TestArg x
Camil Staps's avatar
Camil Staps committed
152
ForAll f = Prop ("ForAll " +++ thunk_name_to_string f) (evaluate f)
Bas Lijnse's avatar
Bas Lijnse committed
153 154

ForEach :: ![x] !(x->p) -> Property | Testable p & TestArg x
Camil Staps's avatar
Camil Staps committed
155
ForEach list f = Prop ("ForEach " +++ thunk_name_to_string list +++ " " +++ thunk_name_to_string f) (forAll f list)
Bas Lijnse's avatar
Bas Lijnse committed
156 157 158 159

(For) infixl 0 :: !(x->p) ![x] -> Property | Testable p & TestArg x
(For) p list = ForEach list p

160
check :: !(a b -> Bool) !a !b -> Property | genShow{|*|}, JSONEncode{|*|} a & genShow{|*|}, JSONEncode{|*|} b
Camil Staps's avatar
Camil Staps committed
161
check op x y = Prop ("check " +++ thunk_name_to_string op) (affirm op (Other relName) x y)
162 163
where
    relName = concat [thunk_name_to_string op, "{", thunk_to_module_name_string op, "}"]
Bas Lijnse's avatar
Bas Lijnse committed
164

165
(=.=) infix 4 :: !a !a -> Property | Eq, genShow{|*|}, JSONEncode{|*|} a
Camil Staps's avatar
Camil Staps committed
166
(=.=) x y = Prop "=.=" (affirm (==) Eq x y)
Bas Lijnse's avatar
Bas Lijnse committed
167

168
affirm :: !(a b->Bool) !Relation a b .GenState !.Admin -> [Admin] | genShow{|*|}, JSONEncode{|*|} a & genShow{|*|}, JSONEncode{|*|} b
169
affirm op rel x y rs admin
170 171 172 173 174 175 176 177 178 179 180 181
    | op x y = evaluate True rs admin
    | otherwise = evaluate
        False
        rs
        { Admin | admin
        & failedAssertions = [ ( ExpectedRelation (toJSON x) rel (toJSON y)
                               , concat $ genShow{|*|} "" False x []
                               , concat $ genShow{|*|} "" False y []
                               )
                             : admin.Admin.failedAssertions
                             ]
        }
182

Bas Lijnse's avatar
Bas Lijnse committed
183
(ForAndGen) infixl 0 :: !(x->p) ![x] -> Property | Testable p & TestArg x
Camil Staps's avatar
Camil Staps committed
184
(ForAndGen) p list = Prop (thunk_name_to_string p +++ " ForAndGen " +++ thunk_name_to_string list) (evaluate p)
185 186 187 188 189 190
where
    evaluate f rs result =
        forAll f
               (list++generateAll {GenState| genState & recFieldValueNrLimits = result.Admin.recFieldValueNrLimits})
               rs
               result
Bas Lijnse's avatar
Bas Lijnse committed
191 192 193

classify :: !Bool l !p -> Property | Testable p & genShow{|*|} l
classify c l p
Camil Staps's avatar
Camil Staps committed
194 195
	| c	= Prop (testname p) (\rs r = evaluate p rs {r & labels = [show1 l:r.labels]})
		= Prop (testname p) (evaluate p)
Bas Lijnse's avatar
Bas Lijnse committed
196 197

label ::  !l !p -> Property | Testable p & genShow{|*|} l
Camil Staps's avatar
Camil Staps committed
198
label l p = Prop (testname p) (\rs r = evaluate p rs {r & labels = [show1 l:r.labels]})
Bas Lijnse's avatar
Bas Lijnse committed
199

200
name :: !n !p -> Property | Testable p & toString n
201
name n p = Prop (toString n) (\rs r -> evaluate p rs {r & namePath=[toString n:r.namePath]})
Bas Lijnse's avatar
Bas Lijnse committed
202

203
limitNrOfRecFieldValues :: !(Map (TypeName, RecFieldName) Int) !p -> Property | Testable p
Camil Staps's avatar
Camil Staps committed
204
limitNrOfRecFieldValues limits p = Prop (testname p) (\rs r = evaluate p rs {Admin| r & recFieldValueNrLimits = limits})
205

Bas Lijnse's avatar
Bas Lijnse committed
206 207 208 209 210 211 212 213 214 215 216
instance ~ Bool where ~ b = not b

instance ~ Result
where
	~ CE = OK
	~ OK = CE
	~ Pass = CE
	~ Rej = Rej
	~ Undef = Undef

instance ~ Property
Camil Staps's avatar
Camil Staps committed
217
where ~ (Prop n p) = Prop ("~" +++ n) (\rs r = let r` = testAnalysis r (p rs r) in [{r` & res = ~r`.res}])