--------------------------------------------------------------- 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 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 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 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 (or just ) 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