[Haskell] Abusing quickcheck to check existential properties
nr at cs.tufts.edu
Wed Oct 22 23:02:45 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.
Exactly what I'm looking for.
> Perhaps your final remark is tongue-in-cheek?
Perhaps it's taken out of context :-)
It was in a reply to Edward Kmett and was a copy of something Edward
had said, with existentials exchanged for universals. I was aiming to
make the point that if the inability to find a witness is not
interesting, then the inability to find a counterexample is also not
interesting. Since many of us may think we have learned something
useful about a program when QuickCheck or SmallCheck fails to find a
counterexample of a universal claim, perhaps we should reason
contrapositively and agree that we have also learned something useful
if QuickCheck or SmallCheck fails to find a witness of an existential
claim. In other words, I was disagreeing with Edward. Way too
> I agree the question of what "passed 100 tests" tells you is
> tricky; but it isn't "nothing".
I agree violently on both points :-)
> 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).
Now if only I could find time to adapt QuickCheck and/or SmallCheck to
generate unit tests for C code (I'm currently teaching C and assembly
language) I would be one happy camper!
More information about the Haskell