StdProperty.icl 8.65 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
import StdEnv
Camil Staps's avatar
Camil Staps committed
15
import StdMaybe
Camil Staps's avatar
Camil Staps committed
16 17

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

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

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

instance ==> Property
where
Camil Staps's avatar
Camil Staps committed
35
	(==>) c=:(Prop n _ _) p = Prop (n +++ " ==> " +++ testname p) (testlocation p) imp
Bas Lijnse's avatar
Bas Lijnse committed
36 37 38 39 40 41 42 43 44 45
	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
46
instance /\ Bool     Bool      where (/\) x y = prop x /\ prop y
Bas Lijnse's avatar
Bas Lijnse committed
47 48 49
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
50
where (/\) x y = Prop ("(" +++ testname x +++ " /\\ " +++ testname y +++ ")") Nothing (and x y)
Bas Lijnse's avatar
Bas Lijnse committed
51
	  where
52 53 54
		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
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 82
			= 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
83
instance \/ Bool     Bool      where (\/) x y = prop x \/ prop y
Bas Lijnse's avatar
Bas Lijnse committed
84 85 86
instance \/ Property Bool      where (\/) x y = x \/ prop y
instance \/ Bool     Property  where (\/) x y = prop x \/ y
instance \/ Property Property
87
where
Camil Staps's avatar
Camil Staps committed
88
    (\/) x y = Prop ("(" +++ testname x +++ " \\/ " +++ testname y +++ ")") Nothing (or x y)
89 90 91 92
    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
93 94
									r2=:{res=OK} = [r2]
												 = [r]
95
            r             -> evaluate y genState r
Bas Lijnse's avatar
Bas Lijnse committed
96

97
(<==>) infix 1 :: !a !b -> Property	| Testable a & Testable b		//	True if properties are equivalent
Bas Lijnse's avatar
Bas Lijnse committed
98
(<==>) p q 
99 100 101
		# r  = newAdmin
		  b  = testAnalysis r (evaluate p genState r)
		  c  = testAnalysis r (evaluate q genState r)
Bas Lijnse's avatar
Bas Lijnse committed
102 103 104 105 106 107
		= 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
108
ExistsIn f l = Prop ("ExistsIn " +++ thunk_name_to_string f +++ " " +++ thunk_name_to_string l) Nothing p
Bas Lijnse's avatar
Bas Lijnse committed
109 110 111
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
112
Exists f = Prop ("Exists " +++ thunk_name_to_string f) Nothing p
113 114 115 116 117 118 119 120 121
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
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 152
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
153
ForAll f = Prop ("ForAll " +++ thunk_name_to_string f) Nothing (evaluate f)
Bas Lijnse's avatar
Bas Lijnse committed
154 155

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

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

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

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

170
(<.)  infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
Camil Staps's avatar
Camil Staps committed
171
(<.) x y = Prop "<." Nothing (affirm (<) Lt x y)
172

173
(<=.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
Camil Staps's avatar
Camil Staps committed
174
(<=.) x y = Prop "<=." Nothing (affirm (<=) Le x y)
175

176
(>.)  infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
Camil Staps's avatar
Camil Staps committed
177
(>.) x y = Prop ">." Nothing (affirm (>) Gt x y)
178

179
(>=.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
Camil Staps's avatar
Camil Staps committed
180
(>=.) x y = Prop ">=." Nothing (affirm (>=) Ge x y)
181

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

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

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

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

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

Camil Staps's avatar
Camil Staps committed
217 218
location_and_name :: !TestLocation !n !p -> Property | Testable p & toString n
location_and_name l n p = Prop (toString n) (Just l) \rs r -> evaluate p rs {r & namePath=[toString n:r.namePath]}
Bas Lijnse's avatar
Bas Lijnse committed
219

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

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

236
approxEqual :: !a !a !a -> Property | abs, Ord, -, genShow{|*|}, gPrint{|*|} a
Camil Staps's avatar
Camil Staps committed
237
approxEqual err x y = Prop "approximately equals" Nothing
Steffen Michels's avatar
Steffen Michels committed
238
                           (affirm (\x y -> abs (x - y) <= err)
239
                           (Other $ concat ["approximately equals (error = ", printToString err, ")"]) x y)