StdProperty.icl 7.66 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
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 43 44

class (==>) infixr 1 b :: b p -> Property | Testable p

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
45 46 47
		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
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 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]
*/
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
82 83
		or x y genState r 
			= case testAnalysis r (evaluate x genState r) of
Bas Lijnse's avatar
Bas Lijnse committed
84
				r=:{res=OK}		= [r]
85
				r=:{res=Pass}	= case testAnalysis r (evaluate y genState r) of
Bas Lijnse's avatar
Bas Lijnse committed
86 87
									r2=:{res=OK} = [r2]
												 = [r]
88
								= evaluate y genState r
Bas Lijnse's avatar
Bas Lijnse committed
89

90
(<==>) infix 1 :: !a !b -> Property	| Testable a & Testable b		//	True if properties are equivalent
Bas Lijnse's avatar
Bas Lijnse committed
91
(<==>) p q 
92 93 94
		# r  = newAdmin
		  b  = testAnalysis r (evaluate p genState r)
		  c  = testAnalysis r (evaluate q genState r)
Bas Lijnse's avatar
Bas Lijnse committed
95 96 97 98 99 100 101 102 103 104 105
		= 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
106
where p genState r = [exists r [testAnalysis r (evaluate (f a) genState r)\\a <- generateAll genState] MaxExists]
Bas Lijnse's avatar
Bas Lijnse committed
107 108 109 110 111 112 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 152 153 154 155 156 157 158 159
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

// XXXXXXXXXXXXXXXXXXXXXXXXXX

class (VOOR) infixl 0 t :: (t a b) [a] -> [b]
instance VOOR (->)
where VOOR f l = map f l

:: PL a b = PL [a->b]
instance VOOR PL
where VOOR (PL fl) l = diagonal [map f l\\f<-fl] //[f x \\ f<-fl, x<-l]

//| Testable p & TestArg x

// XXXXXXXXXXXXXXXXXXXXXXXXXX

160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179
check :: (a a -> Bool) !a !a -> Property | genShow{|*|} a
check op x y = Prop (affirm op x y)

(=.=) infix 4 :: !a !a -> Property | Eq, genShow{|*|} a
(=.=) x y = check (==) x y

affirm :: (a a->Bool) a a .GenState !.Admin -> [Admin] | genShow{|*|} a
affirm op x y rs admin
	| op x y
		= evaluate True rs admin
		= evaluate False rs
			{admin
			& mes =	["\nnot ("
					:genShow{|*|} "" False x 
						[ " ", thunk_name_to_string op, "{",thunk_to_module_name_string op,"} "
						:	genShow{|*|} "" False y [")\n": admin.mes]
						]
					]
			}

Bas Lijnse's avatar
Bas Lijnse committed
180 181
(ForAndGen) infixl 0 :: !(x->p) ![x] -> Property | Testable p & TestArg x
(ForAndGen) p list = Prop (evaluate p)
182
where evaluate f rs result = forAll f (list++generateAll genState) rs result
Bas Lijnse's avatar
Bas Lijnse committed
183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207

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]})

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

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}])

208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229
// ================================================================
// :( :( 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
}

230 231 232 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
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
	}
266 267 268 269 270 271 272 273 274

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]};

275 276 277 278 279 280 281 282 283 284 285 286
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
	}
287 288 289 290 291 292

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