[Haskell] Abusing quickcheck to check existential properties
colin at cs.york.ac.uk
Wed Oct 22 05:38:59 EDT 2008
> 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.
What you're asking for is similar to what SmallCheck could give you, but
in the context of exhaustive testing of small values not sample testing
of random values. However:
1. As most existentials are within the scope of a universal, there are
many instances tested, so when a witness is indeed found nothing is
2. A report is given only when no witness can be found within the
specified search depth -- or when more than one can be found in the case
of a unique existential.
Perhaps your final remark is tongue-in-cheek? I agree the question of
what "passed 100 tests" tells you is tricky; but it isn't "nothing".
Anyway, in SmallCheck knowing that any witness could only be beyond the
search depth does tell you something (eg. the expected witness might be
a position in a list where the search depth is the length of the list).
More information about the Haskell