Commit af51a144 authored by cvs2snv's avatar cvs2snv
Browse files

This commit was manufactured by cvs2svn to create tag 'clean-2-1-0'.

parent 02f915da
definition module genLibTest
/*
Pieter Koopman 2002
Nijmegen University, The Netherlands
GAST: A Generic Automatic Software Test-system
*/
import StdGeneric
import StdClass
instance + String
(@) infixl 2 :: (a->b) a -> b
(@!)infixl 2 :: (a->b) !a -> b
generic genShow a :: String Bool a [String] -> [String]
generic gEq a :: a a -> Bool
generic gLess a :: a a -> Bool
derive genShow Int, Char, Bool, Real, String, UNIT, PAIR, EITHER, CONS, FIELD, OBJECT, [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,), (,,,,,,,,), (,,,,,,,,,), (->), {}, {!}
derive gEq Int, Char, Bool, Real, String, UNIT, PAIR, EITHER, CONS, FIELD, OBJECT, [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,), (,,,,,,,,), (,,,,,,,,,)
derive gLess Int, Char, Bool, Real, String, UNIT, PAIR, EITHER, CONS, FIELD, OBJECT, [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,), (,,,,,,,,), (,,,,,,,,,)
show :: !a -> [String] | genShow{|*|} a
show1 :: !a -> String | genShow{|*|} a
(===) infix 4 :: !a !a -> Bool | gEq{|*|} a
(=/=) infix 4 :: !a !a -> Bool | gEq{|*|} a
(-<-) infix 4 :: !a !a -> Bool | gLess{|*|} a
(->-) infix 4 :: !a !a -> Bool | gLess{|*|} a
(-<=) infix 4 :: !a !a -> Bool | gLess{|*|} a
(=>-) infix 4 :: !a !a -> Bool | gLess{|*|} a
implementation module genLibTest
/*
Pieter Koopman 2002
Nijmegen University, The Netherlands
GAST: A Generic Automatic Software Test-system
*/
import StdEnv, StdGeneric
instance + String where (+) s t = s +++ t
(@)infixl 2 :: (a->b) a -> b
(@) f x = f x
(@!)infixl 2 :: (a->b) !a -> b
(@!) f x = f x
//--- show ---//
generic genShow a :: String Bool a [String] -> [String]
genShow{|Int|} sep p x rest = [toString x: rest]
genShow{|Char|} sep p x rest = ["'",toString x,"'": rest]
genShow{|Bool|} sep p x rest = [toString x: rest]
genShow{|Real|} sep p x rest = [toString x: rest]
genShow{|String|} sep p s rest = ["\"",s,"\"":rest]
genShow{|UNIT|} sep p _ rest = rest
genShow{|PAIR|} fx fy sep p (PAIR x y) rest = fx sep p x [sep: fy sep p y rest]
genShow{|EITHER|} fl fr sep p (LEFT x) rest = fl sep p x rest
genShow{|EITHER|} fl fr sep p (RIGHT x) rest = fr sep p x rest
genShow{|(->)|} fa fr sep p f rest = ["<function>": rest]
genShow{|{}|} fx sep p xs rest = ["{" :showList fx [x\\x<-:xs] ["}":rest]]
genShow{|{!}|} fx sep p xs rest = ["{!":showList fx [x\\x<-:xs] ["}":rest]]
//genShow{|{#}|} fx sep p xs rest = ["{#":showList fx [x\\x<-:xs] ["}":rest]]
genShow{|[]|} f sep p xs rest = ["[" :showList f xs ["]":rest]]
genShow{|(,)|} f1 f2 sep p (x1,x2) rest = ["(":f1 sep False x1 [",":f2 sep False x2 [")":rest]]]
genShow{|(,,)|} f1 f2 f3 sep p (x1,x2,x3) rest = ["(":f1 sep False x1 [",":f2 sep False x2 [",":f3 sep False x3 [")":rest]]]]
genShow{|(,,,)|} f1 f2 f3 f4 sep p (x1,x2,x3,x4) rest
= ["(":f1 sep False x1 [",":f2 sep False x2 [",":f3 sep False x3 [",":f4 sep False x4 [")":rest]]]]]
genShow{|(,,,,)|} f1 f2 f3 f4 f5 sep p (x1,x2,x3,x4,x5) rest
= ["(":f1 sep False x1 [",":f2 sep False x2 [",":f3 sep False x3 [",":f4 sep False x4 [",":f5 sep False x5 [")":rest]]]]]]
genShow{|(,,,,,)|} f1 f2 f3 f4 f5 f6 sep p (x1,x2,x3,x4,x5, x6) rest = ["(":f1 sep False x1 [",":f2 sep False x2 [",":f3 sep False x3 [",":f4 sep False x4 [",":f5 sep False x5 [",":f6 sep False x6 [")":rest]]]]]]]
genShow{|(,,,,,,)|}f1 f2 f3 f4 f5 f6 f7 sep p (x1,x2,x3,x4,x5,x6,x7) rest
= ["(":f1 sep False x1 [",":f2 sep False x2 [",":f3 sep False x3 [",":f4 sep False x4 [",":f5 sep False x5 [",":f6 sep False x6 [",":f7 sep False x7 [")":rest]]]]]]]]
genShow{|(,,,,,,,)|}f1 f2 f3 f4 f5 f6 f7 f8 sep p (x1,x2,x3,x4,x5,x6,x7,x8) rest
= ["(":f1 sep False x1 [",":f2 sep False x2 [",":f3 sep False x3 [",":f4 sep False x4 [",":f5 sep False x5 [",":f6 sep False x6 [",":f7 sep False x7 [",":f8 sep False x8 [")":rest]]]]]]]]]
genShow{|(,,,,,,,,)|}f1 f2 f3 f4 f5 f6 f7 f8 f9 sep p (x1,x2,x3,x4,x5,x6,x7,x8,x9) rest
= ["(":f1 sep False x1 [",":f2 sep False x2 [",":f3 sep False x3 [",":f4 sep False x4 [",":f5 sep False x5 [",":f6 sep False x6 [",":f7 sep False x7 [",":f8 sep False x8 [",":f9 sep False x9 [")":rest]]]]]]]]]]
genShow{|(,,,,,,,,,)|}f1 f2 f3 f4 f5 f6 f7 f8 f9 f0 sep p (x1,x2,x3,x4,x5,x6,x7,x8,x9,x0) rest
= ["(":f1 sep False x1 [",":f2 sep False x2 [",":f3 sep False x3 [",":f4 sep False x4 [",":f5 sep False x5 [",":f6 sep False x6 [",":f7 sep False x7 [",":f8 sep False x8 [",":f9 sep False x9 [",":f0 sep False x0 [")":rest]]]]]]]]]]]
genShow{|CONS of {gcd_name, gcd_arity, gcd_fields}|} fx sep p (CONS x) rest
| gcd_arity == 0
= [gcd_name: rest]
| isEmpty gcd_fields // ordinary constructor
| p // parentheses needed
= ["(",gcd_name," ":fx " " True x [")":rest]]
= [gcd_name," ":fx " " True x rest]
| otherwise // record
= ["{",{gcd_name.[i]\\i<-[1..size gcd_name-1]},"|":fx "," False x ["}":rest]]
genShow{|FIELD of {gfd_name}|} fx sep p (FIELD x) rest
= [gfd_name,"=":fx sep False x rest]
genShow{|OBJECT|} f sep p (OBJECT x) rest
= f sep p x rest
//showList :: (String Bool a [String] -> [String]) ![a] [String] -> [String]
showList :: (.String -> .(.Bool -> .(.a -> .(u:[v:String] -> w:[x:String])))) ![.a] z:[u0:String] -> w0:[x0:String], [w0 <= u,x0 <= v,z w <= w0,u0 x <= x0]
showList f [] rest = rest
showList f [x] rest = f "" False x rest
showList f [x:xs] rest = f "" False x [",":showList f xs rest]
show :: !a -> [String] | genShow{|*|} a
show x = genShow{|*|} "" False x []
show1 :: !a -> String | genShow{|*|} a
show1 x = glue (genShow{|*|} "" False x [])
where
glue :: [String] -> String
glue [] = ""
glue [x:xs]
= case xs of
[] = x
= x+glue xs
//--- equality ---//
generic gEq a :: a a -> Bool
gEq{|UNIT|} _ _ = True
gEq{|PAIR|} fx fy (PAIR x1 y1) (PAIR x2 y2) = fx x1 x2 && fy y1 y2
gEq{|EITHER|} fl fr (LEFT x) (LEFT y) = fl x y
gEq{|EITHER|} fl fr (RIGHT x) (RIGHT y) = fr x y
gEq{|EITHER|} _ _ _ _ = False
gEq{|CONS|} f (CONS x) (CONS y) = f x y
gEq{|FIELD|} f (FIELD x) (FIELD y) = f x y
gEq{|OBJECT|} f (OBJECT x) (OBJECT y) = f x y
gEq{|Int|} x y = x == y
gEq{|Char|} x y = x == y
gEq{|Bool|} x y = x == y
gEq{|Real|} x y = x == y
gEq{|String|} x y = x == y
//gEq{|(->)|} ea eb f g = ...
derive gEq [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,), (,,,,,,,,), (,,,,,,,,,)
(===) infix 4 :: !a !a -> Bool | gEq{|*|} a
(===) x y = gEq{|*|} x y
(=/=) infix 4 :: !a !a -> Bool | gEq{|*|} a
(=/=) x y = not (x === y)
//--- comparision ---//
instance < Bool
where
(<) True b = not b
(<) False _ = False
generic gLess a :: a a -> Bool
gLess{|UNIT|} _ _ = True
gLess{|PAIR|} fx fy (PAIR x1 y1) (PAIR x2 y2) = fx x1 x2 && fy y1 y2
gLess{|EITHER|} fl fr (LEFT x) (LEFT y) = fl x y
gLess{|EITHER|} fl fr (RIGHT x) (RIGHT y) = fr x y
gLess{|EITHER|} fl fr (LEFT x) (RIGHT y) = True
gLess{|EITHER|} fl fr (RIGHT x) (LEFT y) = False
gLess{|CONS|} f (CONS x) (CONS y) = f x y
gLess{|FIELD|} f (FIELD x) (FIELD y) = f x y
gLess{|OBJECT|} f (OBJECT x) (OBJECT y) = f x y
gLess{|Int|} x y = x < y
gLess{|Char|} x y = x < y
gLess{|Bool|} x y = x < y
gLess{|Real|} x y = x < y
gLess{|String|} x y = x < y
derive gLess [], (,), (,,), (,,,), (,,,,), (,,,,,), (,,,,,,), (,,,,,,,), (,,,,,,,,), (,,,,,,,,,)
(-<-) infix 4 :: !a !a -> Bool | gLess{|*|} a
(-<-) x y = gLess{|*|} x y
(->-) infix 4 :: !a !a -> Bool | gLess{|*|} a
(->-) x y = gLess{|*|} y x
(-<=) infix 4 :: !a !a -> Bool | gLess{|*|} a
(-<=) x y = not (gLess{|*|} y x)
(=>-) infix 4 :: !a !a -> Bool | gLess{|*|} a
(=>-) x y = not (gLess{|*|} x y)
module properties
/*
Pieter Koopman 2002
Nijmegen University, The Netherlands
Some properties to be tested by the generic Test System
Run this program with project option "Show basic values only"
*/
import stdTest4
//import StdTest//Small
//import StdTestSmall
:: Tree a = Tip | Bin a (Tree a) (Tree a)
:: Color = Red | Yellow | Blue // | Black
:: List a = Nil | Cons a (List a)
:: Rose a = Rose a [Rose a]
:: Fork a = Fork a a
:: Sequ a = SequEmpty | SequZero .(Sequ .(Fork a)) | SequOne a .(Sequ .(Fork a))
:: Rec = { x::Int, y::Int, c::Color}
:: T = C
(===>) infix 1 :: Bool Bool -> Bool
(===>) p q = (not p) || q
derive generate Tree, Color, List, Rose, Fork, Sequ, Rec, T , Bit, Day, Result //, Trace
derive genShow Tree, Color, List, Rose, Fork, Sequ, Rec, T, Bit, Day, Result //, Trace
derive gEq T, Tree, Color, List, Rose, Fork, Sequ, Rec, Bit, Day, Result //, Trace
propSquare :: Property
propSquare = Exists \x . x^2 == x
propSquare2 :: Property
propSquare2 = Exists \x . let b = x^2 == x in classify b x b
propZero :: Int -> Property
propZero x = prop (x+0 == 0+x)
propPlus :: Int Int -> Bool
propPlus x y = x+y==y+x
propSqrt1 :: Real -> Bool
propSqrt1 x = (\s = s*s) (sqrt x) == x
propSqrt :: Real -> Property
propSqrt x = name "(sqrt x)^2=x" (x>=0.0 ==> let s = sqrt x in s*s == x)
propSqrt2 :: Real -> Bool
propSqrt2 x = x>=0.0 ===> let s = sqrt x in s*s == x
propSqrt3 :: Real -> Property
propSqrt3 x = x>=0.0 ==> let s = sqrt x in name ("sqrt",x) @ s*s == x
propAssoc :: Real Real Real -> Bool
propAssoc x y z = (x+(y+z) == (x+y)+z)
propMax :: Int Int -> Property
propMax x y = label x @ x<=y ==> max x y == y
propRevRev :: [Bool] -> Bool
propRevRev xs = reverse (reverse xs) == xs
propRevRevl :: [T] -> Property
propRevRevl xs = classify (isEmpty xs) xs (reverse (reverse xs) === xs)
propRevReval :: [Bit] -> Property
propRevReval xs = label (length xs) (reverse (reverse xs) === xs)
propDrop :: Int Int [Int] -> Bool
propDrop m n xs = drop n (drop m xs) == drop (n+m) xs
propDrop2 :: Int Int [Int] -> Property
propDrop2 m n xs = n>=0 && m>=0 ==> drop n (drop m xs) == drop (n+m) xs
propDeMorganl :: Bool Bool -> Property
propDeMorganl x y = label ('x',x) (label ('y',y) ((x&&y) == not (not x || not y)))
propDeMorgan :: Bool Bool -> Bool
propDeMorgan x y = x&&y == not (not x || not y)
propOr :: Bool Bool -> Bool
propOr x y = x||y == or x y
where
or x y = nand (not x) (not y)
not x = nand x x
nand :: Bool Bool -> Bool
nand x y = not (x&&y)
propNot :: Bool -> Property
propNot b = label b case b of
True = not b == False
False = not b == True
propFix :: (Int->Int) -> Property
propFix f = Exists \x = f x == x
propFixL :: (Int->Int) -> Property
propFixL f = Exists \x = let b = f x == x in classify b x b // show the fixpoints found
propTupLists :: ([Bit],[Bit]) -> Property
propTupLists (xs,ys) = classify (isEmpty xs) ("xs",xs) (classify (isEmpty ys) ("ys",ys) (length xs + length ys >= 0))
// --- Alternating bit-protocol
:: Bit = O | I
instance ~ Bit
where
~ O = I
~ I = O
:: Message c = M c Bit | MError
:: Ack = A Bit | AError
:: SenderState c = Send Bit | Exp Bit c
:: ReceiverState = Rec Bit
sender :: (SenderState c) [c] [Ack] -> [Message c]
sender (Send b) [] as = []
sender (Send b) [c:cs] as = [M c b: sender (Exp b c) cs as]
sender state=:(Exp b c) cs [a:as]
= case a of
A b` | b===b` = sender (Send (~b)) cs as
_ = [M c b: sender state cs as]
sender (Exp b c) cs [] = abort "Sender: Acknowledgement expected"
receiver :: ReceiverState [Message c] -> ([Ack],[c])
receiver rState [] = ([],[])
receiver rState=:(Rec b) [m:ms]
= case m of
M c b` | b===b` = ([A b :as],[c:cs]) where (as,cs) = receiver (Rec (~b)) ms
_ = ([A (~b):as], cs ) where (as,cs) = receiver rState ms
sChannel :: (Int->Bool) [Message c] -> [Message c]
sChannel error ms = [ if (error n) MError m \\ m <- ms & n <- [1..]]
rChannel :: (Int->Bool) [Ack] -> [Ack]
rChannel error as = [ if (error n) AError a \\ a <- as & n <- [1..]]
abpSystem :: (Int->Bool) (Int->Bool) [c] -> [c]
abpSystem sError rError toSend
= received
where
msSend = sender (Send O) toSend (rChannel rError acks)
(acks,received) = receiver (Rec O) (sChannel sError msSend)
propAltBit :: (Int->Bool) (Int->Bool) Int -> Bool
propAltBit sError rError n = toSend == received
where
toSend = [1..n]
received = abpSystem sError rError toSend
// --- Stack --- //
:: Stack a :== [a]
pop :: (Stack a) -> Stack a
pop [_:r] = r
pop _ = abort "pop from empty stack"
top :: (Stack a) -> a
top [a:_] = a
top _ = abort "pop from empty stack"
push :: a (Stack a) -> Stack a
push a s = [a:s]
propStack :: a (Stack a) -> Bool | gEq{|*|} a
propStack e s = top (push e s) === e && pop (push e s) === s
propStackN :: a (Stack a) -> Property | gEq{|*|} a
propStackN e s = label (length s) @ p1 /\ p2 /\ p3
where p1 = name "top (push e s)=e" @ top (push e s) === e
p2 = name "pop (push e s)=s" @ pop (push e s) === s
p3 = name "push t (pop s)=s" @ (~(isEmpty s) ==> (let t = top s in push t (pop s) === s))
propStackNInt :: (Int (Stack Int) -> Property)
propStackNInt = propStackN
propStackInt :: (Int (Stack Int) -> Bool)
propStackInt = propStack
propStackL :: Int (Stack Int) -> Property
propStackL e s = label (e,s) @ top (push e s) === e && pop (push e s) === s
propStackC :: Int (Stack Int) -> Property
propStackC e s = classify (isEmpty s) s (propStack e s) //@ top (push e s) === e && pop (push e s) === s
propStackFA :: Property
propStackFA = ForAll \e = ForEach [[],[1],[1,2]] \s = label (e,s) @ top (push e s) === e && pop (push e s) === s
propStack2 :: (Stack Int)[Int] -> Property
propStack2 s es = label (length es,s) @ pushAndPop es s === s
where
pushAndPop :: [e] (Stack e) -> Stack e
pushAndPop l s = popn (length l) (pushl l s)
pushl [] s = s
pushl [e:r] s = pushl r (push e s)
popn 0 s = s
popn n s = popn (n-1) (pop s)
// ---
propMapInt :: ((Int->Int) (Int->Int) [Int] -> Bool)
propMapInt = propMap
propMap :: (a->b) (b->c) [a] -> Bool | gEq{|*|} c
propMap f g xs = map g (map f xs) === map (g o f) xs
propMapC :: (Int->Int) (Int->Int) -> [Int] -> Bool
propMapC f g = \xs = map f (map g xs) == map (f o g) xs
propMapL :: (Int->Int) (Int->Int) [Int] -> Property
propMapL f g xs = label (length xs) @ map f (map g xs) == map (f o g) xs
propRec :: [Rec] -> Property
propRec list = label (length list) @ length list == length (map (\r = r.c) list)
Fib 0 = 1
Fib 1 = 1
Fib n = Fib (n-1) + Fib (n-2)
FibLin n = f n 1 1
where
f 0 a b = a
f n a b = f (n-1) b (a+b)
propFibR :: Property
propFibR = propFib For [0..15]
propFibR2 :: Property
propFibR2 = ForEach [0..15] @ \n = n>=0 ==> Fib n == FibLin n
propFibR3 :: Property
propFibR3 = ForEach [0..15] @ \n = Fib n == FibLin n
propFib :: Int -> Property
propFib n = n>=0 ==> Fib n == FibLin n
propCount :: Property
//propCount = (\x = label x True) For [1..]
//propCount = (\y = (\x = label (x,y) True) For [1..]) For [1..]
//propCount = (\y = label y ((\x = True) For [1..])) For [1..]
propCount = (\y = ((\x = label (x,y) True) For [1..])) For [1..]
//propCount = (\y = label y (ForAll (\x = x =/= x+1))) For [1..]
propList :: (Bit,Bit) -> Property
//propList :: Bit -> Property
//propList :: [Bit] -> Property
propList l = label l True
propInts :: Int Int -> Property
propInts n m = label (n,m) True
//propInts2 :: !Int -> Bool
propInts2 :: ![Int] -> Bool
propInts2 n = n==n
propInts2l :: ![Int] -> Property
propInts2l n = label (length n) (n==n)
/*
propRoots :: Real Real Real Real -> Property
propRoots a b c x = label (a,b,c,x) @ and (map (\r = abs (f r) < 0.01) (roots a b c))
where f x = a*x*x + b*x + c
*/
propRoots :: Real Real Real -> Property
//propRoots a b c = label (a,b,c) @ and (map (\r = abs (f r) < 0.01) (roots a b c))
propRoots a b c = /*label (a,b,c,length rs) @*/ classify (~ok) ("roots",(a,b,c),rs,map f rs) ok
where
f x = a*x*x + b*x + c
rs = (roots a b c)
ok = and (map (\r = abs (f r) < 0.01) rs)
roots :: Real Real Real -> [Real]
roots a b c
| a == 0.0
| b == 0.0
= []
= [~c/b]
# dsq = b*b - 4.0*a*c
| dsq < 0.0
= []
| dsq == 0.0
= [~b/(2.0*a)]
# d = sqrt dsq
= [(~b-d)/(2.0*a),(~b+d)/(2.0*a)]
instance toString Bit
where
toString I = "I"
toString O = "O"
instance toString (a,b) | toString a & toString b
where
toString (a,b) = "("+toString a+","+toString b+")"
propExists :: !a -> Property | TestArg a & gEq{|*|} a
propExists x = label x @ Exists \y = x===y
propExistsColors :: ([Color] -> Property)
propExistsColors = \x = (length x>0) ==> propExists x
:: Day = Mo | Tu | We | Th | Fr | Sa | Su
tomorrow :: Day -> Day
tomorrow d
= case d of
Mo = Tu
Tu = We
We = Th
Th = Fr
Fr = Sa
Sa = Su
Su = Mo
propTomorrow :: Day -> Property
propTomorrow day = Exists \d = tomorrow day === d
propTomorrow2 :: Day -> Property
propTomorrow2 day = Exists \d = tomorrow d === day
propSurjection = propTomorrow2
//propInjection :: Day -> Property
//propInjection day = Exists \d = (tomorrow day === tomorrow d) ==> (day === d)
propInjectionD :: Day Day -> Property
propInjectionD d1 d2 = (tomorrow d1 === tomorrow d2) ==> (d1 === d2)
propInjection :: (a->b) a a -> Property | gEq{|*|} a & gEq{|*|} b
propInjection f x y = (f x === f y) ==> (x === y)
propInverse :: Color -> Property
propInverse c = Exists p where p c` = c === inverse c`
inverse :: Color -> Color
inverse c
= case c of
Red = Blue
Yellow = Red
Blue = Yellow
propImplication :: Int -> Property
propImplication n = (Exists \m = label m (m==n)) ==> True
//---
propForFor :: Property
propForFor = (\y = ((\x = label (x,y) True) For [1..])) For [1..]
propAnd :: Bool Bool -> Property
propAnd x y = name "(x/\y) == (prop x /\ prop y)" (label ("And",</