packages feed

smallcheck (empty) → 0.2.1

raw patch · 22 files changed

+1620/−0 lines, 22 filesdep +basesetup-changed

Dependencies added: base

Files

+ LICENSE view
@@ -0,0 +1,28 @@+All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions+are met:++1. Redistributions of source code must retain the above copyright+   notice, this list of conditions and the following disclaimer.++2. Redistributions in binary form must reproduce the above copyright+   notice, this list of conditions and the following disclaimer in the+   documentation and/or other materials provided with the distribution.++3. Neither the name of the author nor the names of his contributors+   may be used to endorse or promote products derived from this software+   without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``AS IS'' AND ANY EXPRESS OR+IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE+DISCLAIMED.  IN NO EVENT SHALL THE AUTHORS OR CONTRIBUTORS BE LIABLE FOR+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL+DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS+OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION)+HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT,+STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN+ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE+POSSIBILITY OF SUCH DAMAGE.
+ README view
@@ -0,0 +1,257 @@+---------------------------------------------------------------+SmallCheck: another lightweight testing library in Haskell.+Version 0.2, November 2006+Colin Runciman, University of York UK++After QuickCheck, by Koen Claessen and John Hughes (2000-2004).+---------------------------------------------------------------++If you are a Haskell programmer and a QuickCheck user do you ever wish+you could:++* write test generators for your own types more easily?+* be sure that 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?+* guarantee repeatable test results?++If so, try SmallCheck! This note should be enough to  get you started,+assuming some prior experience with QuickCheck.++Similarities and Differences+----------------------------++In many ways SmallCheck is very similar to QuickCheck.  It uses the+idea of type-based generators for test data, and the way testable+properties are expressed is closely based on the QuickCheck approach. Like+QuickCheck, SmallCheck tests whether properties hold for finite completely+defined values at specific types, and reports counter-examples.++The big difference is that instead of using a sample of randomly generated+values, SmallCheck tests properties for all the finitely many values+up to some depth, progressively increasing the depth used.  For data+values, depth means depth of construction.  For functional values, it+is a measure combining the depth to which arguments may be evaluated+and the depth of possible results.++Generators+----------++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+it is a more straightforward task, using SmallCheck's cons<N> family+of generic combinators where N is constructor arity.  For example:++data Tree a = Null | Fork Tree a Tree++instance Serial a => Serial (Tree a) where+  series = cons0 Null \/ cons3 Fork++The default interpretation of depth for datatypes is the depth of nested+construction: constructor functions, including those for newtypes, build+results with depth one greater than their deepest argument.  But this+default can be over-ridden by composing a cons<N> application with an+application of 'depth', like this:++newtype Light a = Light a++instance Serial a => Serial (Light a) where+  series = cons1 Light . depth 0++The depth of Light x is just the depth of x.++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 d = [ \l -> case l of+                       Light x -> f x+               |  f <- (alts1 . depth 0) d ]++Properties+----------++SmallCheck's testable properties are closely based on those of QuickCheck+but with the introduction of existential quantifiers.  Suppose we have+defined a function++isPrefix :: Eq a => [a] -> [a] -> Bool++and wish to specify it by some suitable property.  Using QuickCheck we+might define++prop_isPrefix1 :: String -> String -> Bool+prop_isPrefix1 xs ys = isPrefix xs (xs++ys)++where xs and ys are universally quantified.  This property is necessary+but not sufficient for a correct isPrefix.  For example, it is satisfied+by the function that always returns True!  We can test the same property+using SmallCheck.  But we can also test the following property, which+involves an existentially quantified variable:++prop_isPrefix2 :: String -> String -> Bool+prop_isPrefix2 xs ys = isPrefix xs ys ==>+                         exists $ \xs' -> ys == xs++xs'++The default testing of existentials is bounded by the same depth as their+context, here the depth-bound for xs and ys.  This rule has important+consequences.  Just as a universal property may be satisfied when the+depth bound is shallow but fail when it is deeper, so the reverse may be+true for an existential property.  So when testing properties involving+existentials it may be appropriate to try deeper testing after a shallow+failure. However, sometimes the default same-depth-bound interpretation+of existential properties can make testing of a valid property fail at+all depths.  Here is a contrived but illustrative example:++prop_append1 :: [Bool] -> [Bool] -> Property+prop_append1 xs ys = exists $ \zs -> zs == xs++ys++Customised variants of 'exists' are handy in such circumstances.+For example, 'existsDeeperBy' transforms the depth bound by a given+Int->Int function:++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.++Pragmatics of ==>+-----------------++As in QuickCheck, the ==> operator can be used to express a restricting+condition under which a property should hold.  For example, testing a+propositional-logic module (see examples/logical), we might define:++prop_tautEval :: Proposition -> Environment -> Property+prop_tautEval p e =+  tautology p ==> eval p e++But here is an alternative definition:++prop_tautEval :: Proposition -> Property+prop_taut p =+  tautology p ==> \e -> eval p e++The first definition generates p and e for each test, whereas the second+only generates e if the tautology p holds.  This difference is not great+in QuickCheck where single random values are generated, but in SmallCheck+the second definition is far better as the test-space is reduced from+P*E to T'+T*E where P, T, T' and E are the numbers of propositions,+tautologies, non-tautologies and environments.++Testing+-------++Just as QuickCheck has a top-level function 'quickCheck' so SmallCheck+has 'smallCheck d'.++smallCheck  :: Testable a => Int -> a -> IO ()++It runs series of tests using depth bounds 0..d, stopping if any test+fails, and prints a summary report or a counter-example. The variant:++smallCheckI :: Testable a =>        a -> IO ()+ +is interactive. Instead of requiring a maximum-depth argument, it invites+the user to decide whether to do deeper tests and whether to continue+after a failure.  The interface is low-tech: y<return> (or just <return>)+means "yes", anything else means "no".  For example:++haskell> smallCheckI prop_append1+Depth 0:+  Completed 1 test(s) without failure.+  Deeper? y+Depth 1:+  Failed test no. 5. Test values follow.+  [True]+  [True]+  Continue? n+  Deeper? n+haskell>++Having methods to generate series of all (depth-bounded) values of+an argument type, SmallCheck can give at least partial information+about the extension of a function.  For example, if we test the+property++prop_assoc op =+  \x y z -> (x `op` y) `op` z == x `op` (y `op` z)+  where+  typeInfo = op :: Bool -> Bool -> Bool++the result is shown as follows.++haskell> smallCheckI prop_assoc+Depth 0:+  Failed test no. 22. Test values follow.+  {True->{True->True;False->True};False->{True->False;False->True}}+  False+  True+  False++Large Test Spaces+-----------------++Using the standard generic scheme to define series of test value, it+often turns out that at some small depth d the 10,000-100,000 tests+are quickly checked, but at depth d+1 it is infeasible to complete+the billions of tests.  There are ways to reduce some dimensions of+the search space so that other dimensions can be tested more deeply:+for example, cut the scope of quantifiers to a small fixed domain+(forAllElem, thereExistsElem), use newtypes to define restricted series+for some data types (see the 'examples' directory) or assign depth >1+to some constructors.++Function spaces grow exponentially in relation to their result and+argument spaces.  Even with a depth bound, testing all functional+arguments is a challenge.  Keep base-types as small as possible.+For example, try testing higher-order polymorphic functions over their+() or Bool instances.++Version 0.1+-----------++The differences from 0.0 are two fixes (space-fault, output buffering),+an 'unsafe' but sometimes useful Testable (IO a) instance and additional+examples.++Version 0.2+-----------++The 'smallCheck' driver now takes an argument d and runs test series+at depths 0..d without interaction, stopping if any test fails.+The interactive variant is still available as 'smallCheckI'.  All+Prelude numeric types now have Serial instances, including floating-point+types. Serial types Nat and Natural are also defined.  Examples extended.++Final Notes+-----------++The name is intended to acknowledge QuickCheck, not to suggest that+SmallCheck is a tool of equal refinement.++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:++http://www.cs.york.ac.uk/fp/smallcheck0.2.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.++Colin.Runciman@cs.york.ac.uk+6 November 2006
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ Test/SmallCheck.hs view
@@ -0,0 +1,398 @@+---------------------------------------------------------------------+-- SmallCheck: another lightweight testing library.+-- Colin Runciman, August 2006+-- Version 0.2 (November 2006)+--+-- After QuickCheck, by Koen Claessen and John Hughes (2000-2004).+---------------------------------------------------------------------++module Test.SmallCheck (+  smallCheck, smallCheckI, depthCheck, test,+  Property, Testable,+  forAll, forAllElem,+  exists, existsDeeperBy, thereExists, thereExistsElem,+  (==>),+  Series, Serial(..),+  (\/), (><), two, three, four,+  cons0, cons1, cons2, cons3, cons4,+  alts0, alts1, alts2, alts3, alts4,+  N(..), Nat, Natural,+  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)++------------------ <Series of depth-bounded values> -----------------++-- Series arguments should be interpreted as a depth bound (>=0)+-- Series results should have finite length++type Series a = Int -> [a]++-- sum+infixr 7 \/+(\/) :: Series a -> Series a -> Series a+s1 \/ s2 = \d -> s1 d ++ s2 d++-- product+infixr 8 ><+(><) :: Series a -> Series b -> Series (a,b)+s1 >< s2 = \d -> [(x,y) | x <- s1 d, y <- s2 d]++------------------- <methods for type enumeration> ------------------++-- enumerated data values should be finite and fully defined+-- enumerated functional values should be total and strict++-- bounds:+-- 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)++instance Serial () where+  series   _ = [()]+  coseries d = [ \() -> b+               | b <- series 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 ]++instance Serial Integer where+  series   d = [ toInteger (i :: Int)+               | i <- series d ]+  coseries d = [ f . (fromInteger :: Integer->Int)+               | f <- series d ]++newtype N a = N a++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 ]++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 ]++instance Serial Double where+  series   d = [ frac (x :: Float)+               | x <- series d ]+  coseries d = [ f . (frac :: Double->Float)+               | f <- series 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 ]++instance (Serial a, Serial b) =>+         Serial (a,b) where+  series   = series >< series+  coseries = map uncurry . coseries++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++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++uncurry3 :: (a->b->c->d) -> ((a,b,c)->d)+uncurry3 f (x,y,z) = f x y z++uncurry4 :: (a->b->c->d->e) -> ((a,b,c,d)->e)+uncurry4 f (w,x,y,z) = f w x y z++two   :: Series a -> Series (a,a)+two   s = s >< s++three :: Series a -> Series (a,a,a)+three s = \d -> [(x,y,z) | (x,(y,z)) <- (s >< s >< s) d]++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 ::+         a -> Series a+cons0 c _ = [c]++cons1 :: Serial a =>+         (a->b) -> Series b+cons1 c d = [c z | d > 0, z <- series (d-1)]++cons2 :: (Serial a, Serial b) =>+         (a->b->c) -> Series c+cons2 c d = [c y z | d > 0, (y,z) <- series (d-1)]++cons3 :: (Serial a, Serial b, Serial c) =>+         (a->b->c->d) -> Series d+cons3 c d = [c x y z | d > 0, (x,y,z) <- series (d-1)]++cons4 :: (Serial a, Serial b, Serial c, Serial d) =>+         (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 =>+            Series a+alts0 d = series d++alts1 ::  (Serial a, Serial b) =>+            Series (a->b)+alts1 d = if d > 0 then series (dec d)+          else [\_ -> x | x <- series 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]++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]++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]++instance Serial Bool where+  series     = cons0 True \/ cons0 False+  coseries d = [ \x -> if x then b1 else b2+               | (b1,b2) <- series d ]++instance Serial a => Serial (Maybe a) where+  series     = cons0 Nothing \/ cons1 Just+  coseries d = [ \m -> case m of+                       Nothing -> z+                       Just x  -> f x+               |  z <- alts0 d ,+                  f <- alts1 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 ]++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 ]++-- Warning: the coseries instance here may generate duplicates.+instance (Serial a, Serial b) => Serial (a->b) where+  series = coseries+  coseries d = [ \f -> g [f x | x <- series d]+               | g <- series d ]++-- For customising the depth measure.  Use with care!++depth :: Int -> Int -> Int+depth d d' | d >= 0    = d'+1-d+           | otherwise = error "SmallCheck.depth: argument < 0"++dec :: Int -> Int+dec d | d > 0     = d-1+      | otherwise = error "SmallCheck.dec: argument <= 0"++inc :: Int -> Int+inc d = d+1++-- 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 =+    if maxarheight == 1+    && sumarwidth + length ars * length "->;" < widthLimit then+      "{"++(+      concat $ intersperse ";" $ [a++"->"++r | (a,r) <- ars]+      )++"}"+    else+      concat $ [a++"->\n"++indent r | (a,r) <- ars]+    where+    ars = take lengthLimit [ (show x, show (f x))+                           | x <- series depthLimit ]+    maxarheight = maximum  [ max (height a) (height r)+                           | (a,r) <- ars ]+    sumarwidth = sum       [ length a + length r+                           | (a,r) <- ars]+    indent = unlines . map ("  "++) . lines+    height = length . lines+    (widthLimit,lengthLimit,depthLimit) = (80,20,3)::(Int,Int,Int)++---------------- <properties and their evaluation> ------------------++-- adapted from QuickCheck originals: here results come in lists,+-- properties have depth arguments, stamps (for classifying random+-- tests) are omitted, existentials are introduced++newtype PR = Prop [Result]++data Result = Result {ok :: Maybe Bool, arguments :: [String]}++nothing :: Result+nothing = Result {ok = Nothing, arguments = []}++result :: Result -> PR+result res = Prop [res]++newtype Property = Property (Int -> PR)++class Testable a where+  property :: a -> Int -> PR++instance Testable Bool where+  property b _ = Prop [Result (Just b) []]++instance Testable PR where+  property prop _ = prop++instance (Serial a, Show a, Testable b) => Testable (a->b) where+  property f = f' where Property f' = forAll series f++instance Testable Property where+  property (Property f) d = f d++-- For testing properties involving IO.  Unsafe, so use with care!+instance Testable a => Testable (IO a) where+  property = property . unsafePerformIO++evaluate :: Testable a => a -> Series Result+evaluate x d = rs where Prop rs = property x d++forAll :: (Show a, Testable b) => Series a -> (a->b) -> Property+forAll xs f = Property $ \d -> Prop $+  [ r{arguments = show x : arguments r}+  | x <- xs d, r <- evaluate (f x) d ]++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 ] )+      [] ]+  where+  pass (Result Nothing _)  = True+  pass (Result (Just b) _) = b++thereExistsElem :: Testable b => [a] -> (a->b) -> Property+thereExistsElem xs = thereExists (const xs)++exists :: (Serial a, Testable b) =>+            (a->b) -> Property+exists = thereExists series++existsDeeperBy :: (Serial a, Testable b) =>+                    (Int->Int) -> (a->b) -> Property+existsDeeperBy f = thereExists (series . f)++infixr 0 ==>++(==>) :: Testable a => Bool -> a -> Property+True ==>  x = Property (property x)+False ==> x = Property (const (result nothing))++--------------------- <top-level test drivers> ----------------------++-- similar in spirit to QuickCheck but with iterative deepening++test :: Testable a => a -> IO ()+test = smallCheckI++-- test for values of depths 0..d stopping when a property+-- fails or when it has been checked for all these values+smallCheck :: Testable a => Int -> a -> IO ()+smallCheck d = iterCheck 0 (Just d)++-- interactive variant, asking the user whether testing should+-- continue/go deeper after a failure/completed iteration+smallCheckI :: Testable a => a -> IO ()+smallCheckI = iterCheck 0 Nothing++depthCheck :: Testable a => Int -> a -> IO ()+depthCheck d = iterCheck d (Just d)++iterCheck :: Testable a => Int -> Maybe Int -> a -> IO ()+iterCheck dFrom mdTo t = iter dFrom+  where+  iter d = do+    putStrLn ("Depth "++show d++":")+    let Prop results = property t d+    ok <- check (mdTo==Nothing) 0 0 True results+    maybe (whenUserWishes "  Deeper" () $ iter (d+1))+          (\dTo -> when (ok && d < dTo) $ iter (d+1))+          mdTo++check :: Bool -> Int -> Int -> 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 ".")+  when (x > 0) $+    putStrLn ("  But "++show x++" did not meet ==> condition.")+  return ok+check i n x ok (Result Nothing _ : rs) = do+  progressReport i n x+  check i (n+1) (x+1) ok rs+check i n x f (Result (Just True) _ : rs) = do+  progressReport i n x+  check i (n+1) x f rs+check i n x f (Result (Just False) args : rs) = do+  putStrLn ("  Failed test no. "++show (n+1)++". Test values follow.")+  mapM_ (putStrLn . ("  "++)) args+  ( if i then+      whenUserWishes "  Continue" False $ check i (n+1) x False rs+    else+      return False )++whenUserWishes :: String -> a -> IO a -> IO a+whenUserWishes wish x action = do+  putStr (wish++"? ")+  hFlush stdout+  reply <- getLine+  ( if (null reply || reply=="y") then action+    else return x )++progressReport :: Bool -> Int -> Int -> IO ()+progressReport i n x | n >= x = do+  when i $ ( putStr (n' ++ replicate (length n') '\b') >>+             hFlush stdout )+  where+  n' = show n
+ examples/imperative/Behaviour.hs view
@@ -0,0 +1,23 @@+module Behaviour(Trace(..),(+++),approx) where++data Trace a+  = Step (Trace a)+  | a :> Trace a+  | End+  | Crash+  deriving (Eq, Show)++(+++) :: Trace a -> Trace a -> Trace a+Step s   +++ t = Step (s +++ t)+(x :> s) +++ t = x :> (s +++ t)+End      +++ t = t+Crash    +++ t = Crash++approx :: Eq a => Int -> Trace a -> Trace a -> Bool+approx 0 _        _        = True+approx n (a :> s) (b :> t) = a == b && approx (n-1) s t+approx n (Step s) (Step t) = approx (n-1) s t+approx n End    End        = True+approx n Crash  Crash      = True+approx n _        _        = False+
+ examples/imperative/Compiler.hs view
@@ -0,0 +1,59 @@+module Compiler(compile) where++import Machine+import Syntax+import StackMap+import Value++compile :: Command -> [Instruction]+compile c =+  replicate (depth sm) (Push Wrong) +++  compObey sm c +++  [Halt]+  where+  sm = stackMap c++compObey :: StackMap -> Command -> [Instruction]+compObey sm Skip = +  []+compObey sm (v := e) =+  compEval sm e +++  [Store (location sm v + 1)]+compObey sm (c1 :-> c2) =+  compObey sm c1 +++  compObey sm c2+compObey sm (If e c1 c2) =+  compEval sm e +++  [JumpUnless (length isc1 + 1)] +++  isc1 +++  [Jump (length isc2)] +++  isc2+  where+  isc1 = compObey sm c1+  isc2 = compObey sm c2+compObey sm (While e c) =+  ise +++  [JumpUnless (length isc + 1)] +++  isc +++  [Jump (negate (length isc + 1 + length ise + 1))]+  where+  ise = compEval sm e+  isc = compObey sm c+compObey sm (Print e) =+  compEval sm e +++  [Display]++compEval :: StackMap -> Expr -> [Instruction]+compEval sm (Val v) =+  [Push v]+compEval sm (Var v) =+  [Fetch (location sm v)]+compEval sm (Uno op1 e) =+  -- was op before arg eval  +  compEval sm e +++  [Instr1 op1]+compEval sm (Duo op2 e1 e2) =+  -- was op before arg evals  +  compEval sm        e1 +++  compEval (push sm) e2 +++  [Instr2 op2]
+ examples/imperative/Interpreter.hs view
@@ -0,0 +1,41 @@+module Interpreter(obey) where++import Syntax+import Behaviour+import Value++type Env = [(Name,Value)]++obey :: Command -> Trace Value+obey p = fst (run p [])++look :: Name -> Env -> Value+look x s = maybe Wrong id (lookup x s)++update :: Name -> Value -> Env -> Env+update x a s = (x,a) : filter (\(y,_) -> y/=x) s++run :: Command -> Env -> (Trace Value, Env)+run Skip        s = (End, s)+run (x := e)    s = (End, update x (eval e s) s)+run (p :-> q)   s = let (outp, sp) = run p s+                        (outq, sq) = run q sp+                    in (outp +++ outq, sq)+run (If e p q)  s = case eval e s of+                    -- was True -> q, False -> p+                    Log True  -> run p s+                    Log False -> run q s+                    _         -> (Crash, s)+run (While e p) s = case eval e s of+                    Log True  -> let (outp,sp) = run p s+                                     (outw,sw) = run (While e p) sp+                                 in (outp +++ Step outw, sw)+                    Log False -> (End, s)+                    _         -> (Crash, s)+run (Print e)   s = (eval e s :> End, s)++eval :: Expr -> Env -> Value+eval (Var x)      s = look x s+eval (Val v)      s = v+eval (Uno op a)   s = uno op (eval a s)+eval (Duo op a b) s = duo op (eval a s) (eval b s)
+ examples/imperative/Machine.hs view
@@ -0,0 +1,50 @@+module Machine(Instruction(..), exec) where++import Array+import Behaviour+import Value++data Instruction+  = Push Value+  | Pop+  | Fetch Int+  | Store Int+  | Instr1 Op1+  | Instr2 Op2+  | Display+  | Jump Int+  | JumpUnless Int+  | Halt+ deriving (Eq, Show)+ +exec :: [Instruction] -> Trace Value+exec instrs = run 1 []+  where+  size   = length instrs+  memory = array (1,size) ([1..] `zip` instrs)+  run pc stack =+    if pc < 1 || size < pc then Crash+    else+      case (memory ! pc, stack) of+      (Push x	    , stack)          -> run pc' (x : stack)+      (Pop	    , _ : stack)      -> run pc' stack+      (Fetch n      , stack)	 +        | length stack >  n           -> run pc' (stack !! n : stack)+      (Store n      , x : stack)+        | length stack >= n           -> run pc' (take (n-1) stack +++                                                  x : drop n stack)+      (Instr1 op1   , i : stack)      -> run pc' (uno op1 i : stack)+      (Instr2 op2   , i : j : stack)  -> run pc' (duo op2 j i : stack)+      (Display      , i : stack)      -> i :> run pc' stack+      (Jump n	    , stack)	      -> step n (run (pc' + n) stack)+      (JumpUnless n , Log b : stack)+        | b	                      -> run pc' stack+        | otherwise                   -> step n (run (pc' + n) stack)+      (Halt	    , stack)	      -> End+      _ 			      -> Crash+     where+      pc' = pc + 1++step :: Int -> Trace Value -> Trace Value    +step n t | n < 0     = Step t+         | otherwise = t
+ examples/imperative/Properties.hs view
@@ -0,0 +1,178 @@+import Behaviour+import Interpreter+import Compiler+import Machine+import Syntax+import Value++import Test.SmallCheck++------------- <series of expressions and commands> -------------++-- In the abstract syntax variables are just strings,+-- but we do not want to enumerate all lists of characters.+-- Just a couple of distinct names.++newtype VarName = VarName Name++instance Serial VarName where+  series = const [VarName [c] | c <- ['a'..'b']]++var :: VarName -> Expr+var (VarName v) = Var v++assign :: VarName -> Expr -> Command+assign (VarName v) e = (v := e)++-- Uses of depth 0 ensure that all occurrences of variables+-- or literals are treated as zero-depth atoms.+-- The rest is completely standard, but for the use of+-- 'var' for Var and 'assign' for Assign.++instance Serial Value where+  series = cons0 Wrong+        \/ cons1 Log . depth 0+        \/ cons1 Num . depth 0++instance Serial Op1 where+  series = const [Not, Minus]++instance Serial Op2 where+  series = const [And, Or, Eq, Less, LessEq,+                  Add, Sub, Mul, Div, Mod]++instance Serial Expr where+  series = cons1 var . depth 0+        \/ cons1 Val . depth 0+        \/ cons2 Uno+        \/ cons3 Duo++instance Serial Command where+  series = cons0 Skip+        \/ cons1 Print+        \/ cons2 assign+        \/ cons2 (:->)+        \/ cons3 If+        \/ cons2 While++----------------- <Closed Expressions> -------------------++-- If we want a series for a subset of the values in+-- a given type, one way to define it is via a newtype.+-- Here, expressions without variables.++newtype ClosedExpr = Closed Expr deriving Show++instance Serial ClosedExpr where+  series = cons1 val . depth 0+        \/ cons2 uno+        \/ cons3 duo+    where+    val v = Closed (Val v)+    uno op (Closed e) = Closed (Uno op e)+    duo op (Closed e1) (Closed e2) = Closed (Duo op e1 e2)++----------------- <Customised Programs> -----------------++-- The space of all commands grows very quickly with depth,+-- and many syntactically legal commands are bound to fail.+-- Here we define a restricted subset of commands in a+-- 'standard form':+-- -- Skip only occurs as an else-alternative+-- -- Print is only applied to simple variables+-- -- Only integer values are assigned to variables.+-- -- If and While conditions are compound comparisons.++newtype StdCommand = Std Command deriving Show++instance Serial StdCommand where+  series = cons1 print'+        \/ cons2 assign'+        \/ cons2 seq'+        \/ cons3 if'+        \/ cons2 while'+    where+    print'  (VarName v)                   = Std (Print (Var v))+    assign' (VarName v) (I e)             = Std (v := e)+    seq'    (Std c0) (Std c1)             = Std (c0 :-> c1)+    if'     (B e) (Std c0) (SkipOrStd c1) = Std (If e c0 c1)+    while'  (B e) (Std c)                 = Std (While e c)++newtype SkipOrStdCommand = SkipOrStd Command++instance Serial SkipOrStdCommand where+  series = cons0 skip+        \/ cons1 std . depth 0+    where+    skip        = SkipOrStd Skip+    std (Std c) = SkipOrStd c++newtype IExpr = I Expr++instance Serial IExpr where+  series = cons1 var' . depth 0+        \/ cons1 val' . depth 0+        \/ cons1 uno'+        \/ cons3 duo'+    where+    var' (VarName v)          = I (Var v)+    val' i                    = I (Val (Num i))+    uno' (I e)                = I (Uno Minus e)+    duo' (I2 d) (I e0) (I e1) = I (Duo d e0 e1)++newtype IOp2 = I2 Op2++instance Serial IOp2 where+  series = const [I2 op | op <- [Add, Sub, Mul, Div, Mod]]++newtype BExpr = B Expr++instance Serial BExpr where+  series = cons1 uno'+        \/ cons3 duo'+        \/ cons3 cmp'+    where+    uno' (B e)                = B (Uno Not e)+    duo' (B2 d) (B e0) (B e1) = B (Duo d e0 e1)+    cmp' (C2 c) (I e0) (I e1) = B (Duo c e0 e1)++newtype BOp2 = B2 Op2++instance Serial BOp2 where+  series = const [B2 op | op <- [And,Or]]++newtype COp2 = C2 Op2++instance Serial COp2 where+  series = const [C2 op | op <- [Eq,Less,LessEq]]++-------- <depth-bounded equivalence of program traces> --------++newtype Approx = Approx Int deriving Show++instance Serial Approx where+  series d = [Approx d]++(=~=) :: Eq a => Trace a -> Trace a -> Approx -> Bool+s =~= t = \(Approx d) -> approx d s t++----------------- <congruence properties> ------------------++prop_Congruence :: Command -> Property+prop_Congruence p =+  t1 /= Crash || t2 /= Crash ==>+    (t1 =~= t2)+  where+  t1 = obey p+  t2 = exec (compile p)++prop_StdCongruence :: StdCommand -> Property+prop_StdCongruence (Std p) =+  prop_Congruence p++main :: IO ()+main = do+  putStrLn "-- congruence for all programs:"+  smallCheck 2 prop_Congruence+  putStrLn "-- congruence for standard-form programs:"+  smallCheck 2 prop_StdCongruence
+ examples/imperative/README view
@@ -0,0 +1,10 @@+First see ../../README.++This directory gives the largest illustrative example.  We test for+congruence between an interpreter and compiler for a small imperative+language.  The example is adapted from an original using QuickCheck,+as described in the lecture notes for AFP'02 (LNCS 2638).  Compared+with the simpler example in ../logic, here specialised instances+are used to restrict the input space to programs in a standard form.+Run Properties.main and compare the rate of growth for the last two+properties tested.
+ examples/imperative/StackMap.hs view
@@ -0,0 +1,35 @@+module StackMap where++import Syntax+import List( union )++type StackMap = (Int,[Name])++stackMap :: Command -> StackMap+stackMap c = (0, comVars c)++push :: StackMap -> StackMap+push (n, vars) = (n+1, vars)++pop :: StackMap -> StackMap+pop (n, vars) = (n-1, vars)++location :: StackMap -> Name -> Int+location (n, vars) v = n + length (takeWhile (/=v) vars)++depth :: StackMap -> Int+depth (n, vars) = n + length vars++expVars :: Expr -> [Name]+expVars (Var v)     = [v]+expVars (Val _)     = []+expVars (Uno _ a)   = expVars a+expVars (Duo _ a b) = expVars a `union` expVars b++comVars :: Command -> [Name]+comVars Skip         = []+comVars (x := e)     = [x] `union` expVars e+comVars (c1 :-> c2)  = comVars c1 `union` comVars c2+comVars (If e c1 c2) = expVars e `union` comVars c1 `union` comVars c2+comVars (While e c)  = expVars e `union` comVars c+comVars (Print e)    = expVars e
+ examples/imperative/Syntax.hs view
@@ -0,0 +1,21 @@+module Syntax(Name, Expr(..), Command(..)) where++import Value++type Name = String++data Expr+  = Var Name+  | Val Value+  | Uno Op1 Expr+  | Duo Op2 Expr Expr+  deriving (Eq, Show)++data Command+  = Skip+  | Name := Expr+  | Command :-> Command+  | If Expr Command Command+  | While Expr Command+  | Print Expr+  deriving (Eq, Show)
+ examples/imperative/Value.hs view
@@ -0,0 +1,44 @@+module Value(Value(..), Op1(..), Op2(..), uno, duo) where++data Value+  = Num Int+  | Log Bool+  | Wrong+  deriving (Eq, Show)++data Op1+  = Not+  | Minus+  deriving (Eq, Show)++data Op2+  = And+  | Or+  | Mul+  | Add+  | Sub+  | Div+  | Mod+  | Less+  | LessEq +  | Eq+  deriving (Eq, Show)++uno :: Op1 -> Value -> Value+uno Not   (Log b) = Log (not b)+uno Minus (Num n) = Num (negate n)+uno _     _       = Wrong++duo :: Op2 -> Value -> Value -> Value+duo And     (Log a) (Log b)          = Log (a && b)+duo Or      (Log a) (Log b)          = Log (a || b)+duo Eq      (Log a) (Log b)          = Log (a == b)+duo Mul     (Num m) (Num n)          = Num (m * n)+duo Add     (Num m) (Num n)          = Num (m + n)+duo Sub     (Num m) (Num n)          = Num (m - n)+duo Div     (Num m) (Num n) | n /= 0 = Num (m `div` n)+duo Mod     (Num m) (Num n) | n /= 0 = Num (m `mod` n)+duo Less    (Num m) (Num n)          = Log (m < n)+duo LessEq  (Num m) (Num n)          = Log (m <= n)+duo Eq      (Num m) (Num n)          = Log (m == n)+duo _       _       _                = Wrong
+ examples/listy/ListProps.hs view
@@ -0,0 +1,92 @@+------------------------------------------------+-- Properties (some valid some invalid) of a few+-- standard list-processing functions.+-- A test module for SmallCheck.+-- Colin Runciman, August 2006.+-- Revised for 0.2, November 2006.+------------------------------------------------++module ListProps where++import Test.SmallCheck++-- properties about higher-order functions+-- plausible-looking but invalid laws about folds++prop_fold1 :: [Bool] -> Property+prop_fold1 xs =+  not (null xs) ==>+    \f -> foldl1 f xs == foldr1 f xs++prop_fold2 :: [Bool] -> [Bool] -> Property+prop_fold2 xs ys =+  not (null xs) && not (null ys) ==>+    \f -> foldr1 f xs `f` foldr1 f ys == foldr1 f (xs++ys)++-- properties using 'exists' with data and functional arguments++-- invalid because depth-bound for zs same as for xs ys+prop_union1 :: [Bool] -> [Bool] -> Property+prop_union1 xs ys =+  exists $ \zs ->+    \b -> (b `elem` zs) == (b `elem` xs || b `elem` ys)++-- valid variant: depth-bound doubled in existential+prop_union2 :: [Bool] -> [Bool] -> Property+prop_union2 xs ys =+  existsDeeperBy (*2) $ \zs ->+    \b -> (b `elem` zs) == (b `elem` xs || b `elem` ys)++-- do magical span arguments exist?+prop_span1 :: [Bool] -> [Bool] -> [Bool] -> Property+prop_span1 xs ys zs =+  xs++ys == zs ==> exists $ \t -> (xs,ys) == span t zs++-- deliberate mistake in final isPrefix equation+isPrefix :: Ord a => [a] -> [a] -> Bool+isPrefix [] ys = True+isPrefix (x:xs) [] = False+isPrefix (x:xs) (y:ys) = x==y || isPrefix xs ys++-- this completeness property still holds+isPrefixComplete :: String -> String -> Bool+isPrefixComplete xs ys =+  isPrefix xs (xs ++ ys)++-- but this existential soundness property fails+isPrefixSound :: String -> String -> Property+isPrefixSound xs ys = isPrefix xs ys ==>+  exists $ \xs' -> ys == (xs ++ xs')++main :: IO ()+main = do+  test1 "\\xs -> not (null xs) ==>\n\+        \  \\f -> foldl1 f xs == foldr1 f xs ?"+        prop_fold1+  test1 "\\xs ys -> not (null xs) && not (null ys) ==>\n \+        \  \\f -> foldr1 f xs `f` foldr1 f ys == foldr1 f (xs++ys) ?"+        prop_fold2+  test1 "\\xs ys -> exists $ \\zs ->\n\+        \  \\b -> (b `elem` zs) == (b `elem` xs || b `elem` ys) ?"+        prop_union1+  test1 "\\xs ys -> existsDeeperBy (*2) $ \\zs ->\n\+        \  \\b -> (b `elem` zs) == (b `elem` xs || b `elem` ys) ?"+        prop_union2+  test1 "\\xs ys zs -> xs++ys==zs ==>\n\+        \  exists $ \\t -> (xs,ys) == span t zs ?"+        prop_span1+  test1 "\\xs ys -> isPrefix xs (xs++ys) ?"+        isPrefixComplete+  test1 "\\xs ys zs -> isPrefix xs ys ==>\n\+        \  exists $ \\xs' -> ys == xs ++ xs' ?"+        isPrefixSound++test1 :: Testable a => String -> a -> IO ()+test1 s t = do+  rule+  putStrLn s+  rule+  smallCheck 4 t+  where+  rule = putStrLn "----------------------------------------------------"+
+ examples/listy/README view
@@ -0,0 +1,5 @@+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.
+ examples/logical/LogicProps.hs view
@@ -0,0 +1,128 @@+----------------------------------------------------+-- Propositional formulae, satisfiable, tautologous.+-- A test module for SmallCheck.+-- Colin Runciman, August 2006.+----------------------------------------------------++module PropLogic where++import Test.SmallCheck++import Data.List (nub)++data Prop = Var Name+          | Not Prop+          | And Prop Prop+          | Or  Prop Prop+          | Imp Prop Prop++instance Show Prop where+  show p = case p of+           Var n   -> show n+           Not q   -> "~"++show' q+           And q r -> show' q++"&"++show' r+           Or  q r -> show' q++"|"++show' r+           Imp q r -> show' q++"=>"++show' r+    where+    show' x = if priority p > priority x then "("++show x++")"+              else show x+    priority (Var _)   = 5+    priority (Not _)   = 4+    priority (And _ _) = 3+    priority (Or  _ _) = 2+    priority (Imp _ _) = 1++data Name = P | Q | R deriving (Eq,Show)++type Env = Name -> Bool++eval :: Prop -> Env -> Bool+eval (Var v)   env = env v+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++envsFor :: Prop -> [Env]+envsFor p = foldr bind [const False] (nub (varsOf p))+  where+  bind v es = concat [ [\x -> x==v || e x, e]+                     | e <- es ]++varsOf :: Prop -> [Name]+varsOf (Var v)   = [v]+varsOf (Not p)   = varsOf p+varsOf (And p q) = varsOf p ++ varsOf q+varsOf (Or  p q) = varsOf p ++ varsOf q+varsOf (Imp p q) = varsOf p ++ varsOf q++tautologous :: Prop -> Bool+tautologous p = all (eval p) (envsFor p)++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 Prop where+  series = cons1 Var+        \/ cons1 Not+        \/ cons2 And+        \/ cons2 Or+        \/ cons2 Imp++---------------------- <properties for testing> ---------------------++prop_taut1 :: Prop -> Property+prop_taut1 p =+  tautologous p ==> \e -> eval p e++prop_taut2 :: Prop -> Property+prop_taut2 p =+  not (tautologous p) ==> exists (\e -> not $ eval p e)++prop_sat1 :: Prop -> Env -> Property+prop_sat1 p e =+  eval p e ==> satisfiable p++prop_sat2 :: Prop -> Property+prop_sat2 p =+  satisfiable p ==> exists (\e -> eval p e)++prop_tautSat1 :: Prop -> Property+prop_tautSat1 p =+  not (tautologous p) ==> satisfiable (Not p)++prop_tautSat2 :: Prop -> Property+prop_tautSat2 p =+  not (satisfiable p) ==> tautologous (Not p)++main :: IO ()+main = do+  test1 "\\p -> tautologous p ==> \\e -> eval p e ?"+        prop_taut1+  test1 "\\p -> not (tautologous p) ==>\n\+        \  exists (\\e -> not $ eval p e) ?"+        prop_taut2+  test1 "\\p e -> eval p e ==> satisfiable p ?"+        prop_sat1+  test1 "\\p -> satisfiable p ==> exists (\\e -> eval p e) ?"+        prop_sat2+  test1 "\\p -> not (tautologous p) ==> satisfiable (Not p) ?"+        prop_tautSat1+  test1 "\\p -> not (satisfiable p) ==> tautologous (Not p) ?"+        prop_tautSat2++test1 :: Testable a => String -> a -> IO ()+test1 s t = do+  rule+  putStrLn s+  rule+  smallCheck 3 t+  where+  rule = putStrLn "----------------------------------------------------"+
+ examples/logical/README view
@@ -0,0 +1,7 @@+First see ../../README.++In this directory, LogicProps.hs illustrates the basic way to define+Serial instances of your own types, and hence Testable properties of+functions over them. Compile or interpret LogicProps.main (SmallCheck is+the only other module required) for a small selection of self-introducing+tests.
+ examples/numeric/NumProps.hs view
@@ -0,0 +1,61 @@+------------------------------------------+-- Illustrating numerics in SmallCheck 0.2+-- Colin Runciman, November 2006.+------------------------------------------++module NumProps where++import Test.SmallCheck++primes :: [Int]+primes = sieve [2..]+  where+  sieve (p:xs) =+    p : filter (noFactorIn primes) xs+  noFactorIn (p:ps) x =+    p*p > x || x `mod` p > 0 && noFactorIn ps x++-- using natural numbers++prop_primes1 :: Nat -> Property+prop_primes1 (N n) =+  n > 1 ==> forAll (`take` primes) $ \p ->+    p `mod` n > 0 || n == p++prop_primes2 :: Nat -> Property+prop_primes2 (N n) =+  n > 0 ==> exists $ \exponents ->+    n == product (zipWith power primes exponents)+  where+  power p (N e) = product (replicate e p)++-- using floating point numbers++prop_logExp :: Float -> Bool+prop_logExp x = exp (log x) == x++prop_recipRecip :: Float -> Bool+prop_recipRecip x = 1.0 / (1.0 / x) == x++main :: IO ()+main = do+  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\+        \  n == product (zipWith power primes exponents)"+        prop_primes2+  test1 "\\x -> exp (log x) == x"+        prop_logExp+  test1 "\\x -> 1.0 / (1.0 / x) == x"+        prop_recipRecip++test1 :: Testable a => String -> a -> IO ()+test1 s t = do+  rule+  putStrLn s+  rule+  smallCheck 8 t+  where+  rule = putStrLn "----------------------------------------------------"+
+ examples/numeric/README view
@@ -0,0 +1,9 @@+First see ../../README.++In this directory, NumProps.hs illustrates the use of test series+for natural numbers, either by explicit signatures including Nat (or+Natural) or by use of the N constructor.  It also illustrates use of+floating-point series. Compile or interpret NumProps (SmallCheck is+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.
+ examples/regular/README view
@@ -0,0 +1,8 @@+First see ../../README.++In this directory, Regular.hs illustrates a test involving IO -- writing+and reading expressions to/from a file.  The use of 'smart constructors'+in the series definition is necessary for the property to hold, but does+*not* reduce the number of tests -- rather, there are duplicated tests for+the same expressions generated in different ways. Compile or interpret+Regular.main for a self-introducing test.
+ examples/regular/Regular.hs view
@@ -0,0 +1,116 @@+module Regular where++import Data.Char (isAlpha)+import Data.List (intersperse)+import Control.Monad (liftM)+import Test.SmallCheck++-- A data type of regular expressions.++data RE = Emp+        | Lam+        | Sym Char+	| Alt [RE]+        | Cat [RE]+	| Rep RE+	deriving Eq++isEmp, isLam, isSym, isCat, isAlt, isRep :: RE -> Bool+isEmp Emp     = True+isEmp _       = False+isLam Lam     = True+isLam _       = False+isSym (Sym _) = True+isSym _       = False+isAlt (Alt _) = True+isAlt _       = False+isCat (Cat _) = True+isCat _       = False+isRep (Rep _) = True+isRep _       = False++-- Syms may be used to represent terminals or variables.+-- Using cat and alt instead of Cat and Alt ensures that:+-- (1) Cat and Alt arguments are multi-item lists;+-- (2) items in Cat arguments are not Cats;+-- (3) items in Alt arguments are not Alts.++cat :: [RE] -> RE+cat []  = Lam+cat [x] = x+cat xs  = Cat (concatMap catList xs)+  where+  catList (Cat ys) = ys+  catList z        = [z]++alt :: [RE] -> RE+alt []  = Emp+alt [x] = x+alt xs  = Alt (concatMap altList xs)+  where+  altList (Alt ys) = ys+  altList z        = [z]++instance Read RE where+  readsPrec _ s  = [rest s [[[]]]]++rest :: String -> [[[RE]]] -> (RE,String)+rest ""      (    a:as) = if null as then (a2re a,"")+                          else wrong+rest ('+':s) ((c:a):as) = if null c then wrong+			  else rest s (([]:c:a):as)+rest ('*':s) ((c:a):as) = case c of+                          []     -> wrong+                          (x:xs) -> rest s (((Rep x:xs):a):as)+rest ('0':s) ((c:a):as) = rest s (((Emp:c):a):as)+rest ('1':s) ((c:a):as) = rest s (((Lam:c):a):as)+rest ('(':s) as         = rest s ([[]]:as)+rest (')':s) (a:as)     = case as of+                          [] -> wrong+			  ((c:a'):as') -> rest s (((a2re a:c):a'):as')+rest (' ':s) as         = rest s as+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)++wrong = error "unreadable RE"++instance Show RE where+  show Emp      = "0"+  show Lam      = "1"+  show (Sym c)  = [c]+  show (Alt xs) = concat (intersperse "+" (map show xs))+  show (Cat xs) = concatMap (showBrackIf isAlt) xs+  show (Rep x)  = showBrackIf (\x -> isCat x || isAlt x) x ++ "*"++showBrackIf p x = ['(' | q] ++ show x ++ [')' | q] where q = p x++instance Serial RE where+  series = cons0 Emp+        \/ cons0 Lam+        \/ cons1 Sym . depth 0+        \/ cons1 alt+        \/ cons1 cat+        \/ cons1 Rep++prop_readShow :: RE -> IO Bool+prop_readShow re = do+  writeFile "tmp" (show re)+  re' <- liftM read (readFile "tmp")+  return (re'==re)++main = do+  rule+  putStrLn "Testing property involving IO.  Always returns True?"+  putStrLn "do\n\+           \  writeFile \"tmp\" (show re)\n\+           \  re' <- liftM read (readFile \"tmp\")\n\+           \  return (re'==re)"+  rule+  smallCheck 4 prop_readShow+  where+  rule = putStrLn+           "----------------------------------------------------"
+ smallcheck.cabal view
@@ -0,0 +1,48 @@+Name:          smallcheck+Version:       0.2.1+License:       BSD3+License-File:  LICENSE+Author:        Colin Runciman+Maintainer:    Colin Runciman <Colin.Runciman@cs.york.ac.uk>++Stability:     Beta+Category:      Testing+Synopsis:      Another lightweight testing library in Haskell.+Description:   SmallCheck is similar to QuickCheck (Claessen and Hughes 2000-) but+               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-Type:    Simple++Extra-source-files: examples/numeric/NumProps.hs, examples/logical/LogicProps.hs,+                    examples/imperative/Interpreter.hs, examples/imperative/Syntax.hs,+                    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++Data-files:         examples/numeric/README, examples/logical/README, examples/imperative/README,+                    examples/listy/README, examples/regular/README, README++Exposed-modules:    Test.SmallCheck