SmartCheck icon indicating copy to clipboard operation
SmartCheck copied to clipboard

Only activate existential sub-value generalization when there is more than one constructor

Open rudymatela opened this issue 8 years ago • 0 comments

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.)

Notes

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.

rudymatela avatar Aug 04 '17 14:08 rudymatela