...
 
Commits (3)
......@@ -30,6 +30,7 @@ instance Testable (o1, o2, a) | Testable a
where
evaluate (_,_,p) g a = evaluate p g a
testname (_,_,p) = testname p
testlocation (_,_,p) = testlocation p
instance getOptions ([Testoption], a, b) where getOptions (opts,_,_) = opts
instance getPrintOptions (a, [PrintOption], b) where getPrintOptions (_,opts,_) = opts
......@@ -38,6 +39,7 @@ instance Testable ExposedProperty
where
evaluate (EP p) g a = evaluate p g a
testname (EP p) = testname p
testlocation (EP p) = testlocation p
instance getOptions ExposedProperty where getOptions (EP p) = getOptions p
......@@ -89,9 +91,9 @@ where
stream pc [ge:ges] io w
# io = foldl (\io ev -> snd $ fflush $ io <<< ev) io $ printEvents pc [ge]
# w = case ge of
GE_TestFinished _ {resultType=CounterExpls _ _ _} _ _ -> setReturnCode 1 w
GE_TestFinished _ {resultType=Undefined _} _ _ -> setReturnCode 1 w
_ -> w
GE_TestFinished _ _ {resultType=CounterExpls _ _ _} _ _ -> setReturnCode 1 w
GE_TestFinished _ _ {resultType=Undefined _} _ _ -> setReturnCode 1 w
_ -> w
= stream pc ges io w
stream _ [] io w = (io,w)
......
......@@ -13,7 +13,7 @@ definition module Gast.StdProperty
import Gast.GenLibTest
import Gast.Testable
from Testing.TestEvents import :: Relation
from Testing.TestEvents import :: TestLocation, :: Relation
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
......@@ -54,6 +54,7 @@ classify :: !Bool l !p -> Property | Testable p & genShow{|*|} l
label :: !l !p -> Property | Testable p & genShow{|*|} l
name :: !n !p -> Property | Testable p & toString n
location_and_name :: !TestLocation !n !p -> Property | Testable p & toString n
/**
* Assigns a name to a testable property.
......
......@@ -12,6 +12,7 @@ implementation module Gast.StdProperty
*/
import StdEnv
import StdMaybe
import Data.Func
from Math.Random import genRandInt
......@@ -26,12 +27,12 @@ import Gast.ThunkNames
instance ==> Bool
where
(==>) c p
| c = Prop ("Bool ==> " +++ testname p) (evaluate p)
= Prop ("Bool ==> " +++ testname p) (\rs r = [{r & res = Rej}])
| c = Prop ("Bool ==> " +++ testname p) (testlocation p) (evaluate p)
= Prop ("Bool ==> " +++ testname p) (testlocation p) (\rs r = [{r & res = Rej}])
instance ==> Property
where
(==>) c=:(Prop n _) p = Prop (n +++ " ==> " +++ testname p) imp
(==>) c=:(Prop n _ _) p = Prop (n +++ " ==> " +++ testname p) (testlocation p) imp
where
imp rs r
# r1 = testAnalysis r (evaluate c rs r)
......@@ -46,7 +47,7 @@ instance /\ Bool Bool where (/\) x y = prop x /\ prop 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 ("(" +++ testname x +++ " /\\ " +++ testname y +++ ")") (and x y)
where (/\) x y = Prop ("(" +++ testname x +++ " /\\ " +++ testname y +++ ")") Nothing (and x y)
where
and x y genState r
# r1 = testAnalysis r (evaluate x genState r)
......@@ -84,7 +85,7 @@ 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 ("(" +++ testname x +++ " \\/ " +++ testname y +++ ")") (or x y)
(\/) x y = Prop ("(" +++ testname x +++ " \\/ " +++ testname y +++ ")") Nothing (or x y)
where
or x y genState r = case testAnalysis r (evaluate x genState r) of
r=:{res=OK} -> [r]
......@@ -104,11 +105,11 @@ where
(===>) p q = (not p) || q
ExistsIn :: (x->p) [x] -> Property | Testable p & TestArg x
ExistsIn f l = Prop ("ExistsIn " +++ thunk_name_to_string f +++ " " +++ thunk_name_to_string l) 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]
Exists :: (x->p) -> Property | Testable p & TestArg x
Exists f = Prop ("Exists " +++ thunk_name_to_string f) p
Exists f = Prop ("Exists " +++ thunk_name_to_string f) Nothing p
where
p genState r =
[ exists
......@@ -149,34 +150,34 @@ where
= abort "Unknow result in testAnalysis"
ForAll :: !(x->p) -> Property | Testable p & TestArg x
ForAll f = Prop ("ForAll " +++ thunk_name_to_string f) (evaluate f)
ForAll f = Prop ("ForAll " +++ thunk_name_to_string f) Nothing (evaluate f)
ForEach :: ![x] !(x->p) -> Property | Testable p & TestArg x
ForEach list f = Prop ("ForEach " +++ thunk_name_to_string list +++ " " +++ thunk_name_to_string f) (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) p list = ForEach list p
check :: !(a b -> Bool) !a !b -> Property | genShow{|*|}, gPrint{|*|} a & genShow{|*|}, gPrint{|*|} b
check op x y = Prop name (\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
name = thunk_name_to_string op
relName = concat [name, "{", thunk_to_module_name_string op, "}"]
(=.=) infix 4 :: !a !a -> Property | Eq, genShow{|*|}, gPrint{|*|} a
(=.=) x y = Prop "=.=" (affirm (==) Eq x y)
(=.=) x y = Prop "=.=" Nothing (affirm (==) Eq x y)
(<.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
(<.) x y = Prop "<." (affirm (<) Lt x y)
(<.) x y = Prop "<." Nothing (affirm (<) Lt x y)
(<=.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
(<=.) x y = Prop "<=." (affirm (<=) Le x y)
(<=.) x y = Prop "<=." Nothing (affirm (<=) Le x y)
(>.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
(>.) x y = Prop ">." (affirm (>) Gt x y)
(>.) x y = Prop ">." Nothing (affirm (>) Gt x y)
(>=.) infix 4 :: !a !a -> Property | Ord, genShow{|*|}, gPrint{|*|} a
(>=.) x y = Prop ">=." (affirm (>=) Ge x y)
(>=.) x y = Prop ">=." Nothing (affirm (>=) Ge x y)
affirm :: !(a b->Bool) !Relation a b .GenState !.Admin -> [Admin] | genShow{|*|}, gPrint{|*|} a & genShow{|*|}, gPrint{|*|} b
affirm op rel x y rs admin
......@@ -194,7 +195,7 @@ affirm op rel x y rs admin
}
(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) (evaluate p)
(ForAndGen) p list = Prop (thunk_name_to_string p +++ " ForAndGen " +++ thunk_name_to_string list) Nothing (evaluate p)
where
evaluate f rs result =
forAll f
......@@ -204,17 +205,20 @@ where
classify :: !Bool l !p -> Property | Testable p & genShow{|*|} l
classify c l p
| c = Prop (testname p) (\rs r = evaluate p rs {r & labels = [show1 l:r.labels]})
= Prop (testname p) (evaluate p)
| c = Prop (testname p) Nothing (\rs r = evaluate p rs {r & labels = [show1 l:r.labels]})
= Prop (testname p) Nothing (evaluate p)
label :: !l !p -> Property | Testable p & genShow{|*|} l
label l p = Prop (testname p) (\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]})
name :: !n !p -> Property | Testable p & toString n
name n p = Prop (toString n) (\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]})
location_and_name :: !TestLocation !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]}
limitNrOfRecFieldValues :: !(Map (TypeName, RecFieldName) Int) !p -> Property | Testable p
limitNrOfRecFieldValues limits p = Prop (testname p) (\rs r = evaluate p rs {Admin| r & recFieldValueNrLimits = limits})
limitNrOfRecFieldValues limits p = Prop (testname p) Nothing (\rs r = evaluate p rs {Admin| r & recFieldValueNrLimits = limits})
instance ~ Bool where ~ b = not b
......@@ -227,9 +231,9 @@ where
~ Undef = Undef
instance ~ Property
where ~ (Prop n p) = Prop ("~" +++ n) (\rs r = let r` = testAnalysis r (p rs r) in [{r` & res = ~r`.res}])
where ~ (Prop n m p) = Prop ("~" +++ n) m (\rs r = let r` = testAnalysis r (p rs r) in [{r` & res = ~r`.res}])
approxEqual :: !a !a !a -> Property | abs, Ord, -, genShow{|*|}, gPrint{|*|} a
approxEqual err x y = Prop "approximately equals"
approxEqual err x y = Prop "approximately equals" Nothing
(affirm (\x y -> abs (x - y) <= err)
(Other $ concat ["approximately equals (error = ", printToString err, ")"]) x y)
......@@ -11,10 +11,11 @@ definition module Gast.Testable
pieter@cs.ru.nl
*/
from StdMaybe import :: Maybe(Nothing)
import Gast.GenLibTest
from Gast.StdProperty import ::Property // for instance of testable
import Gast.Gen
from Testing.TestEvents import :: CounterExample, :: FailedAssertion
from Testing.TestEvents import :: TestLocation, :: CounterExample, :: FailedAssertion
from Text.GenPrint import class PrintOutput, :: PrintState, generic gPrint
//--- basics --//
......@@ -34,16 +35,20 @@ newAdmin :: Admin
derive gLess Result
instance == Result
:: Property = Prop String (GenState Admin -> [Admin])
:: Property = Prop String (Maybe TestLocation) (GenState Admin -> [Admin])
prop :: a -> Property | Testable a
class TestArg a | genShow{|*|}, ggen{|*|}, gPrint{|*|} a
class Testable a
where
evaluate :: !a GenState !Admin -> [Admin]
testname :: a -> String
testlocation :: a -> Maybe TestLocation
testlocation _ = Nothing
instance Testable Bool
instance Testable Result
instance Testable Property
......@@ -113,10 +118,10 @@ generateAll :: !GenState -> [a] | ggen{|*|} a //& genType{|*|} a
}
:: GastEvent
= GE_TestStarted String
| GE_TestFinished String TestsResult [CounterExampleRes] [(String,Int)]
| GE_CounterExample CounterExampleRes
| GE_Tick Int Admin
= GE_TestStarted !(Maybe TestLocation) !String
| GE_TestFinished !(Maybe TestLocation) !String !TestsResult ![CounterExampleRes] ![(String,Int)]
| GE_CounterExample !CounterExampleRes
| GE_Tick !Int !Admin
:: PrintOption
= Verbose
......@@ -128,8 +133,8 @@ generateAll :: !GenState -> [a] | ggen{|*|} a //& genType{|*|} a
:: PrintConfig =
{ everyOutput :: Int Admin -> String
, counterExampleOutput :: CounterExampleRes -> String
, beforeStartOutput :: String -> String
, resultOutput :: String TestsResult [CounterExampleRes] [(String, Int)] -> String
, beforeStartOutput :: (Maybe TestLocation) String -> String
, resultOutput :: (Maybe TestLocation) String TestsResult [CounterExampleRes] [(String, Int)] -> String
}
printEvents :: PrintConfig [GastEvent] -> [String]
......
......@@ -17,6 +17,7 @@ from Data.Func import $
import Data.Functor
from Data.List import instance Functor [], concatMap
import qualified Data.Map
import Data.Maybe
import Math.Random
import Testing.TestEvents
import Text
......@@ -49,8 +50,9 @@ instance Testable Result where
instance Testable Property
where
evaluate (Prop _ p) genState result = p genState result
testname (Prop n _) = n
evaluate (Prop _ _ p) genState result = p genState result
testname (Prop n _ _) = n
testlocation (Prop _ l _) = l
instance Testable (a->b) | Testable b & genShow{|*|} a & ggen{|*|} a & TestArg a
where
......@@ -58,6 +60,7 @@ where
where
genState` = {GenState| genState & recFieldValueNrLimits = admin.Admin.recFieldValueNrLimits}
testname f = thunk_name_to_string f
testlocation f = Just {moduleName=Just (thunk_to_module_name_string f)}
instance Testable [a] | Testable a
where
......@@ -65,7 +68,7 @@ where
testname xs = "[" +++ join "," (map testname xs) +++ "]"
prop :: a -> Property | Testable a
prop p = Prop (testname p) (evaluate p)
prop p = Prop (testname p) (testlocation p) (evaluate p)
forAll :: !(a->b) ![a] GenState !Admin -> [Admin] | Testable b & TestArg a
forAll f [] genState r=:{Admin| args} = [{r & args = reverse args, res = OK}] // to handle empty sets of values
......@@ -109,10 +112,10 @@ printEvents pc [ge:ges] = case s of
s -> [s:printEvents pc ges]
where
s = case ge of
GE_TestStarted n -> pc.beforeStartOutput n
GE_TestFinished n r ces labels -> pc.resultOutput n r ces labels
GE_CounterExample ce -> pc.counterExampleOutput ce
GE_Tick n adm -> pc.everyOutput n adm
GE_TestStarted l n -> pc.beforeStartOutput l n
GE_TestFinished l n r ces labels -> pc.resultOutput l n r ces labels
GE_CounterExample ce -> pc.counterExampleOutput ce
GE_Tick n adm -> pc.everyOutput n adm
printEvents _ [] = []
defaultTestConfig =
......@@ -170,8 +173,8 @@ testEventsPrintConfig =
noCounterExampleOutput :: CounterExampleRes -> String
noCounterExampleOutput _ = ""
noBeforeOutput :: !String -> String
noBeforeOutput _ = ""
noBeforeOutput :: !(Maybe TestLocation) !String -> String
noBeforeOutput _ _ = ""
noEveryOutput :: !Int Admin -> String
noEveryOutput n _ = ""
......@@ -194,8 +197,8 @@ where
showFailedAssertion :: !(!FailedAssertion, !String, !String) -> [String]
showFailedAssertion (ExpectedRelation _ rel _, x, y) = ["not (", x, " ", toString rel, " ", y, ")\n"]
humanReadableResOutput :: Bool String TestsResult [CounterExampleRes] [(String, Int)] -> String
humanReadableResOutput addWhite name {maxTests, nRej, resultType} _ labels = withBlank $ showName True name +++ resStr
humanReadableResOutput :: Bool (Maybe TestLocation) String TestsResult [CounterExampleRes] [(String, Int)] -> String
humanReadableResOutput addWhite _ name {maxTests, nRej, resultType} _ labels = withBlank $ showName True name +++ resStr
where
resStr = case resultType of
Proof nTests -> "Proof: " +++ msgStr +++ conclude nTests 0 labels
......@@ -234,17 +237,18 @@ where
showLabels 0 [(lab,n):rest] = ["\n",lab,": ",toString n:showLabels 0 rest]
showLabels ntests [(lab,n):rest] = ["\n",lab,": ",toString n," (",toString (toReal (n*100)/toReal ntests),"%)":showLabels ntests rest]
jsonEventStart :: !String -> String
jsonEventStart name = toString (toJSON {StartEvent | name=name}) +++ "\n"
jsonEventStart :: !(Maybe TestLocation) !String -> String
jsonEventStart loc name = toString (toJSON {StartEvent | name=name, location=loc}) +++ "\n"
jsonEventEnd :: String TestsResult [CounterExampleRes] [(String, Int)] -> String
jsonEventEnd name res counterExamples labels = toString (toJSON endEvent) +++ "\n"
jsonEventEnd :: !(Maybe TestLocation) !String !TestsResult ![CounterExampleRes] ![(String, Int)] -> String
jsonEventEnd loc name res counterExamples labels = toString (toJSON endEvent) +++ "\n"
where
endEvent =
{ name = showName False name
, event = eventType
, message = concat
[ humanReadableResOutput False name res counterExamples labels
{ name = showName False name
, location = loc
, event = eventType
, message = concat
[ humanReadableResOutput False loc name res counterExamples labels
: map (humanReadableCEOutput False False) counterExamples
]
}
......@@ -347,14 +351,14 @@ testEventsn n rs p = printEvents testEventsPrintConfig $ testConfig rs { default
testConfig :: RandomStream Config p -> [GastEvent] | Testable p
testConfig rs {maxTests,maxArgs,fails,genState} p
# res = evaluate p genState newAdmin
= [GE_TestStarted (testname p):analyse res maxTests maxArgs 0 0 0 [] []]
= [GE_TestStarted (testlocation p) (testname p):analyse res maxTests maxArgs 0 0 0 [] []]
where
analyse :: ![.Admin] !Int !Int !Int !Int !Int [CounterExampleRes] ![(String,Int)] -> [GastEvent]
analyse results nTests nArgs nRej nUnd nE counterExamples labels =
case analyse` results nTests nArgs nRej nUnd nE of
// testing of property finished
Just resType -> [GE_TestFinished
(testname p)
(testlocation p) (testname p)
{maxTests = maxTests, nRej = nRej, resultType = resType}
counterExamples
labels]
......@@ -378,7 +382,7 @@ where
more | nE+1<fails
= analyse rest (nTests-1) (nArgs-1) nRej nUnd (nE+1) [counterExample: counterExamples] (admin res.labels labels)
= [GE_TestFinished
(testname p)
(testlocation p) (testname p)
{ maxTests = maxTests
, nRej = nRej
, resultType = CounterExpls (nTests - 1) nUnd (nE + 1)
......