diff --git a/README b/README --- a/README +++ b/README @@ -1,7 +1,7 @@ --------------------------------------------------------------- SmallCheck: another lightweight testing library in Haskell. -Version 0.2, November 2006 -Colin Runciman, University of York UK +Version 0.4, 21 May 2008 +Colin Runciman, University of York, UK After QuickCheck, by Koen Claessen and John Hughes (2000-2004). --------------------------------------------------------------- @@ -14,7 +14,7 @@ * write properties using existentials as well as universals? * establish complete coverage of a defined test-space? * display counter-examples of functional type? -* guarantee repeatable test results? +* always repeat tests and obtain the same results? If so, try SmallCheck! This note should be enough to get you started, assuming some prior experience with QuickCheck. @@ -35,9 +35,16 @@ is a measure combining the depth to which arguments may be evaluated and the depth of possible results. -Generators ----------- +QuickCheck's statistics-gathering operators have been omitted from +SmallCheck's property language, as they seem more relevant to the +random-testing approach. +Data Generators +--------------- + +SmallCheck itself defines data generators for all the data types used +by the Prelude. + Writing SmallCheck generators for application-specific types is straightforward. Just as the QuickCheck user defines 'arbitrary' generators, so a SmallCheck user defines 'series' generators -- but @@ -62,21 +69,39 @@ The depth of Light x is just the depth of x. +Function Generators +------------------- + To generate functions of an application-specific argument type requires a second method 'coseries' -- cf. 'coarbitrary' in QuickCheck. Again there is a standard pattern, this time using the alts combinators where again N is constructor arity. Here are Tree and Light instances: - coseries d = [ \t -> case t of - Null -> z - Fork t1 x t2 -> f t1 x t2 - | z <- alts0 d , - f <- alts3 d ] + coseries rs d = [ \t -> case t of + Null -> z + Fork t1 x t2 -> f t1 x t2 + | z <- alts0 rs d , + f <- alts3 rs d ] - coseries d = [ \l -> case l of - Light x -> f x - | f <- (alts1 . depth 0) d ] + coseries rs d = [ \l -> case l of + Light x -> f x + | f <- (alts1 rs . depth 0) d ] +(NB changed from Version 0.2: 'coseries' and 'alts' family now take a +series argument -- here rs. In the coseries definitions we simply pass +on rs as series argument in each 'alts' application.) + +Automated Derivation of Generators +---------------------------------- + +For small examples, Series instances are easy enough to define by hand, +following the above patterns. But for programs with many or large data +type definitions, automatic derivation using a tool such as 'derive' +is a better option. For example, the following command-line appends to +Prog.hs the Series instances for all data types defined there. + +$ derive Prog.hs -d Serial --append + Properties ---------- @@ -98,7 +123,7 @@ using SmallCheck. But we can also test the following property, which involves an existentially quantified variable: -prop_isPrefix2 :: String -> String -> Bool +prop_isPrefix2 :: String -> String -> Property prop_isPrefix2 xs ys = isPrefix xs ys ==> exists $ \xs' -> ys == xs++xs' @@ -122,9 +147,8 @@ prop_append2 :: [Bool] -> [Bool] -> Property prop_append2 xs ys = existsDeeperBy (*2) $ \zs -> zs == xs++ys -QuickCheck's statistics-gathering operators have been omitted from -SmallCheck's property language, as they seem more relevant to the -random-testing approach. +There are also quantifiers for unique existence. Their names include +a 1 immediately after 'exists': eg. exists1, exists1DeeperBy. Pragmatics of ==> ----------------- @@ -200,6 +224,10 @@ True False +When (unique) existential properties are tested, any failure reports +conclude with "non-existence" (or "non-uniqueness" followed by two +witnesses). + Large Test Spaces ----------------- @@ -235,23 +263,46 @@ Prelude numeric types now have Serial instances, including floating-point types. Serial types Nat and Natural are also defined. Examples extended. +Version 0.3 +----------- + +Existential quantifiers now have unique variants for which two witnesses +are reported when uniqueness fails. The over-generating coseries method +for functions of functional arguments has been replaced; now 'coseries' +and the 'alts' family take a series argument. Test counters are +now Integers, not Ints. Ord and Eq are now derived for the N types. +Examples extended. + +Version 0.4 +----------- + +The module SmallCheck is now Test.SmallCheck. Packaged with Cabal. + Final Notes ----------- The name is intended to acknowledge QuickCheck, not to suggest that -SmallCheck is a tool of equal refinement. +SmallCheck replaces it. See also Lazy SmallCheck. Each tool has its +advantages and disadvantages when compared with the others. SmallCheck is a Haskell 98 module aside from the import of unsafePerformIO for use in a single instance -- the import and instance can be commented out if there is no need to test IO computations. I am not aware of any -other portability issues. SmallCheck can be obtained from: +other portability issues. SmallCheck can be obtained from -http://www.cs.york.ac.uk/fp/smallcheck0.2.tar +http://hackage.haskell.org/cgi-bin/hackage-scripts/package/smallcheck +or alternatively from + +http://www.cs.york.ac.uk/fp/smallcheck0.4.tar + Comments and suggestions are welcome. -Thanks to Galois Connections, my hosts when I first wrote SmallCheck, and -to users who have mailed me with feedback. +Thanks to Galois Connections, my hosts when I first wrote SmallCheck, +to users who have mailed me with feedback, to Ralf Hinze who suggested +the better method for functional coseries, to Neil Mitchell for +automating the derivation of Serial instances, to Matt Naylor for +the circuit-design examples and to Gwern Branwen for Cabal packaging. Colin.Runciman@cs.york.ac.uk -6 November 2006 +23 May 2008 diff --git a/Setup.hs b/Setup.hs --- a/Setup.hs +++ b/Setup.hs diff --git a/Test/SmallCheck.hs b/Test/SmallCheck.hs --- a/Test/SmallCheck.hs +++ b/Test/SmallCheck.hs @@ -1,7 +1,7 @@ --------------------------------------------------------------------- -- SmallCheck: another lightweight testing library. -- Colin Runciman, August 2006 --- Version 0.2 (November 2006) +-- Version 0.4, 23 May 2008 -- -- After QuickCheck, by Koen Claessen and John Hughes (2000-2004). --------------------------------------------------------------------- @@ -11,6 +11,7 @@ Property, Testable, forAll, forAllElem, exists, existsDeeperBy, thereExists, thereExistsElem, + exists1, exists1DeeperBy, thereExists1, thereExists1Elem, (==>), Series, Serial(..), (\/), (><), two, three, four, @@ -20,10 +21,10 @@ depth, inc, dec ) where -import Data.List (intersperse) -import Control.Monad (when) -import System.IO (stdout, hFlush) -import System.IO.Unsafe (unsafePerformIO) -- used only for Testable (IO a) +import List (intersperse) +import Monad (when) +import IO (stdout, hFlush) +import Foreign (unsafePerformIO) -- used only for Testable (IO a) ------------------ ----------------- @@ -51,80 +52,81 @@ -- for data values, the depth of nested constructor applications -- for functional values, both the depth of nested case analysis -- and the depth of results - + class Serial a where series :: Series a - coseries :: Serial b => Series (a->b) + coseries :: Series b -> Series (a->b) instance Serial () where - series _ = [()] - coseries d = [ \() -> b - | b <- series d ] + series _ = [()] + coseries rs d = [ \() -> b + | b <- rs d ] instance Serial Int where - series d = [(-d)..d] - coseries d = [ \i -> if i > 0 then f (N (i - 1)) - else if i < 0 then g (N (abs i - 1)) - else z - | z <- alts0 d, f <- alts1 d, g <- alts1 d ] + series d = [(-d)..d] + coseries rs d = [ \i -> if i > 0 then f (N (i - 1)) + else if i < 0 then g (N (abs i - 1)) + else z + | z <- alts0 rs d, f <- alts1 rs d, g <- alts1 rs d ] instance Serial Integer where - series d = [ toInteger (i :: Int) - | i <- series d ] - coseries d = [ f . (fromInteger :: Integer->Int) - | f <- series d ] + series d = [ toInteger (i :: Int) + | i <- series d ] + coseries rs d = [ f . (fromInteger :: Integer->Int) + | f <- coseries rs d ] newtype N a = N a + deriving (Eq, Ord) instance Show a => Show (N a) where show (N i) = show i instance (Integral a, Serial a) => Serial (N a) where - series d = map N [0..d'] - where - d' = fromInteger (toInteger d) - coseries d = [ \(N i) -> if i > 0 then f (N (i - 1)) - else z - | z <- alts0 d, f <- alts1 d ] + series d = map N [0..d'] + where + d' = fromInteger (toInteger d) + coseries rs d = [ \(N i) -> if i > 0 then f (N (i - 1)) + else z + | z <- alts0 rs d, f <- alts1 rs d ] type Nat = N Int type Natural = N Integer instance Serial Float where - series d = [ encodeFloat sig exp - | (sig,exp) <- series d, - odd sig || sig==0 && exp==0 ] - coseries d = [ f . decodeFloat - | f <- series d ] - + series d = [ encodeFloat sig exp + | (sig,exp) <- series d, + odd sig || sig==0 && exp==0 ] + coseries rs d = [ f . decodeFloat + | f <- coseries rs d ] + instance Serial Double where - series d = [ frac (x :: Float) - | x <- series d ] - coseries d = [ f . (frac :: Double->Float) - | f <- series d ] + series d = [ frac (x :: Float) + | x <- series d ] + coseries rs d = [ f . (frac :: Double->Float) + | f <- coseries rs d ] frac :: (Real a, Fractional a, Real b, Fractional b) => a -> b frac = fromRational . toRational instance Serial Char where - series d = take (d+1) ['a'..'z'] - coseries d = [ \c -> f (N (fromEnum c - fromEnum 'a')) - | f <- series d ] + series d = take (d+1) ['a'..'z'] + coseries rs d = [ \c -> f (N (fromEnum c - fromEnum 'a')) + | f <- coseries rs d ] instance (Serial a, Serial b) => Serial (a,b) where - series = series >< series - coseries = map uncurry . coseries + series = series >< series + coseries rs = map uncurry . (coseries $ coseries rs) instance (Serial a, Serial b, Serial c) => Serial (a,b,c) where - series = \d -> [(a,b,c) | (a,(b,c)) <- series d] - coseries = map uncurry3 . coseries + series = \d -> [(a,b,c) | (a,(b,c)) <- series d] + coseries rs = map uncurry3 . (coseries $ coseries $ coseries rs) instance (Serial a, Serial b, Serial c, Serial d) => Serial (a,b,c,d) where - series = \d -> [(a,b,c,d) | (a,(b,(c,d))) <- series d] - coseries = map uncurry4 . coseries + series = \d -> [(a,b,c,d) | (a,(b,(c,d))) <- series d] + coseries rs = map uncurry4 . (coseries $ coseries $ coseries $ coseries rs) uncurry3 :: (a->b->c->d) -> ((a,b,c)->d) uncurry3 f (x,y,z) = f x y z @@ -141,7 +143,7 @@ four :: Series a -> Series (a,a,a,a) four s = \d -> [(w,x,y,z) | (w,(x,(y,z))) <- (s >< s >< s >< s) d] -cons0 :: +cons0 :: a -> Series a cons0 c _ = [c] @@ -161,64 +163,73 @@ (a->b->c->d->e) -> Series e cons4 c d = [c w x y z | d > 0, (w,x,y,z) <- series (d-1)] -alts0 :: Serial a => +alts0 :: Series a -> Series a -alts0 d = series d +alts0 as d = as d -alts1 :: (Serial a, Serial b) => - Series (a->b) -alts1 d = if d > 0 then series (dec d) - else [\_ -> x | x <- series d] +alts1 :: Serial a => + Series b -> Series (a->b) +alts1 bs d = if d > 0 then coseries bs (dec d) + else [\_ -> x | x <- bs d] -alts2 :: (Serial a, Serial b, Serial c) => - Series (a->b->c) -alts2 d = if d > 0 then series (dec d) - else [\_ _ -> x | x <- series d] +alts2 :: (Serial a, Serial b) => + Series c -> Series (a->b->c) +alts2 cs d = if d > 0 then coseries (coseries cs) (dec d) + else [\_ _ -> x | x <- cs d] -alts3 :: (Serial a, Serial b, Serial c, Serial d) => - Series (a->b->c->d) -alts3 d = if d > 0 then series (dec d) - else [\_ _ _ -> x | x <- series d] +alts3 :: (Serial a, Serial b, Serial c) => + Series d -> Series (a->b->c->d) +alts3 ds d = if d > 0 then coseries (coseries (coseries ds)) (dec d) + else [\_ _ _ -> x | x <- ds d] -alts4 :: (Serial a, Serial b, Serial c, Serial d, Serial e) => - Series (a->b->c->d->e) -alts4 d = if d > 0 then series (dec d) - else [\_ _ _ _ -> x | x <- series d] +alts4 :: (Serial a, Serial b, Serial c, Serial d) => + Series e -> Series (a->b->c->d->e) +alts4 es d = if d > 0 then coseries (coseries (coseries (coseries es))) (dec d) + else [\_ _ _ _ -> x | x <- es d] instance Serial Bool where - series = cons0 True \/ cons0 False - coseries d = [ \x -> if x then b1 else b2 - | (b1,b2) <- series d ] + series = cons0 True \/ cons0 False + coseries rs d = [ \x -> if x then r1 else r2 + | r1 <- rs d, r2 <- rs d ] instance Serial a => Serial (Maybe a) where - series = cons0 Nothing \/ cons1 Just - coseries d = [ \m -> case m of + series = cons0 Nothing \/ cons1 Just + coseries rs d = [ \m -> case m of Nothing -> z Just x -> f x - | z <- alts0 d , - f <- alts1 d ] + | z <- alts0 rs d , + f <- alts1 rs d ] instance (Serial a, Serial b) => Serial (Either a b) where - series = cons1 Left \/ cons1 Right - coseries d = [ \e -> case e of - Left x -> f x - Right y -> g y - | f <- alts1 d , - g <- alts1 d ] + series = cons1 Left \/ cons1 Right + coseries rs d = [ \e -> case e of + Left x -> f x + Right y -> g y + | f <- alts1 rs d , + g <- alts1 rs d ] instance Serial a => Serial [a] where - series = cons0 [] \/ cons2 (:) - coseries d = [ \xs -> case xs of - [] -> y - (x:xs') -> f x xs' - | y <- alts0 d , - f <- alts2 d ] + series = cons0 [] \/ cons2 (:) + coseries rs d = [ \xs -> case xs of + [] -> y + (x:xs') -> f x xs' + | y <- alts0 rs d , + f <- alts2 rs d ] --- Warning: the coseries instance here may generate duplicates. +-- Thanks to Ralf Hinze for the definition of coseries +-- using the nest auxiliary. + instance (Serial a, Serial b) => Serial (a->b) where - series = coseries - coseries d = [ \f -> g [f x | x <- series d] - | g <- series d ] + series = coseries series + coseries rs d = + [ \ f -> g [ f a | a <- args ] + | g <- nest args d ] + where + args = series d + nest [] _ = [ \[] -> c + | c <- rs d ] + nest (a:as) _ = [ \(b:bs) -> f b bs + | f <- coseries (nest as) d ] -- For customising the depth measure. Use with care! @@ -236,7 +247,7 @@ -- show the extension of a function (in part, bounded both by -- the number and depth of arguments) instance (Serial a, Show a, Show b) => Show (a->b) where - show f = + show f = if maxarheight == 1 && sumarwidth + length ars * length "->;" < widthLimit then "{"++( @@ -249,7 +260,7 @@ | x <- series depthLimit ] maxarheight = maximum [ max (height a) (height r) | (a,r) <- ars ] - sumarwidth = sum [ length a + length r + sumarwidth = sum [ length a + length r | (a,r) <- ars] indent = unlines . map (" "++) . lines height = length . lines @@ -303,27 +314,50 @@ forAllElem :: (Show a, Testable b) => [a] -> (a->b) -> Property forAllElem xs = forAll (const xs) -thereExists :: Testable b => Series a -> (a->b) -> Property -thereExists xs f = Property $ \d -> Prop $ - [ Result - ( Just $ or [ all pass (evaluate (f x) d) - | x <- xs d ] ) - [] ] +existence :: (Show a, Testable b) => Bool -> Series a -> (a->b) -> Property +existence u xs f = Property existenceDepth where - pass (Result Nothing _) = True - pass (Result (Just b) _) = b + existenceDepth d = Prop [ Result (Just valid) arguments ] + where + witnesses = [ show x | x <- xs d, all pass (evaluate (f x) d) ] + valid = enough witnesses + enough = if u then unique else (not . null) + arguments = if valid then [] + else if null witnesses then ["non-existence"] + else "non-uniqueness" : take 2 witnesses -thereExistsElem :: Testable b => [a] -> (a->b) -> Property +unique :: [a] -> Bool +unique [_] = True +unique _ = False + +pass :: Result -> Bool +pass (Result Nothing _) = True +pass (Result (Just b) _) = b + +thereExists :: (Show a, Testable b) => Series a -> (a->b) -> Property +thereExists = existence False + +thereExists1 :: (Show a, Testable b) => Series a -> (a->b) -> Property +thereExists1 = existence True + +thereExistsElem :: (Show a, Testable b) => [a] -> (a->b) -> Property thereExistsElem xs = thereExists (const xs) -exists :: (Serial a, Testable b) => - (a->b) -> Property +thereExists1Elem :: (Show a, Testable b) => [a] -> (a->b) -> Property +thereExists1Elem xs = thereExists1 (const xs) + +exists :: (Show a, Serial a, Testable b) => (a->b) -> Property exists = thereExists series -existsDeeperBy :: (Serial a, Testable b) => - (Int->Int) -> (a->b) -> Property +exists1 :: (Show a, Serial a, Testable b) => (a->b) -> Property +exists1 = thereExists1 series + +existsDeeperBy :: (Show a, Serial a, Testable b) => (Int->Int) -> (a->b) -> Property existsDeeperBy f = thereExists (series . f) +exists1DeeperBy :: (Show a, Serial a, Testable b) => (Int->Int) -> (a->b) -> Property +exists1DeeperBy f = thereExists1 (series . f) + infixr 0 ==> (==>) :: Testable a => Bool -> a -> Property @@ -361,7 +395,7 @@ (\dTo -> when (ok && d < dTo) $ iter (d+1)) mdTo -check :: Bool -> Int -> Int -> Bool -> [Result] -> IO Bool +check :: Bool -> Integer -> Integer -> Bool -> [Result] -> IO Bool check i n x ok rs | null rs = do putStr (" Completed "++show n++" test(s)") putStrLn (if ok then " without failure." else ".") @@ -390,7 +424,7 @@ ( if (null reply || reply=="y") then action else return x ) -progressReport :: Bool -> Int -> Int -> IO () +progressReport :: Bool -> Integer -> Integer -> IO () progressReport i n x | n >= x = do when i $ ( putStr (n' ++ replicate (length n') '\b') >> hFlush stdout ) diff --git a/examples/binarytries/BinaryTries.hs b/examples/binarytries/BinaryTries.hs new file mode 100644 --- /dev/null +++ b/examples/binarytries/BinaryTries.hs @@ -0,0 +1,78 @@ +------------------------------------------------- +-- Binary tries representing sets of bitstrings. +-- A test module for SmallCheck. +-- Colin Runciman, May 2008. +------------------------------------------------- + +module BinaryTries where + +import Test.SmallCheck + +-- first representation + +data BT1 = E | B Bool BT1 BT1 deriving Show + +instance Serial BT1 where + series = cons0 E \/ cons3 B + + +contains1 :: BT1 -> [Bool] -> Bool +contains1 E _ = False +contains1 (B b _ _) [] = b +contains1 (B _ z _) (False:s) = contains1 z s +contains1 (B _ _ o) (True :s) = contains1 o s + +prop_uniqueBT1 :: ([Bool]->Bool) -> Property +prop_uniqueBT1 f = + exists1DeeperBy (+1) $ \bt -> contains1 bt === f + +-- second representation + +data BT2 = E2 | NE BT2' + deriving Show + +data BT2' = T | O Bool BT2' | I Bool BT2' | OI Bool BT2' BT2' + deriving Show + +instance Serial BT2 where + series = cons0 E2 \/ cons1 NE + +instance Serial BT2' where + series = cons0 T \/ cons2 O \/ cons2 I \/ cons3 OI + +contains2 :: BT2 -> [Bool] -> Bool +contains2 = contains1 . convert + +convert :: BT2 -> BT1 +convert E2 = E +convert (NE bt') = convert' bt' + +convert' :: BT2' -> BT1 +convert' T = B True E E +convert' (O b z') = B b (convert' z') E +convert' (I b o' ) = B b E (convert' o') +convert' (OI b o' z') = B b (convert' z') (convert' o') + +prop_uniqueBT2 :: ([Bool]->Bool) -> Property +prop_uniqueBT2 f = + exists1DeeperBy (+1) $ \bt -> contains2 bt === f + +(===) :: Eq b => (a->b) -> (a->b) -> a -> Bool +f === g = \x -> f x == g x + +main :: IO () +main = do + test1 "\\f -> exists1DeeperBy (+1) $ \\bt1 -> contains1 bt1 === f ?" + prop_uniqueBT1 + test1 "\\f -> exists1DeeperBy (+1) $ \\bt1 -> contains2 bt2 === f ?" + prop_uniqueBT2 + +test1 :: Testable a => String -> a -> IO () +test1 s t = do + rule + putStrLn s + rule + smallCheck 2 t + where + rule = putStrLn "----------------------------------------------------------" + diff --git a/examples/binarytries/README b/examples/binarytries/README new file mode 100644 --- /dev/null +++ b/examples/binarytries/README @@ -0,0 +1,10 @@ +First see ../../README. + +In this directory, BinaryTries.hs illustrates properties quantified +over functions and requiring the unique existence of a data-structure. +Two different trie representations are defined for sets of bitstrings. +The properties state that each set has a unique representation as a +trie -- true for the second representation, but not for the first. +The properties are specified using functions with boolean results +as a pure representation of sets, independent of any data structure. +Compile or interpret BinaryTries.main for the self-introducing tests. diff --git a/examples/circuits/BitAdd.hs b/examples/circuits/BitAdd.hs new file mode 100644 --- /dev/null +++ b/examples/circuits/BitAdd.hs @@ -0,0 +1,23 @@ +import Test.SmallCheck + +and2 (a,b) = a && b + +xor2 (a,b) = a /= b + +halfAdd (a,b) = (sum,carry) + where sum = xor2 (a,b) + carry = and2 (a,b) + +bit False = 0 +bit True = 1 + +num [] = 0 +num (a:as) = bit a + 2 * num as + +bitAdd a [] = [a] +bitAdd a (b:bs) = s : bitAdd c bs + where (s,c) = halfAdd (a,b) + +prop_bitAdd a as = num (bitAdd a as) == bit a + num as + +main = smallCheck 8 prop_bitAdd diff --git a/examples/circuits/Mux.hs b/examples/circuits/Mux.hs new file mode 100644 --- /dev/null +++ b/examples/circuits/Mux.hs @@ -0,0 +1,113 @@ +import List +import Test.SmallCheck + +type Bit = Bool + +unaryMux :: [Bit] -> [[Bit]] -> [Bit] +unaryMux sel xs = map (tree (||)) + $ transpose + $ zipWith (\s x -> map (s &&) x) sel xs + +tree :: (a -> a -> a) -> [a] -> a +tree f [x] = x +tree f (x:y:ys) = tree f (ys ++ [f x y]) + +decode :: [Bit] -> [Bit] +decode [] = [True] +decode [x] = [not x,x] +decode (x:xs) = concatMap (\y -> [not x && y,x && y]) rest + where + rest = decode xs + +binaryMux :: [Bit] -> [[Bit]] -> [Bit] +binaryMux sel xs = unaryMux (decode sel) xs + +bitMux2 :: Bit -> Bit -> Bit -> Bit +bitMux2 sel x y = (sel && y) || (not sel && x) + +muxf5 = bitMux2 + +muxf6 = bitMux2 + +busMux2 :: Bit -> [Bit] -> [Bit] -> [Bit] +busMux2 sel xs ys = zipWith (bitMux2 sel) xs ys + +bitMux8 :: [Bit] -> [Bit] -> Bit +bitMux8 _ [x] = x +bitMux8 (s0:_) [x0,x1] + = bitMux2 s0 x0 x1 +bitMux8 (s0:s1:_) [x0,x1,x2,x3] + = muxf5 s1 (bitMux8 [s0] [x0,x1]) (bitMux8 [s0] [x2,x3]) +bitMux8 (s0:s1:s2:_) [x0,x1,x2,x3,x4,x5,x6,x7] + = muxf6 s2 (bitMux8 [s0,s1] [x0,x1,x2,x3]) + (bitMux8 [s0,s1] [x4,x5,x6,x7]) +bitMux8 sels xs = bitMux8 (take n sels) (pad m xs) + where + n = log2 (length xs) + m = 2 ^ n + +log2 :: Int -> Int +log2 n = length (takeWhile (< n) (iterate (*2) 1)) + +pad :: Int -> [Bit] -> [Bit] +pad n xs | m > n = xs + | otherwise = xs ++ replicate (n-m) False + where + m = length xs + +bitMux :: [Bit] -> [Bit] -> Bit +bitMux sels [x] = x +bitMux sels xs = bitMux (drop 3 sels) ys + where + ys = zipWith bitMux8 (repeat (take 3 sels)) (groupn 8 xs) + + +groupn :: Int -> [a] -> [[a]] +groupn n [] = [] +groupn n xs = take n xs : groupn n (drop n xs) + +binaryMux' :: [Bit] -> [[Bit]] -> [Bit] +binaryMux' sel = map (bitMux sel) . transpose + +num :: [Bit] -> Int +num [] = 0 +num (a:as) = fromEnum a + 2 * num as + +-- Property 0: binaryMux is correct + +prop_mux0 sel xs = length xs == 2 ^ length sel + && all ((== length (head xs)) . length) xs + ==> binaryMux sel xs == xs !! num sel + +-- But this is inefficient as most of the test cases do not meet the +-- antecedent. Instead, we can define a custom generator in which +-- the number of inputs grows exponentially (i.e. 2^) with respect to +-- the width of the address word. + +newtype Word = Word { bits :: [Bit] } + deriving Show + +newtype File = File { wrds :: [Word] } + deriving Show + +instance Serial Word where + series n = map Word $ sequence (replicate n [False,True]) + +instance Serial File where + series n = map File $ sequence $ replicate (2^n) ws + where + ws = series n :: [Word] + +prop_mux0' sel xs = xs' !! num sel' == binaryMux sel' xs' + where + sel' = bits sel + xs' = map bits (wrds xs) + +-- Property 1: binaryMux' is correct + +prop_mux1 sel xs = xs' !! num sel' == binaryMux' sel' xs' + where + sel' = bits sel + xs' = map bits (wrds xs) + +main = smallCheck 2 prop_mux1 diff --git a/examples/circuits/README b/examples/circuits/README new file mode 100644 --- /dev/null +++ b/examples/circuits/README @@ -0,0 +1,30 @@ +First see ../../README. + +The programs in this directory define a number of different circuits. +Some of these were originally written in Lava and were used to generate +circuit netlists for external synthesis tools and propositional logic for +external theorem provers. They have been slightly adapted as examples +for SmallCheck, so that they do not depend on Lava. + +BitAdd.hs defines a trivial circuit that takes two inputs, a bit and a +bit-vector (i.e. a list of bits), and returns a bit-vector containing +the sum of the two. Using SmallCheck, it is straightforward to verify +that the circuit behaves correctly for all bit-vector inputs up to the +given size. + +Sad.hs defines a more complicated circuit that works over two lists of +lists of bits, but verification with SmallCheck is just as simple and +useful as before. + +Mux.hs defines a simple multiplexor and a more complicated variant that +is optimised for Xilinx FPGAs. Originally, the correctness of the more +complicated version was argued by verifying its equivalence with the +simpler version using an external SAT solver. However, using SmallCheck, +more general properties can be expressed, and so each circuit can be +verified independently in terms of Haskell's list indexing operator (!!). +The correctness properties are again easy to express in SmallCheck, +but their antecedents filter out so many test cases as to make them +inefficient. This problem is resolved by writing a custom test-case +generator using SmallCheck's "Serial" class. + +Matthew Naylor, University of York, 22nd Jan 2007. diff --git a/examples/circuits/Sad.hs b/examples/circuits/Sad.hs new file mode 100644 --- /dev/null +++ b/examples/circuits/Sad.hs @@ -0,0 +1,96 @@ +import Test.SmallCheck + +-- We take the following specification for the sum of absolute +-- differences, and develop a circuit generator that has the same +-- behaviour. + +sad :: [Int] -> [Int] -> Int +sad xs ys = sum (map abs (zipWith (-) xs ys)) + +type Bit = Bool + +low :: Bit +low = False + +high :: Bit +high = True + +inv :: Bit -> Bit +inv a = not a + +and2 :: Bit -> Bit -> Bit +and2 a b = a && b +or2 a b = a || b +xor2 a b = a /= b +xnor2 a b = a == b + +mux2 :: Bit -> Bit -> Bit -> Bit +mux2 sel a b = (sel && b) || (not sel && a) + +bitAdd :: Bit -> [Bit] -> [Bit] +bitAdd x [] = [x] +bitAdd x (y:ys) = let (sum,carry) = halfAdd x y + in sum:bitAdd carry ys + +halfAdd x y = (xor2 x y,and2 x y) + +binAdd :: [Bit] -> [Bit] -> [Bit] +binAdd xs ys = binAdd' low xs ys + +binAdd' cin [] [] = [cin] +binAdd' cin (x:xs) [] = bitAdd cin (x:xs) +binAdd' cin [] (y:ys) = bitAdd cin (y:ys) +binAdd' cin (x:xs) (y:ys) = let (sum,cout) = fullAdd cin x y + in sum:binAdd' cout xs ys + +fullAdd cin a b = let (s0,c0) = halfAdd a b + (s1,c1) = halfAdd cin s0 + in (s1,xor2 c0 c1) + +binGte :: [Bit] -> [Bit] -> Bit +binGte xs ys = binGte' high xs ys + +binGte' gin [] [] = gin +binGte' gin (x:xs) [] = orl (gin:x:xs) +binGte' gin [] (y:ys) = and2 gin (orl (y:ys)) +binGte' gin (x:xs) (y:ys) = let gout = gteCell gin x y + in binGte' gout xs ys + +gteCell gin x y = mux2 (xnor2 x y) x gin + +orl :: [Bit] -> Bit +orl xs = tree or2 low xs + +binDiff :: [Bit] -> [Bit] -> [Bit] +binDiff xs ys = let xs' = pad (length ys) xs + ys' = pad (length xs) ys + gte = binGte xs' ys' + xs'' = map (xor2 (inv gte)) xs' + ys'' = map (xor2 gte) ys' + in init (binAdd' high xs'' ys'') + +pad :: Int -> [Bit] -> [Bit] +pad n xs | m > n = xs + | otherwise = xs ++ replicate (n-m) False + where + m = length xs + +tree :: (a -> a -> a) -> a -> [a] -> a +tree f z [] = z +tree f z [x] = x +tree f z (x:y:ys) = tree f z (ys ++ [f x y]) + +binSum :: [[Bit]] -> [Bit] +binSum xs = tree binAdd [] xs + +binSad :: [[Bit]] -> [[Bit]] -> [Bit] +binSad xs ys = binSum (zipWith binDiff xs ys) + +num :: [Bit] -> Int +num [] = 0 +num (a:as) = fromEnum a + 2 * num as + +prop_binSad xs ys = sad (map num xs) (map num ys) + == num (binSad xs ys) + +main = smallCheck 3 prop_binSad diff --git a/examples/imperative/Properties.hs b/examples/imperative/Properties.hs --- a/examples/imperative/Properties.hs +++ b/examples/imperative/Properties.hs @@ -126,7 +126,7 @@ series = const [I2 op | op <- [Add, Sub, Mul, Div, Mod]] newtype BExpr = B Expr - + instance Serial BExpr where series = cons1 uno' \/ cons3 duo' diff --git a/examples/listy/README b/examples/listy/README --- a/examples/listy/README +++ b/examples/listy/README @@ -1,5 +1,8 @@ First see ../../README. -In this directory, compile or interpret ListProps.main (SmallCheck -is the only other module required) for a small selection of -self-introducing tests of list-processing functions. +In this directory, compile or interpret ListProps.main (SmallCheck is +the only other module required) for a small selection of self-introducing +tests of list-processing functions. + +The definition of isPrefix is deliberately incorrect: the completeness +property still holds, but the existential soundness property fails. diff --git a/examples/logical/LogicProps.hs b/examples/logical/LogicProps.hs --- a/examples/logical/LogicProps.hs +++ b/examples/logical/LogicProps.hs @@ -8,7 +8,7 @@ import Test.SmallCheck -import Data.List (nub) +import List (nub) data Prop = Var Name | Not Prop @@ -41,7 +41,7 @@ eval (Not p) env = not (eval p env) eval (And p q) env = eval p env && eval q env eval (Or p q) env = eval p env || eval q env -eval (Imp p q) env = eval p env <= eval q env +eval (Imp p q) env = eval p env <= eval q env envsFor :: Prop -> [Env] envsFor p = foldr bind [const False] (nub (varsOf p)) @@ -62,11 +62,11 @@ satisfiable :: Prop -> Bool satisfiable p = any (eval p) (envsFor p) -instance Serial Name where - series = cons0 P \/ cons0 Q \/ cons0 R - coseries d = [ \n -> case n of - P -> x ; Q -> y ; R -> z - | x <- alts0 d, y <- alts0 d, z <- alts0 d ] +instance Serial Name where + series = cons0 P \/ cons0 Q \/ cons0 R + coseries rs d = [ \n -> case n of + P -> x ; Q -> y ; R -> z + | x <- alts0 rs d, y <- alts0 rs d, z <- alts0 rs d ] instance Serial Prop where series = cons1 Var @@ -86,7 +86,7 @@ not (tautologous p) ==> exists (\e -> not $ eval p e) prop_sat1 :: Prop -> Env -> Property -prop_sat1 p e = +prop_sat1 p e = eval p e ==> satisfiable p prop_sat2 :: Prop -> Property diff --git a/examples/numeric/NumProps.hs b/examples/numeric/NumProps.hs --- a/examples/numeric/NumProps.hs +++ b/examples/numeric/NumProps.hs @@ -1,9 +1,8 @@ ------------------------------------------- --- Illustrating numerics in SmallCheck 0.2 +---------------------------------------- +-- Illustrating numerics in SmallCheck -- Colin Runciman, November 2006. ------------------------------------------- - -module NumProps where +-- Modified for SmallCheck 0.3, May 2008 +---------------------------------------- import Test.SmallCheck @@ -24,7 +23,8 @@ prop_primes2 :: Nat -> Property prop_primes2 (N n) = - n > 0 ==> exists $ \exponents -> + n > 0 ==> exists1 $ \exponents -> + (null exponents || last exponents /= N 0) && n == product (zipWith power primes exponents) where power p (N e) = product (replicate e p) @@ -42,7 +42,8 @@ test1 "\\(N n) -> n > 1 ==> forAll (`take` primes) $ \\p ->\n\ \ p `mod` n > 0 || n == p" prop_primes1 - test1 "\\(N n) -> n > 0 ==> exists $ \\exponents ->\n\ + test1 "\\(N n) -> n > 0 ==> exists1 $ \\exponents ->\n\ + \ (null exponents || last exponents /= N 0) &&\n\ \ n == product (zipWith power primes exponents)" prop_primes2 test1 "\\x -> exp (log x) == x" diff --git a/examples/numeric/README b/examples/numeric/README --- a/examples/numeric/README +++ b/examples/numeric/README @@ -7,3 +7,8 @@ the only other module required) and run main for a small selection of self-introducing tests -- a couple about natural numbers and primes, and a couple about floating point numbers. + +For version 0.3 the second property about primes has been strengthened +by making the existence unique. The restriction on the exponent list +was prompted by reports of non-uniqueness when the 'exists1' version +was first tested. diff --git a/examples/regular/Regular.hs b/examples/regular/Regular.hs --- a/examples/regular/Regular.hs +++ b/examples/regular/Regular.hs @@ -1,8 +1,9 @@ module Regular where -import Data.Char (isAlpha) -import Data.List (intersperse) -import Control.Monad (liftM) +import Char (isAlpha) +import List (intersperse) +import Monad (liftM) + import Test.SmallCheck -- A data type of regular expressions. @@ -10,10 +11,10 @@ data RE = Emp | Lam | Sym Char - | Alt [RE] + | Alt [RE] | Cat [RE] - | Rep RE - deriving Eq + | Rep RE + deriving Eq isEmp, isLam, isSym, isCat, isAlt, isRep :: RE -> Bool isEmp Emp = True @@ -72,7 +73,7 @@ rest (v :s) ((c:a):as) = if isAlpha v then rest s (((Sym v:c):a):as) else if null as then (a2re (c:a),v:s) else wrong - + a2re :: [[RE]] -> RE a2re = alt . reverse . map (cat . reverse) diff --git a/smallcheck.cabal b/smallcheck.cabal --- a/smallcheck.cabal +++ b/smallcheck.cabal @@ -1,5 +1,5 @@ Name: smallcheck -Version: 0.2.1 +Version: 0.4 License: BSD3 License-File: LICENSE Author: Colin Runciman @@ -12,27 +12,8 @@ instead of testing for a sample of randomly generated values, SmallCheck tests properties for all the finitely many values up to some depth, progressively increasing the depth used. - . - Folk-law: if there is any case in which a program - fails, there is almost always a simple one. - . - Corollary: if a program does not fail in any - simple case, it almost never fails. - . - Other possible sales pitches: - . - * write test generators for your own types more easily - . - * be sure any counter-examples found are minimal - . - * write properties using existentials as well as universals - . - * establish complete coverage of a defined test-space - . - * display counter-examples of functional type -Homepage: http://www.cs.york.ac.uk/fp/smallcheck0.2.tar -Build-Depends: base +Build-Depends: base, haskell98 Build-Type: Simple Extra-source-files: examples/numeric/NumProps.hs, examples/logical/LogicProps.hs, @@ -40,9 +21,12 @@ examples/imperative/Machine.hs, examples/imperative/Behaviour.hs, examples/imperative/Properties.hs, examples/imperative/Value.hs, examples/imperative/StackMap.hs, examples/imperative/Compiler.hs, - examples/listy/ListProps.hs, examples/regular/Regular.hs + examples/listy/ListProps.hs, examples/regular/Regular.hs, + examples/circuits/BitAdd.hs, examples/circuits/Mux.hs, examples/circuits/Sad.hs, + examples/binarytries/BinaryTries.hs Data-files: examples/numeric/README, examples/logical/README, examples/imperative/README, - examples/listy/README, examples/regular/README, README + examples/listy/README, examples/regular/README, examples/circuits/README, + examples/binarytries/README, README Exposed-modules: Test.SmallCheck