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
*/

14
import Gast.Testable, StdEnv, Testing.TestEvents, Text.JSON, Text, Data.Func
Bas Lijnse's avatar
Bas Lijnse committed
15
from Math.Random import genRandInt
16
import System.OS
Bas Lijnse's avatar
Bas Lijnse committed
17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42

instance ==> Bool
where
	(==>) c p
		| c	= Prop (evaluate p)
			= Prop (\rs r = [{r & res = Rej}])

instance ==> Property
where
	(==>) c p = Prop imp
	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

instance /\ Bool     Bool      where (/\) x y = prop (x && y)
instance /\ Property Bool      where (/\) x y = x /\ prop y
instance /\ Bool     Property  where (/\) x y = prop x /\ y
instance /\ Property Property
where (/\) x y = Prop (and x y)
	  where
43 44 45
		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
46 47 48 49 50 51 52 53 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
			= 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]
*/
instance \/ Bool     Bool      where (\/) x y = prop (x || y)
instance \/ Property Bool      where (\/) x y = x \/ prop y
instance \/ Bool     Property  where (\/) x y = prop x \/ y
instance \/ Property Property
where (\/) x y = Prop (or x y)
	  where
80 81
		or x y genState r 
			= case testAnalysis r (evaluate x genState r) of
Bas Lijnse's avatar
Bas Lijnse committed
82
				r=:{res=OK}		= [r]
83
				r=:{res=Pass}	= case testAnalysis r (evaluate y genState r) of
Bas Lijnse's avatar
Bas Lijnse committed
84 85
									r2=:{res=OK} = [r2]
												 = [r]
86
								= evaluate y genState r
Bas Lijnse's avatar
Bas Lijnse committed
87

88
(<==>) infix 1 :: !a !b -> Property	| Testable a & Testable b		//	True if properties are equivalent
Bas Lijnse's avatar
Bas Lijnse committed
89
(<==>) p q 
90 91 92
		# r  = newAdmin
		  b  = testAnalysis r (evaluate p genState r)
		  c  = testAnalysis r (evaluate q genState r)
Bas Lijnse's avatar
Bas Lijnse committed
93 94 95 96 97 98 99 100 101 102 103
		= 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
ExistsIn f l = Prop p
where p rs r = [exists r [testAnalysis r (evaluate (f a) rs r)\\a <- l] MaxExists]

Exists :: (x->p) -> Property | Testable p & TestArg x
Exists f = Prop p
104 105 106 107 108 109 110 111 112
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
113 114 115 116 117 118 119 120 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
ForAll f = Prop (evaluate f)

ForEach :: ![x] !(x->p) -> Property | Testable p & TestArg x
ForEach list f = Prop (forAll f list)

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

152 153 154 155
check :: !(a a -> Bool) !a !a -> Property | genShow{|*|}, JSONEncode{|*|} a
check op x y = Prop (affirm op (Other relName) x y)
where
    relName = concat [thunk_name_to_string op, "{", thunk_to_module_name_string op, "}"]
Bas Lijnse's avatar
Bas Lijnse committed
156

157
(=.=) infix 4 :: !a !a -> Property | Eq, genShow{|*|}, JSONEncode{|*|} a
158
(=.=) x y = Prop (affirm (==) Eq x y)
Bas Lijnse's avatar
Bas Lijnse committed
159

160 161
affirm :: !(a a->Bool) !Relation a a .GenState !.Admin -> [Admin] | genShow{|*|}, JSONEncode{|*|} a
affirm op rel x y rs admin
162 163 164 165 166 167 168 169 170 171 172 173
    | 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
                             ]
        }
174

Bas Lijnse's avatar
Bas Lijnse committed
175 176
(ForAndGen) infixl 0 :: !(x->p) ![x] -> Property | Testable p & TestArg x
(ForAndGen) p list = Prop (evaluate p)
177 178 179 180 181 182
where
    evaluate f rs result =
        forAll f
               (list++generateAll {GenState| genState & recFieldValueNrLimits = result.Admin.recFieldValueNrLimits})
               rs
               result
Bas Lijnse's avatar
Bas Lijnse committed
183 184 185 186 187 188 189 190 191

classify :: !Bool l !p -> Property | Testable p & genShow{|*|} l
classify c l p
	| c	= Prop (\rs r = evaluate p rs {r & labels = [show1 l:r.labels]})
		= Prop (evaluate p)

label ::  !l !p -> Property | Testable p & genShow{|*|} l
label l p = Prop (\rs r = evaluate p rs {r & labels = [show1 l:r.labels]})

192
name :: !n !p -> Property | Testable p & toString n
193
name n p = Prop (\rs r = evaluate p rs {Admin| r & name = [toString n:r.Admin.name]})
Bas Lijnse's avatar
Bas Lijnse committed
194

195 196 197
limitNrOfRecFieldValues :: !(Map (TypeName, RecFieldName) Int) !p -> Property | Testable p
limitNrOfRecFieldValues limits p = Prop (\rs r = evaluate p rs {Admin| r & recFieldValueNrLimits = limits})

Bas Lijnse's avatar
Bas Lijnse committed
198 199 200 201 202 203 204 205 206 207 208 209 210
instance ~ Bool where ~ b = not b

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

instance ~ Property
where ~ (Prop p) = Prop (\rs r = let r` = testAnalysis r (p rs r) in [{r` & res = ~r`.res}])

211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232
// ================================================================
// :( :( dirty low level hacking to obtain names of functions :( :(

thunk_name_to_string1 :: !(a->Bool) -> {#Char}
thunk_name_to_string1 a = code {
    pushD_a 0
    pop_a 1
    .d 0 1 i
        jsr DtoAC
    .o 1 0
}


thunk_name_to_string :: !(a a->Bool) -> {#Char}
thunk_name_to_string a = code {
    pushD_a 0
    pop_a 1
    .d 0 1 i
        jsr DtoAC
    .o 1 0
}

233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268
thunk_to_module_name_pointer :: ((a a->Bool) -> Int)
thunk_to_module_name_pointer = IF_MAC v64mac (IF_INT_64_OR_32 v64 v32)
where
	v32 :: !(a a -> Bool) -> Int
	v32 _ = code {
		pushD_a 0
		pop_a 1
		push_b 0
		load_si16 0
		addI
		load_i 6
	}

	v64 :: !(a a -> Bool) -> Int
	v64 _ = code {
		pushD_a 0
		pop_a 1
		push_b 0
		load_si16 0
		addI
		load_si32 6
	}

	v64mac :: !(a a -> Bool) -> Int
	v64mac _ = code {
		pushD_a 0
		pop_a 1
		push_b 0
		load_si16 0
		addI
		push_b 0
		load_si32 6
		addI
		pushI 6
		addI
	}
269 270 271 272 273 274 275 276 277

thunk_to_module_name_string :: !(a a->Bool) -> {#Char};
thunk_to_module_name_string a
    = get_module_name (thunk_to_module_name_pointer a);

get_module_name :: !Int -> {#Char};
get_module_name m
    = {get_module_name_char m i\\i<-[0..get_module_name_size m-1]};

278 279 280 281 282 283 284 285 286 287 288 289
get_module_name_size :: (Int -> Int)
get_module_name_size = IF_INT_64_OR_32 v64 v32
where
	v32 :: !Int -> Int
	v32 _ = code {
		load_i 0
	}

	v64 :: !Int -> Int
	v64 _ = code {
		load_si32 0
	}
290 291 292 293 294 295

get_module_name_char :: !Int !Int -> Char;
get_module_name_char a i = code {
    addI
    load_ui8 4
}