Commit ddbd445a authored by Camil Staps's avatar Camil Staps 🦆
Browse files

Merge branch 'notEq' into 'master'

add <.> operator

See merge request !32
parents 9f9d3c89 d431c3ed
Pipeline #34070 passed with stage
in 1 minute
...@@ -29,6 +29,7 @@ instance \/ Bool Property ...@@ -29,6 +29,7 @@ instance \/ Bool Property
instance \/ Property Property instance \/ Property Property
(=.=) infix 4 :: !a !a -> Property | Eq, genShow{|*|}, gPrint{|*|} a // shows values x and y if x == y yields False (=.=) infix 4 :: !a !a -> Property | Eq, genShow{|*|}, gPrint{|*|} a // shows values x and y if x == y yields False
(<.>) infix 4 :: !a !a -> Property | Eq, genShow{|*|}, gPrint{|*|} a // shows values x and y if x <> y yields False
(<.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a // shows values x and y if x < y yields False (<.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a // shows values x and y if x < y yields False
(<=.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a // shows values x and y if x <= y yields False (<=.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a // shows values x and y if x <= y yields False
(>.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a // shows values x and y if x > y yields False (>.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a // shows values x and y if x > y yields False
......
implementation module Gast.StdProperty implementation module Gast.StdProperty
/* /*
GAST: A Generic Automatic Software Test-system GAST: A Generic Automatic Software Test-system
stdProperty: opertors on logical properties stdProperty: opertors on logical properties
Pieter Koopman, 2004..2008 Pieter Koopman, 2004..2008
Radboud Universty, Nijmegen Radboud Universty, Nijmegen
The Netherlands The Netherlands
pieter@cs.ru.nl pieter@cs.ru.nl
*/ */
import StdEnv import StdEnv
import StdMaybe import StdMaybe
import Data.Func import Data.Func
from Math.Random import genRandInt from Math.Random import genRandInt
import System.OS import System.OS
import Testing.TestEvents import Testing.TestEvents
import Text import Text
import Text.GenPrint import Text.GenPrint
import Gast.Testable import Gast.Testable
import Gast.ThunkNames import Gast.ThunkNames
instance ==> Bool instance ==> Bool
where where
(==>) c p (==>) c p
| c = Prop ("Bool ==> " +++ testname p) (testlocation p) (evaluate p) | c = Prop ("Bool ==> " +++ testname p) (testlocation p) (evaluate p)
= Prop ("Bool ==> " +++ testname p) (testlocation p) (\rs r = [{r & res = Rej}]) = Prop ("Bool ==> " +++ testname p) (testlocation p) (\rs r = [{r & res = Rej}])
instance ==> Property instance ==> Property
where where
(==>) c=:(Prop n _ _) p = Prop (n +++ " ==> " +++ testname p) (testlocation p) imp (==>) c=:(Prop n _ _) p = Prop (n +++ " ==> " +++ testname p) (testlocation p) imp
where where
imp rs r imp rs r
# r1 = testAnalysis r (evaluate c rs r) # r1 = testAnalysis r (evaluate c rs r)
= case r1.res of = case r1.res of
OK = evaluate p rs r1 OK = evaluate p rs r1
= [{r & res = Rej}] = [{r & res = Rej}]
class (\/) infixr 2 a b :: !a b -> Property // Conditional or of arg1 and arg2 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 class (/\) infixr 3 a b :: !a b -> Property // Conditional and of arg1 and arg2
instance /\ Bool Bool where (/\) x y = prop x /\ prop y instance /\ Bool Bool where (/\) x y = prop x /\ prop y
instance /\ Property Bool where (/\) x y = x /\ prop y instance /\ Property Bool where (/\) x y = x /\ prop y
instance /\ Bool Property where (/\) x y = prop x /\ y instance /\ Bool Property where (/\) x y = prop x /\ y
instance /\ Property Property instance /\ Property Property
where (/\) x y = Prop ("(" +++ testname x +++ " /\\ " +++ testname y +++ ")") Nothing (and x y) where (/\) x y = Prop ("(" +++ testname x +++ " /\\ " +++ testname y +++ ")") Nothing (and x y)
where where
and x y genState r and x y genState r
# r1 = testAnalysis r (evaluate x genState r) # r1 = testAnalysis r (evaluate x genState r)
r2 = testAnalysis r (evaluate y genState r) r2 = testAnalysis r (evaluate y genState r)
= case (r1.res,r2.res) of // collect labels !! = case (r1.res,r2.res) of // collect labels !!
(CE ,_ ) = [r1] // to fix the evaluation order (CE ,_ ) = [r1] // to fix the evaluation order
(_ ,CE ) = [r2] (_ ,CE ) = [r2]
(Undef,_ ) = [r2] (Undef,_ ) = [r2]
(Rej ,OK ) = [r2] (Rej ,OK ) = [r2]
= [r1] = [r1]
/* /*
(OK ,OK ) = [r1] (OK ,OK ) = [r1]
(OK ,Rej ) = [r1] (OK ,Rej ) = [r1]
(OK ,Undef) = [r1] (OK ,Undef) = [r1]
(OK ,CE ) = [r2] (OK ,CE ) = [r2]
(Rej ,OK ) = [r2] (Rej ,OK ) = [r2]
(Rej ,Rej ) = [r1] (Rej ,Rej ) = [r1]
(Rej ,Undef) = [r1] (Rej ,Undef) = [r1]
(Pass ,CE ) = [r2] (Pass ,CE ) = [r2]
(Pass ,OK ) = [r1] (Pass ,OK ) = [r1]
(Pass ,Rej ) = [r1] (Pass ,Rej ) = [r1]
(Pass ,Undef) = [r1] (Pass ,Undef) = [r1]
(Pass ,CE ) = [r2] (Pass ,CE ) = [r2]
(Undef,OK ) = [r2] (Undef,OK ) = [r2]
(Undef,Rej ) = [r2] (Undef,Rej ) = [r2]
(Undef,Undef) = [r2] (Undef,Undef) = [r2]
(Undef,CE ) = [r2] (Undef,CE ) = [r2]
(CE ,OK ) = [r1] (CE ,OK ) = [r1]
(CE ,Rej ) = [r1] (CE ,Rej ) = [r1]
(CE ,Undef) = [r1] (CE ,Undef) = [r1]
(CE ,CE ) = [r1] (CE ,CE ) = [r1]
*/ */
instance \/ Bool Bool where (\/) x y = prop x \/ prop y instance \/ Bool Bool where (\/) x y = prop x \/ prop y
instance \/ Property Bool where (\/) x y = x \/ prop y instance \/ Property Bool where (\/) x y = x \/ prop y
instance \/ Bool Property where (\/) x y = prop x \/ y instance \/ Bool Property where (\/) x y = prop x \/ y
instance \/ Property Property instance \/ Property Property
where where
(\/) x y = Prop ("(" +++ testname x +++ " \\/ " +++ testname y +++ ")") Nothing (or x y) (\/) x y = Prop ("(" +++ testname x +++ " \\/ " +++ testname y +++ ")") Nothing (or x y)
where where
or x y genState r = case testAnalysis r (evaluate x genState r) of or x y genState r = case testAnalysis r (evaluate x genState r) of
r=:{res=OK} -> [r] r=:{res=OK} -> [r]
r=:{res=Pass} -> case testAnalysis r (evaluate y genState r) of r=:{res=Pass} -> case testAnalysis r (evaluate y genState r) of
r2=:{res=OK} = [r2] r2=:{res=OK} = [r2]
= [r] = [r]
r -> evaluate y genState r r -> evaluate y genState r
(<==>) infix 1 :: !a !b -> Property | Testable a & Testable b // True if properties are equivalent (<==>) infix 1 :: !a !b -> Property | Testable a & Testable b // True if properties are equivalent
(<==>) p q (<==>) p q
# r = newAdmin # r = newAdmin
b = testAnalysis r (evaluate p genState r) b = testAnalysis r (evaluate p genState r)
c = testAnalysis r (evaluate q genState r) c = testAnalysis r (evaluate q genState r)
= prop (b.res == c.res) // can this be improved? = prop (b.res == c.res) // can this be improved?
(===>) infix 1 :: Bool Bool -> Bool (===>) infix 1 :: Bool Bool -> Bool
(===>) p q = (not p) || q (===>) p q = (not p) || q
ExistsIn :: (x->p) [x] -> Property | Testable p & TestArg x ExistsIn :: (x->p) [x] -> Property | Testable p & TestArg x
ExistsIn f l = Prop ("ExistsIn " +++ thunk_name_to_string f +++ " " +++ thunk_name_to_string l) Nothing p ExistsIn f l = Prop ("ExistsIn " +++ thunk_name_to_string f +++ " " +++ thunk_name_to_string l) Nothing p
where p rs r = [exists r [testAnalysis r (evaluate (f a) rs r)\\a <- l] MaxExists] 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 :: (x->p) -> Property | Testable p & TestArg x
Exists f = Prop ("Exists " +++ thunk_name_to_string f) Nothing p Exists f = Prop ("Exists " +++ thunk_name_to_string f) Nothing p
where where
p genState r = p genState r =
[ exists [ exists
r r
[ testAnalysis r (evaluate (f a) genState r) [ testAnalysis r (evaluate (f a) genState r)
\\ a <- generateAll {GenState| genState & recFieldValueNrLimits = r.Admin.recFieldValueNrLimits} \\ a <- generateAll {GenState| genState & recFieldValueNrLimits = r.Admin.recFieldValueNrLimits}
] ]
MaxExists MaxExists
] ]
exists r [] n = {r & res = CE} exists r [] n = {r & res = CE}
exists r _ 0 = {r & res = Undef} exists r _ 0 = {r & res = Undef}
exists _ [r=:{res}:x] n = case res of exists _ [r=:{res}:x] n = case res of
OK = r OK = r
Pass = r Pass = r
= exists r x (n-1) = exists r x (n-1)
noCE r [] n = {r & res = OK} noCE r [] n = {r & res = OK}
noCE r _ 0 = {r & res = Pass} noCE r _ 0 = {r & res = Pass}
noCE _ [r=:{res=CE}:x] n = r noCE _ [r=:{res=CE}:x] n = r
noCE _ [r=:{res=OK}:x] n = noCE {r&res=Pass} x (n-1) noCE _ [r=:{res=OK}:x] n = noCE {r&res=Pass} x (n-1)
noCE r [_:x] n = noCE r 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 :: Admin [Admin] -> Admin // maakt van een lijst resultaten een enkel resultaat
testAnalysis r l = analysis l MaxExists Undef OK testAnalysis r l = analysis l MaxExists Undef OK
where where
analysis [] n min max = {r & res = max} analysis [] n min max = {r & res = max}
analysis _ 0 min max = {r & res = min} analysis _ 0 min max = {r & res = min}
analysis [s:x] n min max analysis [s:x] n min max
= case s.res of = case s.res of
CE = s CE = s
OK = analysis x (n-1) Pass max OK = analysis x (n-1) Pass max
Pass = analysis x (n-1) Pass Pass Pass = analysis x (n-1) Pass Pass
Undef = analysis x (n-1) min max Undef = analysis x (n-1) min max
Rej = case min of Rej = case min of
OK = analysis x (n-1) OK max OK = analysis x (n-1) OK max
Pass = analysis x (n-1) Pass max Pass = analysis x (n-1) Pass max
= analysis x (n-1) Rej max = analysis x (n-1) Rej max
= abort "Unknow result in testAnalysis" = abort "Unknow result in testAnalysis"
ForAll :: !(x->p) -> Property | Testable p & TestArg x ForAll :: !(x->p) -> Property | Testable p & TestArg x
ForAll f = Prop ("ForAll " +++ thunk_name_to_string f) Nothing (evaluate f) ForAll f = Prop ("ForAll " +++ thunk_name_to_string f) Nothing (evaluate f)
ForEach :: ![x] !(x->p) -> Property | Testable p & TestArg x ForEach :: ![x] !(x->p) -> Property | Testable p & TestArg x
ForEach list f = Prop ("ForEach " +++ thunk_name_to_string list +++ " " +++ thunk_name_to_string f) Nothing (forAll f list) ForEach list f = Prop ("ForEach " +++ thunk_name_to_string list +++ " " +++ thunk_name_to_string f) Nothing (forAll f list)
(For) infixl 0 :: !(x->p) ![x] -> Property | Testable p & TestArg x (For) infixl 0 :: !(x->p) ![x] -> Property | Testable p & TestArg x
(For) p list = ForEach list p (For) p list = ForEach list p
check :: !(a b -> Bool) !a !b -> Property | genShow{|*|}, gPrint{|*|} a & genShow{|*|}, gPrint{|*|} b check :: !(a b -> Bool) !a !b -> Property | genShow{|*|}, gPrint{|*|} a & genShow{|*|}, gPrint{|*|} b
check op x y = Prop name Nothing \gs a -> affirm op (Other relName) x y gs {a & namePath=[name:a.namePath]} check op x y = Prop name Nothing \gs a -> affirm op (Other relName) x y gs {a & namePath=[name:a.namePath]}
where where
name = thunk_name_to_string op name = thunk_name_to_string op
relName = concat [name, "{", thunk_to_module_name_string op, "}"] relName = concat [name, "{", thunk_to_module_name_string op, "}"]
(=.=) infix 4 :: !a !a -> Property | Eq, genShow{|*|}, gPrint{|*|} a (=.=) infix 4 :: !a !a -> Property | Eq, genShow{|*|}, gPrint{|*|} a
(=.=) x y = Prop "=.=" Nothing (affirm (==) Eq x y) (=.=) x y = Prop "=.=" Nothing (affirm (==) Eq x y)
(<.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a (<.>) infix 4 :: !a !a -> Property | Eq, genShow{|*|}, gPrint{|*|} a
(<.) x y = Prop "<." Nothing (affirm (<) Lt x y) (<.>) x y = Prop "<.>" Nothing (affirm (<>) Ne x y)
(<=.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a (<.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
(<=.) x y = Prop "<=." Nothing (affirm (<=) Le x y) (<.) x y = Prop "<." Nothing (affirm (<) Lt x y)
(>.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a (<=.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
(>.) x y = Prop ">." Nothing (affirm (>) Gt x y) (<=.) x y = Prop "<=." Nothing (affirm (<=) Le x y)
(>=.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a (>.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
(>=.) x y = Prop ">=." Nothing (affirm (>=) Ge x y) (>.) x y = Prop ">." Nothing (affirm (>) Gt x y)
affirm :: !(a b->Bool) !Relation a b .GenState !.Admin -> [Admin] | genShow{|*|}, gPrint{|*|} a & genShow{|*|}, gPrint{|*|} b (>=.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
affirm op rel x y rs admin (>=.) x y = Prop ">=." Nothing (affirm (>=) Ge x y)
| op x y = evaluate True rs admin
| otherwise = evaluate affirm :: !(a b->Bool) !Relation a b .GenState !.Admin -> [Admin] | genShow{|*|}, gPrint{|*|} a & genShow{|*|}, gPrint{|*|} b
False affirm op rel x y rs admin
rs | op x y = evaluate True rs admin
{ Admin | admin | otherwise = evaluate
& failedAssertions = [ ( ExpectedRelation (GPrint (printToString x)) rel (GPrint (printToString y)) False
, concat $ genShow{|*|} "" False x [] rs
, concat $ genShow{|*|} "" False y [] { Admin | admin
) & failedAssertions = [ ( ExpectedRelation (GPrint (printToString x)) rel (GPrint (printToString y))
: admin.Admin.failedAssertions , concat $ genShow{|*|} "" False x []
] , concat $ genShow{|*|} "" False y []
} )
: admin.Admin.failedAssertions
(ForAndGen) infixl 0 :: !(x->p) ![x] -> Property | Testable p & TestArg x ]
(ForAndGen) p list = Prop (thunk_name_to_string p +++ " ForAndGen " +++ thunk_name_to_string list) Nothing (evaluate p) }
where
evaluate f rs result = (ForAndGen) infixl 0 :: !(x->p) ![x] -> Property | Testable p & TestArg x
forAll f (ForAndGen) p list = Prop (thunk_name_to_string p +++ " ForAndGen " +++ thunk_name_to_string list) Nothing (evaluate p)
(list++generateAll {GenState| genState & recFieldValueNrLimits = result.Admin.recFieldValueNrLimits}) where
rs evaluate f rs result =
result forAll f
(list++generateAll {GenState| genState & recFieldValueNrLimits = result.Admin.recFieldValueNrLimits})
classify :: !Bool l !p -> Property | Testable p & genShow{|*|} l rs
classify c l p result
| c = Prop (testname p) Nothing (\rs r = evaluate p rs {r & labels = [show1 l:r.labels]})
= Prop (testname p) Nothing (evaluate p) classify :: !Bool l !p -> Property | Testable p & genShow{|*|} l
classify c l p
label :: !l !p -> Property | Testable p & genShow{|*|} l | c = Prop (testname p) Nothing (\rs r = evaluate p rs {r & labels = [show1 l:r.labels]})
label l p = Prop (testname p) Nothing (\rs r = evaluate p rs {r & labels = [show1 l:r.labels]}) = Prop (testname p) Nothing (evaluate p)
name :: !n !p -> Property | Testable p & toString n label :: !l !p -> Property | Testable p & genShow{|*|} l
name n p = Prop (toString n) Nothing (\rs r -> evaluate p rs {r & namePath=[toString n:r.namePath]}) label l p = Prop (testname p) Nothing (\rs r = evaluate p rs {r & labels = [show1 l:r.labels]})
location_and_name :: !TestLocation !n !p -> Property | Testable p & toString n name :: !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]} name n p = Prop (toString n) Nothing (\rs r -> evaluate p rs {r & namePath=[toString n:r.namePath]})
limitNrOfRecFieldValues :: !(Map (TypeName, RecFieldName) Int) !p -> Property | Testable p location_and_name :: !TestLocation !n !p -> Property | Testable p & toString n
limitNrOfRecFieldValues limits p = Prop (testname p) Nothing (\rs r = evaluate p rs {Admin| r & recFieldValueNrLimits = limits}) location_and_name l n p = Prop (toString n) (Just l) \rs r -> evaluate p rs {r & namePath=[toString n:r.namePath]}
instance ~ Bool where ~ b = not b limitNrOfRecFieldValues :: !(Map (TypeName, RecFieldName) Int) !p -> Property | Testable p
limitNrOfRecFieldValues limits p = Prop (testname p) Nothing (\rs r = evaluate p rs {Admin| r & recFieldValueNrLimits = limits})
instance ~ Result
where instance ~ Bool where ~ b = not b
~ CE = OK
~ OK = CE instance ~ Result
~ Pass = CE where
~ Rej = Rej ~ CE = OK
~ Undef = Undef ~ OK = CE
~ Pass = CE
instance ~ Property ~ Rej = Rej
where ~ (Prop n m p) = Prop ("~" +++ n) m (\rs r = let r` = testAnalysis r (p rs r) in [{r` & res = ~r`.res}]) ~ Undef = Undef
approxEqual :: !a !a !a -> Property | abs, Ord, -, genShow{|*|}, gPrint{|*|} a instance ~ Property
approxEqual err x y = Prop "approximately equals" Nothing where ~ (Prop n m p) = Prop ("~" +++ n) m (\rs r = let r` = testAnalysis r (p rs r) in [{r` & res = ~r`.res}])
(affirm (\x y -> abs (x - y) <= err)
(Other $ concat ["approximately equals (error = ", printToString err, ")"]) x y) approxEqual :: !a !a !a -> Property | abs, Ord, -, genShow{|*|}, gPrint{|*|} a
approxEqual err x y = Prop "approximately equals" Nothing
(affirm (\x y -> abs (x - y) <= err)
(Other $ concat ["approximately equals (error = ", printToString err, ")"]) x y)
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment