Permalink
Browse files

Updated README; other tweaks.

  • Loading branch information...
1 parent 66f87cd commit a5e19bf1e4cd8bb2b4485f1941d477faaec2be36 @leepike committed May 17, 2012
Showing with 160 additions and 61 deletions.
  1. +0 −30 LICENSE
  2. +145 −18 README.md
  3. +1 −0 TODO.md
  4. +12 −11 examples/Div0.hs
  5. +2 −2 src/Test/SmartCheck/Render.hs
View
30 LICENSE
@@ -1,30 +0,0 @@
-Copyright (c)2012, Lee Pike
-
-All rights reserved.
-
-Redistribution and use in source and binary forms, with or without
-modification, are permitted provided that the following conditions are met:
-
- * Redistributions of source code must retain the above copyright
- notice, this list of conditions and the following disclaimer.
-
- * 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.
-
- * Neither the name of Lee Pike nor the names of other
- contributors may be used to endorse or promote products derived
- from this software without specific prior written permission.
-
-THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
-"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 COPYRIGHT
-OWNER 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.
View
163 README.md
@@ -1,30 +1,157 @@
-SmartCheck takes the output of QuickCheck and does data-generic shrinking on it
-(you don't have to define shrink methods yourself). Once it's found the minimal
-value it can, it tries to generalize by replacing holes with arbitrary
-(well-typed) values. If for any replacement the test still fails, it
-conjectures that you plug anything into the holes.
+Synopsis
+--------------------------------
+
+SmartCheck is a smarter
+[QuickCheck](http://hackage.haskell.org/package/QuickCheck), a powerful testing
+library for Haskell. The purpose of SmartCheck is to help you more quickly get
+to the heart of a bug and to quickly all the ways that a property fails.
+
+SmartCheck is useful for debugging programs operating on algebraic datatypes.
+When a property is true, SmartCheck is just like QuickCheck (SmartCheck uses
+QuickCheck as a backend). When a fails, QuickCheck does two things. First, it
+attempts to find a minimal counterexample to the property is a robust,
+systematic way. (You do not need to define any custom shrink instances, like
+with QuickCheck.) Second, once a minimal counterexample is found, SmartCheck
+then attempts to generalize the failed value v by replacing the v's
+substructures with new values to make v', and QuickChecking each new v'. If for
+each new v' generated, the property also fails, we claim the property fails for
+any substructure replaced here (of course, this is true modulo the coverage of
+the tests).
+
+SmartCheck executes in a real-eval-print loop. In each iteration, all values
+that have the "same shape" as the generalized value is removed from possible
+created tests. The loop can be iterated until a fixed-point is reached, and
+SmartCheck is not able to create any new values that fail the property.
A typical example
--------------------------------
- > cd SmartCheck/src/
- > ghci -Wall ../examples/MutualRecData.hs
- *MutualRecData> main
+In the package there is an examples directory containing a number of examples.
+Let's look at the simplest,
+[Div0.hs](https://github.com/leepike/SmartCheck/blob/master/examples/Div0.hs).
+
+ > cd SmartCheck/examples
+ > ghci -Wall Div0.hs
+
+Div0 defines a toy language containing constants (C), addition (A), and division
+(D):
+
+ data M = C Int
+ | A M M
+ | D M M
+ deriving (Read, Show, Data, Typeable, Generic)
+
+Because SmartCheck performs data-generic operations using Data.Data and
+GHC.Generics we have to derive Data, Typeable, and Generic (we plan to eliminate
+dependence on Data.Data in the future). To use GHC.Generics, you also need the
+following pragmas:
+
+ {-# LANGUAGE DeriveDataTypeable #-}
+ {-# LANGUAGE DeriveGeneric #-}
+
+Let's say we have a little interpreter for the language that takes care not to
+divide by 0:
+
+ eval :: M -> Maybe Int
+ eval (C i) = Just i
+ eval (A a b) = do
+ i <- eval a
+ j <- eval b
+ return $ i + j
+ eval (D a b) =
+ if eval b == Just 0 then Nothing
+ else do i <- eval a
+ j <- eval b
+ return $ i `div` j
+
+Now suppose we define a set of values in M such that they won't result in
+division by 0. We might try the following:
+
+ divSubTerms :: M -> Bool
+ divSubTerms (C _) = True
+ divSubTerms (D _ (C 0)) = False
+ divSubTerms (A m0 m1) = divSubTerms m0 && divSubTerms m1
+ divSubTerms (D m0 m1) = divSubTerms m0 && divSubTerms m1
+
+(Can you spot the problem?)
+
+So our property states that so long as a value satisfies divSubTerms, then we
+won't have division by 0:
+
+div_prop :: M -> Property
+div_prop m = divSubTerms m ==> eval m /= Nothing
+
+Assuming we've defined an Arbitrary instance for M (just like in
+QuickCheck---however, we just have to implement the arbitrary method; the shrink
+method is superfluous), we are ready to run SmartCheck.
+
+divTest :: IO ()
+divTest = smartCheck args div_prop
+ where
+ args = scStdArgs { qcArgs = stdArgs
+ , treeShow = PrntString }
+
+In this example, we won't redefine any of QuickCheck's standard arguments, but
+it's certainly possible. the treeShow field tells SmartCheck whether you want
+generalized counterexamples shown in a tree format or printed as a long string
+(the default is the tree format).
+
+Ok, let's try it. First, SmartCheck just runs QuickCheck:
+
+ *Div0> divTest
+ *** Failed! Falsifiable (after 11 tests):
+ A (A (D (A (C (-3)) (C 40)) (C 11)) (D (C (-5)) (C (-42)))) (D (A (D (C (-9)) (C 29)) (C (-23))) (A (D (C (-6)) (D (C 23) (C (-20)))) (D (D (C (-13)) (C (-35))) (D (C 0) (C (-4))))))
- *** Failed! Falsifiable (after 15 tests):
- M (N (M (N (M (N P (-5) "\GS(") (N (M (N P 35 "$<\rk\183\no\NUL") (N (M (N P 31 "d: \228\244\135\251&") (N P 31 "") 52) 62 "\234\STX\246R\204.P\205") 28) 17 "") (-48)) 29 "7\157[\186X6\242\191*") (N (M (N P (-4) "2f\151\DLE!EG\162/\128") (N (M (N P 2 "n<a\USLRLXK") (N (M (N P 23 "\rK\140\STXQ\b\155( ") (N P 9 "}\247\DLE") 42) (-36) "\SO 1MJL\ETX") (-14)) (-47) "_^") 4) 69 "(\\i") (-48)) (-256) "\vp\179\177\163") (N (M (N P 31 "") (N (M (N (M (N (M (N P (-9) "W\ETXi\DC1\b\201") (N (M (N P (-16) "\150=q") (N (M (N P 5 "\RS") (N P (-10) "]") (-18)) 6 "i\ESC") (-6)) (-16) "\238k") (-55)) (-35) "\NUL\"") (N P 6 "xC2HFW") (-57)) (-21) "\\\187\130\153lI^\EM") (N (M (N (M (N P (-27) "}\DC2") (N (M (N P 26 "P\SYN\ACK\226W8-") (N (M (N (M (N (M (N P (-8) "\199\DLE\144\180") (N (M (N (M (N P 2 "") (N P 1 "c\t") (-3)) 3 "=`") (N (M (N (M (N P (-1) "B") (N (M (N (M (N P 1 "") (N P 0 "") 1) 0 "d") (N P 1 "w") 2) 2 "") 2) (-1) "D\v\163") (N (M (N P (-1) "") (N P 1 "\232M") 0) (-2) "") 0) (-3) "1r[") (-5)) 1 "\DC4\EM") (-4)) 0 "H3\RS\239") (N P 8 "\f\DC1y\151d") 15) 15 "") (N P (-2) "") 28) (-20) "\US\NAKZ\DLEVt") (-10)) (-5) "!M\ACKk\DC4\DC1uY?") (-27)) (-14) "YE+\163\rJVS_4") (N (M (N (M (N (M (N (M (N P (-2) "\237\&4@") (N P 6 "") 6) 2 "^\DLEM\189y") (N P (-16) "\222\247(\DLE") (-14)) (-6) "\DEL\DC1iM\vn\218") (N (M (N P 8 "?\249KH\t\153") (N P 9 "") 26) (-16) "") 30) 14 "\STXOLy[\EOT") (N (M (N P 13 "\249%") (N (M (N (M (N (M (N (M (N P (-1) "x") (N (M (N P (-1) "!b") (N P (-2) "\240") 3) 4 "") 1) 5 "\207") (N (M (N P 4 "") (N (M (N (M (N P (-2) "") (N P (-1) "e") 2) 0 "") (N (M (N (M (N (M (N P 1 "") (N P 1 "") (-1)) 1 "") (N P (-1) "") (-1)) 1 "") (N P (-1) "") (-1)) (-1) "") 4) 3 "\144\b\217\n") 3) 8 "") 1) (-3) "3}`") (N P 3 "6\149") (-11)) (-8) "") (N (M (N (M (N P (-5) "e\222J") (N P 5 "/+G") 6) 1 "\151\151\&9") (N P (-7) "") (-12)) 2 "!\237") 18) (-9) "|R+C\186}c") 6) 14 "a\208\ACK\ENQ\SI!") 55) 10 "\158") (-52)) 14 "") (-45)) 90 "lg") (-12)) 177 "\224I\246\189F%\SOH\DC4-") 187
+It then takes the output from QuickCheck and tries systematic shrinking:
*** Smart Shrinking ...
*** Smart-shrunk value:
- M (N P 0 "") (N P 1 "") 187
+ D (D (C (-13)) (C (-35))) (D (C 0) (C (-4)))
+
+Ok, that's some progress! Now SmartCheck attempt to generalize this minimal counterexample:
*** Extrapolating ...
*** Extrapolated value:
forall x0 x1:
- M
- |
- +- x1
- |
- +- x0
- |
- `- 187
+
+ D x1 (D (C 0) x0)
+
+Ahah! We see that for any possible subvalues x0 and x1, the above value fails.
+Our precondition divSubTerms did not account for the possibility of a
+non-terminal divisor evaluating to 0; we only pattern-matched on constants.
+
+SmartCheck asks us if we want to continue:
+
+ Attempt to find a new counterexample? ('Enter' to continue; any character
+ then 'Enter' to quit.)
+
+SmartCheck will omit any term that has the "same shape" as D x1 (D (C 0) x0) and
+try to find a new counterexample.
+
+ *** Failed! Falsifiable (after 13 tests):
+ D (A (C 23) (C (-52))) (A (D (D (C 52) (C 72)) (D (D (D (C 28) (C (-32))) (A (C 36) (C (-85)))) (C (-32)))) (A (A (A (C (-122)) (C (-76))) (C 52)) (D (D (D (C 91) (C 98)) (D (C 122) (C 64))) (C 5))))
+
+ *** Smart Shrinking ...
+ *** Smart-shrunk value:
+ D (D (C 52) (C 72)) (A (C (-1)) (C 1))
+
+ *** Extrapolating ...
+ *** Extrapolated value:
+ forall x0:
+
+ D x0 (A C (-1) (C 1))
+
+We find another counterexample; this time, the divisor is an addition term.
+
+We might ask SmartCheck to find another counterexample:
+
+ ...
+
+ *** Extrapolating ...
+ *** Could not extrapolate a new value; done.
+
+At this point, SmartCheck can't find a newly-shaped counterexample. (This
+doesn't mean there aren't more---you can try to increase the standard arguments
+to QuickCheck to allow more failed test before giving up (maxDiscard) or
+increasing the size of tests (maxSize). Or you could simply just keep running
+the real-eval-print loop.
View
@@ -26,6 +26,7 @@ TODO
* Make SubT from Forest into Tree(?) More natural and allows to index the head.
+* Fix parentheses bug for showing Strings.
Won't Do / Can't Do
-----------------------------------------------
View
@@ -15,7 +15,7 @@ import GHC.Generics
data M = C Int
| A M M
| D M M
- deriving (Read, Show, Data, Typeable, Eq, Generic)
+ deriving (Read, Show, Data, Typeable, Generic)
instance SubTypes M
@@ -45,24 +45,25 @@ instance Arbitrary M where
-- property: so long as 0 isn't in the divisor, we won't try to divide by 0.
-- It's false: something might evaluate to 0 still.
-div1 :: M -> Property
-div1 m = divSubTerms m ==> eval m /= Nothing
- where
+div_prop :: M -> Property
+div_prop m = divSubTerms m ==> eval m /= Nothing
+
-- precondition: no dividand in a subterm can be 0.
- divSubTerms (C _) = True
- divSubTerms (D _ (C 0)) = False
- divSubTerms (A m0 m1) = divSubTerms m0 && divSubTerms m1
- divSubTerms (D m0 m1) = divSubTerms m0 && divSubTerms m1
+divSubTerms :: M -> Bool
+divSubTerms (C _) = True
+divSubTerms (D _ (C 0)) = False
+divSubTerms (A m0 m1) = divSubTerms m0 && divSubTerms m1
+divSubTerms (D m0 m1) = divSubTerms m0 && divSubTerms m1
-- div0 (A _ _) = property False
-- div0 _ = property True
divTest :: IO ()
-divTest = smartCheck args div1
+divTest = smartCheck args div_prop
where
args = scStdArgs { qcArgs = stdArgs
- { maxSuccess = 1000
- , maxSize = 20 }
+ -- { maxSuccess = 1000
+ -- , maxSize = 20 }
, treeShow = PrntString
}
@@ -60,11 +60,11 @@ replaceWithVars format d idxs vars =
stitchTree :: Tree String -> String
stitchTree = stitch
where
+ stitch (Node str forest) = str ++ " " ++ (unwords $ map stitchTree' forest)
+
stitchTree' (Node str []) = str
stitchTree' node = '(' : stitch node ++ ")"
- stitch (Node str forest) = str ++ " " ++ (unwords $ map stitchTree' forest)
-
---------------------------------------------------------------------------------
-- Make a Tree out of a Data value. On each level, we just use the user-defined

0 comments on commit a5e19bf

Please sign in to comment.