Permalink
Browse files

Updated README, TODOs, and References.

  • Loading branch information...
1 parent 254fca2 commit f699ed11ad4f296e44f0ec764bbd3de50ef963d0 @leepike committed Jul 27, 2012
Showing with 26 additions and 92 deletions.
  1. +19 −70 README.md
  2. +5 −22 TODO.md
  3. +2 −0 refs/README.txt
View
@@ -6,59 +6,35 @@
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 discover _each_ possible way that a
-property may fail.
-
-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 property fails, SmartCheck kicks into gear.
-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, but if you do, those are used. SmartCheck usually can do
-much better than even custom shrink instances.) Second, once a minimal
-counterexample is found, SmartCheck then attempts to generalize the failed value
-d by replacing `d`'s substructures with new values to make `d'`, and QuickChecking
-each new `d'`. If for each new `d'` 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.
+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 discover _each_ possible way that a property may fail.
+
+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 property fails, SmartCheck kicks into gear. 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, but if you do, those are used. SmartCheck usually can do much better than even custom shrink instances.) Second, once a minimal counterexample is found, SmartCheck then attempts to generalize the failed value d by replacing `d`'s substructures with new values to make `d'`, and QuickChecking each new `d'`. If for each new `d'` 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
--------------------------------
-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).
+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):
+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, Typeable, Generic)
-Because SmartCheck performs data-generic operations using GHC.Generics we have
-to derive Typeable and Generic. To use GHC.Generics, you
-also need the following pragmas: and the single automatically-derived instance:
+Because SmartCheck performs data-generic operations using GHC.Generics we have to derive Typeable and Generic. To use GHC.Generics, you also need the following pragmas: and the single automatically-derived instance:
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
instance SubTypes M
-Let's say we have a little interpreter for the language that takes care to
-return `Nothing` if there is a division by 0:
+Let's say we have a little interpreter for the language that takes care to return `Nothing` if there is a division by 0:
eval :: M -> Maybe Int
eval (C i) = Just i
@@ -72,73 +48,52 @@ return `Nothing` if there is a division by 0:
j <- eval b
return $ i `div` j
-Now suppose we define a set of values of M such that they won't result in
-division by 0. We might try the following:
+Now suppose we define a set of values of 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
-So our property (tries) to state that so long as a value satisfies divSubTerms,
-then we won't have division by 0 (can you spot the problem in `divSubTerms`?):
+So our property (tries) to state that so long as a value satisfies divSubTerms, then we won't have division by 0 (can you spot the problem in `divSubTerms`?):
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.
+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 = PrintString }
-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).
+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 7 tests):
D (D (D (A (C (-20)) (D (D (C 2) (C (-19))) (C (-8)))) (D (D (C (-23)) (C 32)) (C (-7)))) (A (A (C 2) (C 10)) (A (C (-2)) (C 13)))) (D (A (C 12) (C (-7))) (D (A (C (-29)) (C 19)) (C 30)))
-Oh, that's confusing, and for such a simple property and small datatype!
-SmartCheck takes the output from QuickCheck and tries systematic shrinking for
-the one failed test-case, kind of like [SmallCheck](http://www.cs.york.ac.uk/fp/smallcheck/) might. We get the following
-reduced counterexample:
+Oh, that's confusing, and for such a simple property and small datatype! SmartCheck takes the output from QuickCheck and tries systematic shrinking for the one failed test-case, kind of like [SmallCheck](http://www.cs.york.ac.uk/fp/smallcheck/) might. We get the following reduced counterexample:
*** Smart Shrinking ...
*** Smart-shrunk value:
D (C 0) (D (C 0) (C (-1)))
-Ok, that's some progress! Now SmartCheck attempt to generalize this (local) minimal
-counterexample. SmartCheck has two generalization steps that we'll explain
-separately although SmartCheck combines their results in practice (you can turn
-off each kind of generalization in the flags). First,
-SmartCheck tries to generalize *values* in the shrunk counterexample. SmartCheck
-returns
+Ok, that's some progress! Now SmartCheck attempt to generalize this (local) minimal counterexample. SmartCheck has two generalization steps that we'll explain separately although SmartCheck combines their results in practice (you can turn off each kind of generalization in the flags). First, SmartCheck tries to generalize *values* in the shrunk counterexample. SmartCheck returns
*** Extrapolating values ...
*** Extrapolated value:
forall x0:
D x0 (D (C 0) (C (-1)))
-Ahah! We see that for any possible subvalues x0, 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.
+Ahah! We see that for any possible subvalues x0, 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.
-In addition, SmartCheck tries to do something I call *constructor generalization*.
-For a datatype with a finite number of constructors, the idea is to see if for
-each subvalue in the counterexample, there is are subvalues that also fail the
-property, using every possible constructor in the datatype. So for example, for
-our counterexample above
+In addition, SmartCheck tries to do something I call *constructor generalization*. For a datatype with a finite number of constructors, the idea is to see if for each subvalue in the counterexample, there is are subvalues that also fail the property, using every possible constructor in the datatype. So for example, for our counterexample above
*** Extrapolating constructors ...
*** Extrapolated value:
@@ -147,9 +102,7 @@ our counterexample above
D (C 0) (D C0 (C (-1)))
-So in the hole `C0`, SmartCheck was able to build a value using each of the
-constructors `C`, `A`, and `D` (well, it already knew there was a value using
-`C`---`C 0`.
+So in the hole `C0`, SmartCheck was able to build a value using each of the constructors `C`, `A`, and `D` (well, it already knew there was a value using `C`---`C 0`.
SmartCheck asks us if we want to continue:
@@ -183,8 +136,4 @@ 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.)
+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
27 TODO.md
@@ -1,12 +1,6 @@
TODO
-----------------------------------------------
-* Use [GHC generics](http://www.haskell.org/ghc/docs/latest/html/users_guide/generic-programming.html)
- instead of SubTypes class.
-
-* Use instances so I can pass anything that can be turned into a property to
- reduce, like in QuickCheck.
-
* Make sure I can use extrapolation on its own, without reduce.
* Testing with arguments to value constructors omitted in the SubTypes
@@ -16,10 +10,7 @@ TODO
you give them an index that is out of bounds. Perhaps I should return a
Maybe?
-* Check that the SubTypes class works with tuples, lists.
-
* Options:
- * Chatty option for reducing/extrapolating.
* Option for controlling depth into structure we recurse.
* Performance analysis of extrapolation.
@@ -31,25 +22,12 @@ TODO
* Document SubTypes class methods!
-* In PrintTree, pull baseTypes up? not sure...
-
-* Am I passing args to iterateArb correctly? Document the use of size and tries
- better.
-
- * maxSize parameter in interateArb really depends on using a sized parameter in
- arbitrary instances. Anyway to ensure/control this?
-
* We extrapolate if there exists at least one test that satisfies the
precondition, and for all tests that asatisfy the precondition, they fail. Is
this the right thing to do? (I think it is.)
* Args to optionally extrapolate and contructor extrapolate.
-* Generalize extrapolate/Replace --- same iter function used in both.
-
-* I don't think I need ReplaceSubs --- Chop will work. I just want to prevent
- recurring in a substs tree.
-
* Make sure that foldM (extractResult prop) FailedPreCond res in SmartGen fails
eagerly.
@@ -80,6 +58,11 @@ Won't Do / Can't Do
* I think I need something like this.
+* I don't think I can make a generic instance for the arbitrary method. This is
+ because I don't take a value and apply a function to it. Rather, I want to
+ generate a new value. But Generics expects to have some sort of
+ representation of the data you're manipulating.
+
Done
-----------------------------------------------
* ~~Rename examples/Test to examples/MutRecData~~
View
@@ -1,5 +1,7 @@
-- Refs ------------------------------------------------------------------------
+* Feat in Haskell '12: http://wiki.portal.chalmers.se/cse/pmwiki.php/FP/Testing-Feat
+
* The SYB paper:
http://research.microsoft.com/en-us/um/people/simonpj/Papers/hmap/index.htm
Has shrink example

0 comments on commit f699ed1

Please sign in to comment.