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 reported.
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 subtly :-)
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).
Indeed so. 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! Norman