[Haskell] Abusing quickcheck to check existential properties
Koen Claessen
koen at chalmers.se
Mon Oct 13 05:57:17 EDT 2008
Hi Norman,
> But how do I use QuickCheck to check an existential?
The "standard" method in QuickCheck is to be constructive, and
actually implement the function that constructs for the value. So,
instead of
forAll x . exists y . P(x,y)
you write
forAll x . P(x, find_y(x))
for a suitably implemented function find_y. (This function is called a
skolem function by logicians).
It often depends on the problem domain how easy/hard it is to write
such a function. For example, you may be actually able to just
calculate y in find_y. Example:
prop_Leq x (y :: Integer) =
x <= y ==>
exists d . d >= 0 s.t. x+d == y
becomes
prop_Leq x (y :: Integer) =
x <= y ==>
let d = y-x in
d >= 0 &&
x+d == y
In some cases though, some kind of search might be needed. The library
SmallCheck provides default such search functions for Haskell types
(if your search can be limited by a concept of depth).
One thing that writing a skolem search function forces you to do is to
decide when the existential can *not* be found (after all, we are
interested in finding bugs). So, this forces you to think about what
bounds you have on the search domain, which can be hard.
/Koen
More information about the Haskell
mailing list