StdProperty.icl 8.22 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
import Testing.TestEvents
import Text
21
import Text.GenPrint
Camil Staps's avatar
Camil Staps committed
22 23 24

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{|*|}, gPrint{|*|} a & genShow{|*|}, gPrint{|*|} b
Camil Staps's avatar
Camil Staps committed
161
check op x y = Prop name (\gs a -> affirm op (Other relName) x y gs {a & namePath=[name:a.namePath]})
162
where
Camil Staps's avatar
Camil Staps committed
163 164
	name = thunk_name_to_string op
	relName = concat [name, "{", thunk_to_module_name_string op, "}"]
Bas Lijnse's avatar
Bas Lijnse committed
165

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

169
(<.)  infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
170 171
(<.) x y = Prop "<." (affirm (<) Lt x y)

172
(<=.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
173 174
(<=.) x y = Prop "<=." (affirm (<=) Le x y)

175
(>.)  infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
176 177
(>.) x y = Prop ">." (affirm (>) Gt x y)

178
(>=.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
179 180
(>=.) x y = Prop ">=." (affirm (>=) Ge x y)

181
affirm :: !(a b->Bool) !Relation a b .GenState !.Admin -> [Admin] | genShow{|*|}, gPrint{|*|} a & genShow{|*|}, gPrint{|*|} b
182
affirm op rel x y rs admin
183 184 185 186 187
    | op x y = evaluate True rs admin
    | otherwise = evaluate
        False
        rs
        { Admin | admin
188
        & failedAssertions = [ ( ExpectedRelation (printToString x) rel (printToString y)
189 190 191 192 193 194
                               , concat $ genShow{|*|} "" False x []
                               , concat $ genShow{|*|} "" False y []
                               )
                             : admin.Admin.failedAssertions
                             ]
        }
195

Bas Lijnse's avatar
Bas Lijnse committed
196
(ForAndGen) infixl 0 :: !(x->p) ![x] -> Property | Testable p & TestArg x
Camil Staps's avatar
Camil Staps committed
197
(ForAndGen) p list = Prop (thunk_name_to_string p +++ " ForAndGen " +++ thunk_name_to_string list) (evaluate p)
198 199 200 201 202 203
where
    evaluate f rs result =
        forAll f
               (list++generateAll {GenState| genState & recFieldValueNrLimits = result.Admin.recFieldValueNrLimits})
               rs
               result
Bas Lijnse's avatar
Bas Lijnse committed
204 205 206

classify :: !Bool l !p -> Property | Testable p & genShow{|*|} l
classify c l p
Camil Staps's avatar
Camil Staps committed
207 208
	| 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
209 210

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

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

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

Bas Lijnse's avatar
Bas Lijnse committed
219 220 221 222 223 224 225 226 227 228 229
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
230
where ~ (Prop n p) = Prop ("~" +++ n) (\rs r = let r` = testAnalysis r (p rs r) in [{r` & res = ~r`.res}])
Steffen Michels's avatar
Steffen Michels committed
231

232
approxEqual :: !a !a !a -> Property | abs, Ord, -, genShow{|*|}, gPrint{|*|} a
Steffen Michels's avatar
Steffen Michels committed
233 234
approxEqual err x y = Prop "approximately equals"
                           (affirm (\x y -> abs (x - y) <= err)
235
                           (Other $ concat ["approximately equals (error = ", printToString err, ")"]) x y)