Commit abf857b0 authored by Bas Lijnse's avatar Bas Lijnse

Upgraded to new version from Pieter

parent 92ecbddd
...@@ -3,22 +3,94 @@ definition module Gast.Gen ...@@ -3,22 +3,94 @@ definition module Gast.Gen
/* /*
GAST: A Generic Automatic Software Test-system GAST: A Generic Automatic Software Test-system
Gast.Gen: generic generation of values of a type gen: generic generation of values of a type
Pieter Koopman, 2004 Pieter Koopman, 2004, 2014
Radboud Universty, Nijmegen Radboud Universty, Nijmegen
The Netherlands The Netherlands
pieter@cs.ru.nl pieter@cs.ru.nl
*/ */
import StdGeneric import StdGeneric
from Gast.Set import :: Set
:: RandomStream :== [Int]
aStream :: RandomStream
splitRandomStream :: !RandomStream -> (RandomStream,RandomStream)
randomize :: [a] [Int] Int ([Int] -> [a]) -> [a] randomize :: [a] [Int] Int ([Int] -> [a]) -> [a]
generic ggen a :: Int [Int] -> [a] generic ggen a :: !GenState -> [a]
:: GenState
= { depth :: !Int // depth
, maxDepth :: !Int
, path :: ![ConsPos] // path to nonrecursive constructor
, skewl :: !Int
, skewr :: !Int
// , random :: !RandomStream
, recInfo :: !(Set RecInfo)
, pairTree :: !PairTree
}
:: TypeName :== String
:: RecInfo = { r_name :: TypeName, r_types :: Set TypeName }
:: PairTree = PTLeaf | PTNode PairTree Bool Bool PairTree
genState :: GenState
derive ggen Int, Bool, Real, Char, UNIT, PAIR, EITHER, CONS of gcd, OBJECT of gtd, FIELD, (,), (,,), (,,,), [], String, RECORD
//derive ggen Int, Bool, Real, Char, UNIT, PAIR, EITHER, CONS, OBJECT, FIELD, (,), (,,), (,,,), [], String
maxint :: Int
minint :: Int
StrLen :== 80
/* ****************************
definition module gen
/*
GAST: A Generic Automatic Software Test-system
gen: generic generation of values of a type
Pieter Koopman, 2004
Radboud Universty, Nijmegen
The Netherlands
pieter@cs.ru.nl
*/
import StdGeneric, set ///, genType
:: RandomStream :== [Int]
aStream :: RandomStream
split :: !RandomStream -> (RandomStream,RandomStream)
randomize :: [a] [Int] Int ([Int] -> [a]) -> [a]
generic ggen a :: !GenState -> [a]
:: GenState
= { depth :: !Int // depth
, maxDepth :: !Int
, path :: ![ConsPos] // path to nonrecursive constructor
, skewl :: !Int
, skewr :: !Int
// , random :: !RandomStream
// , recInfo :: !(Set RecInfo)
, seenTypes :: [GenType]
, currType :: GenType
, pairTree :: !PairTree
}
:: TypeName :== String
//:: RecInfo = { r_name :: TypeName, r_types :: Set TypeName }
:: PairTree = PTLeaf | PTNode PairTree Bool Bool PairTree
genState :: GenState
derive ggen Int, Bool, Real, Char, UNIT, PAIR, EITHER, CONS, OBJECT, FIELD, (,), (,,), (,,,), [], String derive ggen Int, Bool, Real, Char, UNIT, PAIR, EITHER, CONS of gcd, OBJECT of gtd, FIELD, (,), (,,), (,,,), [], String
//derive ggen Int, Bool, Real, Char, UNIT, PAIR, EITHER, CONS, OBJECT, FIELD, (,), (,,), (,,,), [], String
maxint :: Int maxint :: Int
minint :: Int minint :: Int
StrLen :== 80 StrLen :== 80
********************** */
This diff is collapsed.
definition module Gast.Set
import StdOverloaded, Data.Maybe, Gast.GenLibTest
/*
Pieter Koopman, pieter@cs.ru.nl
an implementation of sets for Gast, 2012
*/
:: Set a
// basic assumption: (not (a<b) && not (b<a)) == (a == b)
toList :: (Set a) -> [a] //
toSet :: [a] -> Set a | < a // toSet l ==: insl l O
instance == (Set a) | == a // equivalence
O :: Set a // empty set
singleton :: a -> Set a // singleton a ==: ins a O
ins :: !a !(Set a) -> Set a | < a // insert element
insl :: ![a] !(Set a) -> Set a | < a // insert list of elements
(isIn) infixl 5 :: !a !(Set a) -> Bool | < a // test if element is in set
(isSubSet) infixl 5 :: !(Set a) !(Set a) -> Bool | < a // test for subset
(-.) infixl 5 :: !(Set a) !a -> Set a | < a // remove element
(\.) infixl 5 :: !(Set a) !(Set a) -> Set a | < a // set difference
(u) infixl 5 :: !(Set a) !(Set a) -> Set a | < a // union
(n) infixl 5 :: !(Set a) !(Set a) -> Set a | < a // intersection
(|-) infixl 5 :: !(Set a) !a -> Maybe a | < a // remove and yield the given element
elem :: (Set a) -> (Maybe a, Set a) // remove smallest element
cardinality :: (Set a) -> Int // # elements in set
setMap :: (a->b) (Set a) -> Set b | < b // apply function to elements
derive genShow Set
implementation module Gast.Set
/*
Pieter Koopman, pieter@cs.ru.nl
an implementation of sets for Gast, 2012
*/
import StdEnv, Data.Maybe, Gast.GenLibTest
:: Set a = Set [a] // always sorted
toList :: (Set a) -> [a]
toList (Set s) = s
toSet :: [a] -> Set a | < a
toSet l = insl l O
instance == (Set a) | == a
where (==) (Set x) (Set y) = x == y
/* where
eq [a:x] [b:y] = a == b && eq x y
(==) [] [] = True
(==) s t = False
*/
O :: Set a
O = Set []
singleton :: a -> Set a
singleton a = Set [a]
ins :: !a !(Set a) -> Set a | < a // insert
ins a (Set s) = Set (insl a s)
where
insl a [] = [a]
insl a s=:[b:x]
| a < b = [a:s]
| b < a = [b:insl a x]
= [a:x] //s // a == b
insl :: ![a] !(Set a) -> Set a | < a // insert list
insl l s = foldl (flip ins) s l
(|-) infixl 5 :: !(Set a) !a -> Maybe a | < a // remove
(|-) (Set [b:x]) a
| a < b = Nothing
| b < a = Set x |- a
= Just b
(|-) (Set []) a = Nothing
(isIn) infixl 5 :: !a !(Set a) -> Bool | < a // is in set
(isIn) a (Set [b:x])
| b < a = a isIn Set x
= not (a < b)
(isIn) a (Set []) = False
(isSubSet) infixl 5 :: !(Set a) !(Set a) -> Bool | < a
(isSubSet) s=:(Set [a:x]) t=:(Set [b:y])
| a < b = False
| b < a = s isSubSet Set y
= Set x isSubSet Set y
(isSubSet) (Set s) t = isEmpty s
(\.) infixl 5 :: !(Set a) !(Set a) -> Set a | < a // difference
(\.) (Set x) (Set y) = Set (diff x y)
where
diff s=:[a:x] t=:[b:y]
| a < b = [a:diff x t]
| b < a = diff s y
= diff x y // a == b
diff s [] = s
diff [] t = []
(-.) infixl 5 :: !(Set a) !a -> Set a | < a // difference
(-.) (Set s) a = Set (diff s a)
where
diff [] a = []
diff s=:[b:x] a
| a < b = s
| b < a = [b: diff x a]
= x // a == b
(u) infixl 5 :: !(Set a) !(Set a) -> Set a | < a // union
(u) (Set x) (Set y) = Set (union x y)
where
union s=:[a:x] t=:[b:y]
| a < b = [a: union x t]
| b < a = [b: union s y]
= [a: union x y] // a == b
union [] t = t
union s [] = s
(n) infixl 5 :: !(Set a) !(Set a) -> Set a | < a // intersection
(n) (Set x) (Set y) = Set (intersection x y)
where
intersection s=:[a:x] t=:[b:y]
| a < b = intersection x t
| b < a = intersection s y
= [a: intersection x y] // a == b
intersection s t = []
elem :: (Set a) -> (Maybe a, Set a) // remove smallest element
elem (Set [a:x]) = (Just a, Set x )
elem set = (Nothing, set)
cardinality :: (Set a) -> Int
cardinality (Set s) = length s
setMap :: (a->b) (Set a) -> Set b | < b
setMap f (Set s) = toSet (map f s)
//derive genShow Set
genShow{|Set|} f s p set c = genShow{|*->*|} f s p (toList set) c
...@@ -3,7 +3,7 @@ definition module Gast.StdProperty ...@@ -3,7 +3,7 @@ definition module Gast.StdProperty
/* /*
GAST: A Generic Automatic Software Test-system GAST: A Generic Automatic Software Test-system
Gast.StdProperty: opertors on logical properties stdProperty: opertors on logical properties
Pieter Koopman, 2004 Pieter Koopman, 2004
Radboud Universty, Nijmegen Radboud Universty, Nijmegen
...@@ -11,6 +11,7 @@ definition module Gast.StdProperty ...@@ -11,6 +11,7 @@ definition module Gast.StdProperty
pieter@cs.ru.nl pieter@cs.ru.nl
*/ */
import Gast.GenLibTest
import Gast.Testable import Gast.Testable
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
...@@ -26,12 +27,16 @@ instance \/ Property Bool ...@@ -26,12 +27,16 @@ instance \/ Property Bool
instance \/ Bool Property instance \/ Bool Property
instance \/ Property Property instance \/ Property Property
(=.=) infix 4 :: !a !a -> Property | Eq, genShow{|*|} a // shows values x and y if x =.= y yields False
//check :: (a a -> Bool) -> a a -> Property | genShow{|*|} a
check :: (a a -> Bool) !a !a -> Property | genShow{|*|} a
class (==>) infixr 1 b :: b p -> Property | Testable p class (==>) infixr 1 b :: b p -> Property | Testable p
instance ==> Bool instance ==> Bool
instance ==> Property instance ==> Property
(<==>) infix 4 :: !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
ExistsIn :: (x->p) [x] -> Property | Testable p & TestArg x // type is too restricive ExistsIn :: (x->p) [x] -> Property | Testable p & TestArg x // type is too restricive
Exists :: (x->p) -> Property | Testable p & TestArg x Exists :: (x->p) -> Property | Testable p & TestArg x
......
...@@ -3,7 +3,7 @@ implementation module Gast.StdProperty ...@@ -3,7 +3,7 @@ implementation module Gast.StdProperty
/* /*
GAST: A Generic Automatic Software Test-system GAST: A Generic Automatic Software Test-system
Gast.StdProperty: opertors on logical properties stdProperty: opertors on logical properties
Pieter Koopman, 2004..2008 Pieter Koopman, 2004..2008
Radboud Universty, Nijmegen Radboud Universty, Nijmegen
...@@ -41,10 +41,9 @@ instance /\ Bool Property where (/\) x y = prop x /\ y ...@@ -41,10 +41,9 @@ instance /\ Bool Property where (/\) x y = prop x /\ y
instance /\ Property Property instance /\ Property Property
where (/\) x y = Prop (and x y) where (/\) x y = Prop (and x y)
where where
and x y rs r and x y genState r
# (rs2,rs) = splitRandomStream rs # r1 = testAnalysis r (evaluate x genState r)
r1 = testAnalysis r (evaluate x rs r) r2 = testAnalysis r (evaluate y genState r)
r2 = testAnalysis r (evaluate y rs2 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]
...@@ -79,21 +78,19 @@ instance \/ Bool Property where (\/) x y = prop x \/ y ...@@ -79,21 +78,19 @@ instance \/ Bool Property where (\/) x y = prop x \/ y
instance \/ Property Property instance \/ Property Property
where (\/) x y = Prop (or x y) where (\/) x y = Prop (or x y)
where where
or x y rs r or x y genState r
# (rs2,rs) = splitRandomStream rs = case testAnalysis r (evaluate x genState r) of
= case testAnalysis r (evaluate x rs r) of
r=:{res=OK} = [r] r=:{res=OK} = [r]
r=:{res=Pass} = case testAnalysis r (evaluate y rs2 r) of r=:{res=Pass} = case testAnalysis r (evaluate y genState r) of
r2=:{res=OK} = [r2] r2=:{res=OK} = [r2]
= [r] = [r]
= evaluate y rs2 r = evaluate y genState r
(<==>) infix 4 :: !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
# rs = genRandInt 42 # r = newAdmin
r = {res=Undef, labels=[], args=[], name=[]} b = testAnalysis r (evaluate p genState r)
b = testAnalysis r (evaluate p rs r) c = testAnalysis r (evaluate q genState r)
c = testAnalysis r (evaluate q rs 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
...@@ -105,9 +102,7 @@ where p rs r = [exists r [testAnalysis r (evaluate (f a) rs r)\\a <- l] MaxExist ...@@ -105,9 +102,7 @@ where p rs r = [exists r [testAnalysis r (evaluate (f a) rs r)\\a <- l] MaxExist
Exists :: (x->p) -> Property | Testable p & TestArg x Exists :: (x->p) -> Property | Testable p & TestArg x
Exists f = Prop p Exists f = Prop p
where p rs r where p genState r = [exists r [testAnalysis r (evaluate (f a) genState r)\\a <- generateAll genState] MaxExists]
# (rs,rs2) = splitRandomStream rs
= [exists r [testAnalysis r (evaluate (f a) rs2 r)\\a <- generateAll rs] 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
...@@ -161,11 +156,29 @@ where VOOR (PL fl) l = diagonal [map f l\\f<-fl] //[f x \\ f<-fl, x<-l] ...@@ -161,11 +156,29 @@ where VOOR (PL fl) l = diagonal [map f l\\f<-fl] //[f x \\ f<-fl, x<-l]
// XXXXXXXXXXXXXXXXXXXXXXXXXX // XXXXXXXXXXXXXXXXXXXXXXXXXX
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]
]
]
}
(ForAndGen) infixl 0 :: !(x->p) ![x] -> Property | Testable p & TestArg x (ForAndGen) infixl 0 :: !(x->p) ![x] -> Property | Testable p & TestArg x
(ForAndGen) p list = Prop (evaluate p) (ForAndGen) p list = Prop (evaluate p)
where evaluate f rs result where evaluate f rs result = forAll f (list++generateAll genState) rs result
# (rs,rs2) = splitRandomStream rs
= forAll f (list++generateAll rs) rs2 result
classify :: !Bool l !p -> Property | Testable p & genShow{|*|} l classify :: !Bool l !p -> Property | Testable p & genShow{|*|} l
classify c l p classify c l p
...@@ -191,3 +204,53 @@ where ...@@ -191,3 +204,53 @@ where
instance ~ Property instance ~ Property
where ~ (Prop p) = Prop (\rs r = let r` = testAnalysis r (p rs r) in [{r` & res = ~r`.res}]) where ~ (Prop p) = Prop (\rs r = let r` = testAnalysis r (p rs r) in [{r` & res = ~r`.res}])
// ================================================================
// :( :( 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
}
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
}
get_module_name_char :: !Int !Int -> Char;
get_module_name_char a i = code {
addI
load_ui8 4
}
...@@ -3,58 +3,78 @@ definition module Gast.Testable ...@@ -3,58 +3,78 @@ definition module Gast.Testable
/* /*
GAST: A Generic Automatic Software Test-system GAST: A Generic Automatic Software Test-system
Gast.Testable: the test algorithm for logical properties testable: the test algorithm for logical properties
Pieter Koopman, 2002-2007 Pieter Koopman, 2002-2012
Radboud Universty, Nijmegen Radboud Universty, Nijmegen
The Netherlands The Netherlands
pieter@cs.ru.nl pieter@cs.ru.nl
*/ */
import Gast.GenLibTest import Gast.GenLibTest
from Gast.StdProperty import ::Property // for instance of testable from Gast.StdProperty import ::Property // for instance of testable
import Gast.Gen import Gast.Gen
//--- basics --// //--- basics --//
:: Admin = {labels::![String], args::![String], name::![String], res::Result} :: Admin = {labels::![String], args::![String], name::![String], res::Result, mes::[String]}
:: Result = Undef | Rej | Pass | OK | CE :: Result = Undef | Rej | Pass | OK | CE
:: RandomStream :== [Int] newAdmin :: Admin
derive gLess Result derive gLess Result
instance == Result instance == Result
:: Property = Prop (RandomStream Admin -> [Admin]) :: Property = Prop (GenState Admin -> [Admin])
prop :: a -> Property | Testable a prop :: a -> Property | Testable a
class TestArg a | genShow{|*|}, ggen{|*|} a class TestArg a | genShow{|*|} a & ggen{|*|} a
class Testable a where evaluate :: a RandomStream !Admin -> [Admin] class Testable a where evaluate :: a GenState !Admin -> [Admin]
instance Testable Bool instance Testable Bool
instance Testable Result instance Testable Result
instance Testable Property instance Testable Property
instance Testable (a->b) | Testable b & TestArg a ///instance Testable (a->b) | Testable b & genShow{|*|} a & ggen{|*|} a //TestArg a
instance Testable (a->b) | Testable b & genShow{|*|} a & ggen{|*|} a & TestArg a
instance Testable [a] | Testable a instance Testable [a] | Testable a
//derive bimap [], (,), (,,), (,,,), (,,,,), (,,,,,) //derive bimap [], (,), (,,), (,,,), (,,,,), (,,,,,)
MaxExists :== 500 MaxExists :== 1000
NrOfTest :== 1000 NrOfTest :== 1000
//--- for generating lists of elements ---// //--- for generating lists of elements ---//
aStream :: RandomStream //aStream :: RandomStream
//split :: !RandomStream -> (RandomStream,RandomStream)
//--- for implementation of properties ---// //--- for implementation of properties ---//
diagonal :: [[a]] -> [a] diagonal :: [[a]] -> [a]
forAll :: !(a->b) ![a] RandomStream !Admin -> [Admin] | Testable b & TestArg a forAll :: !(a->b) ![a] GenState !Admin -> [Admin] | Testable b & TestArg a
splitRandomStream :: !RandomStream -> (RandomStream,RandomStream) //split :: !RandomStream -> (RandomStream,RandomStream)
generateAll :: !RandomStream -> [a] | ggen{|*|} a //generateAll :: !RandomStream -> [a] | ggen{|*|} a
generateAll :: !GenState -> [a] | ggen{|*|} a //& genType{|*|} a
//--- testing --// //--- testing --//
:: Testoption
= Tests Int
| Fails Int
| Args Int
| RandomSeed Int