[Haskell] Abusing quickcheck to check existential properties

Norman Ramsey nr at cs.tufts.edu
Sat Oct 18 18:39:32 EDT 2008


 > The answer is that QuickCheck can't correctly constructively verify an
 > existential condition without a constructive mechanism to generate the
 > existential (i.e. the Skolem function mentioned before).

I agree but don't think it's relevant.  QuickCheck can't verify a
universal either.

 > If [elided] you can abuse [QuickCheck] but unfortunately this costs
 > you the invariant that when quickcheck says something is wrong that
 > something really is wrong.
 > 
 > And to me at least the value of QuickCheck is that it never cries wolf.

It's a great point, and I agree completely.  

I guess what I would like is to reuse most of the mechanisms in
QuickCheck to have it say one of these two things:

  1. Found an satisfying instance after 73 tries: [gives instance]

  2. After 100 tries, could not find a satisfying instance.

Like failure, the first tells you something definite about your
program.  And like passing 100 tests, the second tells you nothing.


Norman


More information about the Haskell mailing list