StdProperty.icl 7.78 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
Camil Staps's avatar
Camil Staps committed
21
import Text.GenJSON
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{|*|}, JSONEncode{|*|} a & genShow{|*|}, JSONEncode{|*|} 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{|*|}, JSONEncode{|*|} 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
affirm :: !(a b->Bool) !Relation a b .GenState !.Admin -> [Admin] | genShow{|*|}, JSONEncode{|*|} a & genShow{|*|}, JSONEncode{|*|} b
170
affirm op rel x y rs admin
171 172 173 174 175 176 177 178 179 180 181 182
    | 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
                             ]
        }
183

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

classify :: !Bool l !p -> Property | Testable p & genShow{|*|} l
classify c l p
Camil Staps's avatar
Camil Staps committed
195 196
	| 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
197 198

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

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

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

Bas Lijnse's avatar
Bas Lijnse committed
207 208 209 210 211 212 213 214 215 216 217
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
218
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
219 220 221 222 223

approxEqual :: !a !a !a -> Property | abs, Ord, -, genShow{|*|}, JSONEncode{|*|} a
approxEqual err x y = Prop "approximately equals"
                           (affirm (\x y -> abs (x - y) <= err)
                           (Other $ concat ["approximately equals (error = ", toString $ toJSON err, ")"]) x y)