leepike / smartcheck Goto Github PK
View Code? Open in Web Editor NEWA Smarter QuickCheck
License: BSD 3-Clause "New" or "Revised" License
A Smarter QuickCheck
License: BSD 3-Clause "New" or "Revised" License
This is perhaps related to issue #12.
For the motivating example of the SmartCheck paper, SmartCheck reports a correct counter-example,
but an incorrect generalization:
forall values x0 x1 x2 x3:
T x3 (: -21874 x0) x2 (: -12585 []) x1
It is too general and includes values that are not counter-examples:
> let x0 = [21874]; x1 = []; x2 = []; x3 = []
> prop (T x3 (-21874:x0) x2 (-12585:[]) x1)
True
I have run the example with the default parameters, maybe tuning it to test more could fix this.
When can we expect to see smartcheck
on Hackage? If you don't think it's ready, where does it need work and how can the rest of us help?
I've played with it a bit via cabal-dev, and it seems pretty great!
Hello,
I think SmartCheck-0.2.2 does not compile under GHC 8.0.2 or with QuickCheck 2.10.*. Though this may be just my system misbehaving. I have tried the following.
Starting from a fresh home directory, I did:
$ cabal update
Downloading the latest package list from hackage.haskell.org
$ cabal install smartcheck
Resolving dependencies...
Downloading smartcheck-0.2.2...
Configuring smartcheck-0.2.2...
Building smartcheck-0.2.2...
Failed to install smartcheck-0.2.2
Build log ( /home/testuser/.cabal/logs/smartcheck-0.2.2.log ):
cabal: Entering directory '/tmp/cabal-tmp-30973/smartcheck-0.2.2'
Configuring smartcheck-0.2.2...
Building smartcheck-0.2.2...
Preprocessing library smartcheck-0.2.2...
<command line>: cannot satisfy -package-id QuickCheck-2.10.0.1-ALuGysu7txTB2VnkPyDuTq
(use -v for more information)
cabal: Leaving directory '/tmp/cabal-tmp-30973/smartcheck-0.2.2'
cabal: Error: some packages failed to install:
smartcheck-0.2.2 failed during the building phase. The exception was:
ExitFailure 1
After some fiddling around, I installed the immediately previous version
of QuickCheck (2.9.2):
$ cabal install tf-random primitive random generic-deriving mtl --reinstall --force-reinstalls
...
$ cabal install QuickCheck-2.9.2
...
Installed QuickCheck-2.9.2
When I try to install install SmartCheck bound with QuickCheck-2.9.2, I get a compilation error message:
$ cabal install smartcheck --constraint 'QuickCheck <= 2.9.2'
Resolving dependencies...
Configuring smartcheck-0.2.2...
Building smartcheck-0.2.2...
Failed to install smartcheck-0.2.2
Build log ( /home/testuser/.cabal/logs/smartcheck-0.2.2.log ):
cabal: Entering directory '/tmp/cabal-tmp-1490/smartcheck-0.2.2'
Configuring smartcheck-0.2.2...
Building smartcheck-0.2.2...
Preprocessing library smartcheck-0.2.2...
src/Test/SmartCheck/Types.hs:6:14: warning:
-XOverlappingInstances is deprecated: instead use per-instance pragmas OVERLAPPING/OVERLAPPABLE/OVERLAPS
[ 1 of 11] Compiling Test.SmartCheck.Types ( src/Test/SmartCheck/Types.hs, dist/build/Test/SmartCheck/Types.o )
src/Test/SmartCheck/Types.hs:256:10: error:
• No instance for (Generic Char)
arising from a use of ‘Test.SmartCheck.Types.$dmsubTypes’
• In the expression: Test.SmartCheck.Types.$dmsubTypes @Char
In an equation for ‘subTypes’:
subTypes = Test.SmartCheck.Types.$dmsubTypes @Char
In the instance declaration for ‘SubTypes Char’
...
src/Test/SmartCheck/Types.hs:259:10: error:
• No instance for (Generic Int)
arising from a use of ‘Test.SmartCheck.Types.$dmshowForest’
• In the expression: Test.SmartCheck.Types.$dmshowForest @Int
In an equation for ‘showForest’:
showForest = Test.SmartCheck.Types.$dmshowForest @Int
In the instance declaration for ‘SubTypes Int’
cabal: Leaving directory '/tmp/cabal-tmp-1490/smartcheck-0.2.2'
cabal: Error: some packages failed to install:
smartcheck-0.2.2 failed during the building phase. The exception was:
ExitFailure 1
This may be my system, but it seems this issue is related to the fact that
Generic instances have been removed from base types starting with GHC 8.0. See
comment number 7 from GHC ticket 10532. See also this issue from lens and
this issue from optparse.
I am using GHC 8.0.2, cabal-install 1.24.0.2 and Cabal 1.24.2.0.
I tried installing under GHC 7.10 and it worked fine.
While trying to run SmartCheck, I've bumped into some problems. I've tried
both vanilla scStdArgs (check prop = smartCheck scStdArgs
) and this version here:
check prop = smartCheck scArgs prop
where scArgs = scStdArgs { format = PrintString
, scMaxForall = 100 -- 20
, scMinForall = 50 -- 10
, scMaxExists = 50 -- 20
, scMaxDepth = Just 5 -- Nothing
, scMaxSize = 20 -- 10
}
The property described here are very simple but artificial, just to show, in the simplest form possible, issues I've seen.
This property should fail for False *
:
prop_booleans :: Bool -> Bool -> Bool
prop_booleans p q = p
But actually, SmartCheck reports failing for only False
(it should be False False
or False True
). And it is not able to extrapolate:
> check prop_booleans
Failed! Falsifiable (after 1 test):
False
*** (If any stage takes too long, try modifying SmartCheck's standard arguments (see Args.hs).)
*** Smart Shrinking ...
*** Smart-shrunk value:
False
*** Extrapolating values ...
*** Extrapolating Constructors ...
*** Could not extrapolate a new value.
Attempt to find a new counterexample?
('Enter' to continue; any character then 'Enter' to quit.)
+++ OK, passed 100 tests.
*** No value to smart-shrink; done.
Of the counterexamples reported in other properties, I've noticed that the
first parameter is usually missing.
QuickCheck correctly reports the output:
> quickCheck prop_booleans
*** Failed! Falsifiable (after 5 tests and 1 shrink):
False
False
Lazy SmallCheck is able to report the partial counterexample:
> depthCheck 3 prop_booleans
LSC: Counterexample found after 3 tests.
Var 0: False
Var 1: _
Another issue happens for a slightly different statement of the property above:
-- This should fail for "(False,*)"
prop_booleans2 :: (Bool,Bool) -> Bool
prop_booleans2 (p,q) = p
After running SmartCheck, it is able to correctly report a counterexample
(False,True)
, but it is not able to extrapolate that to (False,*)
.
SmartCheck is supposed to work that way in this case?
> check prop_booleans2
*** Failed! Falsifiable (after 1 test):
*** (If any stage takes too long, try modifying SmartCheck's standard arguments (see Args.hs).)
*** Smart Shrinking ...
*** Smart-shrunk value:
(False,True)
*** Extrapolating values ...
*** Extrapolating Constructors ...
*** Could not extrapolate a new value.
Attempt to find a new counterexample?
('Enter' to continue; any character then 'Enter' to quit.)
*** Gave up! Passed only 0 tests.
*** No value to smart-shrink; done.
Lazy SmallCheck is also able to report the partial counterexample:
> depthCheck 3 prop_booleans2
LSC: Counterexample found after 4 tests.
Var 0: (False,_)
*** Exception: ExitFailure 1
This property should fail for any list containing a repeated element:
prop_nub :: [Int] -> Bool
prop_nub xs = xs == nub xs
When running SmartCheck, it displays a (correct) counterexample, but extrapolates that to something invalid:
*** Failed! Falsifiable (after 7 tests):
*** (If any stage takes too long, try modifying SmartCheck's standard arguments (see Args.hs).)
*** Smart Shrinking ...
*** Smart-shrunk value:
[4,4]
*** Extrapolating values ...
*** Extrapolating Constructors ...
*** Extrapolated value:
forall values x0:
: 4 (: x0 [])
[4,*]
is clearly not a correct extrapolation. A correct one would be
[4,4,*]
or 4:4:*
. Or am I misinterpreting the output?
I'm using HEAD SmartCheck (7c35ea3). My GHC is 7.8.2.
It would be nice if SmartCheck supported custom generators, like QuickCheck does with forAll
. For example, I want to use SmartCheck to test an interpreter I'm working on, but I need to be able generate expressions of a given type. I can probably work around it with the standard newtype trick though, for now.
Hi,
I think I found a regression on SmartCheck-0.2.2 in relation to SmartCheck-0.2.1.
Consider the following minimal SmartChecking program:
import Test.SmartCheck
import Data.List (nub)
main :: IO ()
main = smartCheck scStdArgs{format = PrintString}
$ \xs -> nub xs == (xs :: [Int])
When compiled and run against smartcheck-0.2.1, it produces:
$ ghc-7.10 -dynamic list.hs
$ yes | ./list
*** Finding a counterexample with QuickCheck...
*** Failed! Falsifiable (after 6 tests):
*** Smart Shrinking ...
*** Smart-shrunk value:
[-2,-2]
*** Extrapolating values ...
*** Extrapolating Constructors ...
*** Extrapolated value:
forall values x0:
: -2 (: -2 x0)
*** Done.
So far so good. This is what I would expect. The tail of the list is generalized. The property fails regardless of the tail.
(Above, I have trimmed/summarized the output a bit.)
When compiled and run against smartcheck-0.2.2, it produces:
$ ghc-7.10 -dynamic list.hs
$ yes | list
*** Finding a counterexample with QuickCheck...
+++ OK, passed 1 tests.
*** Analyzing the first argument of the property with SmartCheck...
*** (If any stage takes too long, modify SmartCheck's arguments.)
*** No value to smart-shrink; done.
SmartCheck fails to report a counter-example and says it passes the property for just 1 test.
(Above, output is in full.)
The root of the problem seems to be that QuickCheck restructured its internal State type a bit.
Add a way to optionally shrink base types.
One way to do this would be to define a "shrink-like" class, and the user can define instances for types they want to shrink. Then during the reduction phase, it will additionally shrink according to the definition. I can't use QC's shrink directly, since shrink is defined by default for base types.
Note that simply using a newtype won't help, since base types inside of a new or data type isn't touched.
This is more of a feature request than a bug itself.
When there is only one possible constructor, existential sub-value generalization does not produce a
very useful result.
Consider the following faulty sort
implementation along with a property:
sort :: Ord a => [a] -> [a]
sort [] = []
sort (x:xs) = sort (filter (< x) xs)
++ [x]
++ sort (filter (> x) xs)
prop_sortCount :: Int -> [Int] -> Bool
prop_sortCount x xs = count x (sort xs) == count x xs
where
count x = length . filter (== x)
The property fails, as shown by QuickCheck:
> quickCheck prop_sortCount
*** Failed! Falsifiable (after 51 tests and 9 shrinks):
21
[21,21]
The generalization produced by SmartCheck is not very useful, see:
> smartCheck scStdArgs{format = PrintString} (prop_sortCount :: Int -> [Int] -> Bool)
*** Failed! Falsifiable (after 57 tests and 10 shrinks):
*** Non SmartChecked arguments:
[-10,-10]
*** Analyzing the first argument of the property with SmartCheck...
*** Smart-shrunk value:
-10
*** Extrapolated value:
forall constructors C0:
there exist arguments x̅ s.t.
C0
The existential sub-value generalization is correct: for all possible constructors (GHC.Int
) there exists a value (-10
) that falsifies the property. But that is obvious from the reported counter-example itself.
Perhaps existential sub-value generalization should only activate when there is more than one constructor that can be placed? (In which case it is really useful -- cf. divSubTerms
example from SmartCheck's paper.)
If we set runExists = False
, SmartCheck reports that it cannot extrapolate a
new value -- this is what I would intuitively expect in this case.
SmartCheck does work flawlessly if we uncurry the property (so it can
generalize the second argument as well):
> smartCheck scStdArgs{format = PrintString} $ uncurry prop_sortCount
*** Finding a counterexample with QuickCheck...
*** Failed! Falsifiable (after 8 tests):
*** Smart-shrunk value:
(5,[5,5])
*** Extrapolated value:
forall values x0: (,) 5 (: 5 (: 5 x0))
The sort
example is also used in issue #12.
Consider the following faulty sort
implementation along with a property:
sort :: Ord a => [a] -> [a]
sort [] = []
sort (x:xs) = sort (filter (< x) xs)
++ [x]
++ sort (filter (> x) xs)
prop_sortCount :: Int -> [Int] -> Bool
prop_sortCount x xs = count x (sort xs) == count x xs
where
count x = length . filter (== x)
SmartCheck does work flawlessly if we uncurry the property so it can generalize the second argument as well:
> smartCheck scStdArgs{format = PrintString} $ uncurry prop_sortCount
*** Finding a counterexample with QuickCheck...
*** Failed! Falsifiable (after 8 tests):
*** Smart-shrunk value:
(5,[5,5])
*** Extrapolated value:
forall values x0: (,) 5 (: 5 (: 5 x0))
However, if we flip the property so that SmartCheck can generalize only the second argument, the reported generalization is incorrect:
*Main Test.QuickCheck> smartCheck scStdArgs{format = PrintString} $ flip prop_sortCount
*** Finding a counterexample with QuickCheck...
*** Failed! Falsifiable (after 11 tests):
*** Non SmartChecked arguments:
0
*** Analyzing the first argument of the property with SmartCheck...
*** Smart-shrunk value:
[8,-10,9,0,0,-9,-3,4,-4]
*** Extrapolated value:
forall values x0:
: 8 x0
By incorrect, I mean it includes values that are not counter-examples, like 8:[]
or 8:7:6:[]
. Of course, it also includes correct counter-examples, like: 8:8:[]
.
I would expect it to report something like:
*** Extrapolated value:
forall values x0:
: 8 (: 9 (: 0 (: 0 x0)))
I understand this may be hard to fix because of the nature of the generalization algorithm that is being used. The algorithm is unsound in the general case anyway.
I have run this with default values. Maybe just changing the parameters may get rid of the incorrect generalization.
The sort
example is also used in issue #11.
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.