StdProperty.icl 7.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
Bas Lijnse's avatar
Bas Lijnse committed
15 16 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
from Math.Random import genRandInt

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

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

159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178
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
179 180
(ForAndGen) infixl 0 :: !(x->p) ![x] -> Property | Testable p & TestArg x
(ForAndGen) p list = Prop (evaluate p)
181
where evaluate f rs result = forAll f (list++generateAll genState) rs result
Bas Lijnse's avatar
Bas Lijnse committed
182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206

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

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

thunk_to_module_name_pointer :: !(a a->Bool) -> Int;
thunk_to_module_name_pointer a = code {
    pushD_a 0
    pop_a 1
    push_b 0
    load_si16 0
    addI
    load_i 6
237 238
    pushI 4294967295
    and%
239 240 241 242 243 244 245 246 247 248 249 250 251
}

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

get_module_name_size :: !Int -> Int;
get_module_name_size a = code {
    load_i 0
252 253
    pushI 4294967295
    and%
254 255 256 257 258 259 260
}

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