packages feed

smallcheck 0.2.1 → 0.4

raw patch · 16 files changed

+604/−175 lines, 16 filesdep +haskell98setup-changednew-uploader

Dependencies added: haskell98

Files

README view
@@ -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<N> 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<N>' family now take a+series argument -- here rs.  In the coseries definitions we simply pass+on rs as series argument in each 'alts<N>' 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<N>' 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
Setup.hs view
Test/SmallCheck.hs view
@@ -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)  ------------------ <Series of depth-bounded values> ----------------- @@ -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 )
+ examples/binarytries/BinaryTries.hs view
@@ -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 "----------------------------------------------------------"+
+ examples/binarytries/README view
@@ -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.
+ examples/circuits/BitAdd.hs view
@@ -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
+ examples/circuits/Mux.hs view
@@ -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
+ examples/circuits/README view
@@ -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.
+ examples/circuits/Sad.hs view
@@ -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
examples/imperative/Properties.hs view
@@ -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'
examples/listy/README view
@@ -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.
examples/logical/LogicProps.hs view
@@ -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
examples/numeric/NumProps.hs view
@@ -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"
examples/numeric/README view
@@ -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.
examples/regular/Regular.hs view
@@ -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) 
smallcheck.cabal view
@@ -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