Abusing quickcheck to check existential properties
I recently used QuickCheck to check on some calculations for image compression. (I love exact rational arithmetic!) But I thought only to check for inverse properties, and I realized afterward I had failed to check for ranges. For example I should have checked that boundedB block = -1 <= b && b <= 1 where Cos a b c d = cos_of_block block which turns out to be correct. But actually my calculations were wrong, and the real bounds on b are not +/- 1 but rather +/- 0.5, so I might equally well have passed a more stringent test. It's quite embarrassing as I have only 5 bits of precision to represent b, and throwing away a bit on values that don't exist is not the best idea I have had recently. What I would really like to do is write some combinators for interval checking that say * It is a *universal* property that for *every* input, the output lies within the stated interval. * It is an *existential* property of *some* input that the output lies close to the ends of the stated interval. But how do I use QuickCheck to check an existential? I realize I could run boundsNotAchieved block = -0.9 <= b && b <= 0.9 where Cos a b c d = cos_of_block block and then if the test of boundsNotAcheived fails, my test passes (by exists x : P(x) iff not forall(x) : not P(x)). But if I set up a test suite in which some tests are supposed to fail and others are supposed to succeed, I will never keep track of which is which. I would like to build an existential test. Is it sufficient for me to write boundsAchieved block = expectFailure (-0.9 <= b && b <= 0.9) where Cos a b c d = cos_of_block block and then run 'quickCheck boundsAchieved'? In the long run I'd love something like fillsIntervalWithin :: (Num a, Ord a, Arbitrary a) => (a, a) -> a -> a -> Property with the idea that I want to test the partial application fillsIntervalWithin (lo, hi) epsilon and have the test succeed if every input x satisfies lo <= x <= hi and if some input x satisfies not (lo + epsilon <= x <= hi - epsilon). I'm betting someone on this list has already thought about similar problems and can advise me. (Because I have yet to write the specialized instance declaration for Arbitrary that guarantees the numerical invariants of the inputs, I have yet to test any of the examples in this email.) Norman
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
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))
Interesting. For A-E properties I can see where this approach would be helpful, especially if it's not too hard to think of a good skolem function. In my case x is empty and so I'm left with 'find a y such that P(y)' or a bit more exactly 'find an x in the four-dimensional unit cube such that 0.9 < f(x)' I've already written f and I'd really rather not write f-inverse; I want the computer to do some of the work for me. So perhaps SmallCheck would be a better way to go. It does seem a pity, as almost all the QuickCheck machinery would be useful in such a search. On the other hand there are similar scenarios on which I've already given up in despair, such as writing a generator for creating well-typed terms in a nontrivial language. Anyway, thanks for suggesting a skolem function---I'm sure I'll find use for one sooner or later. Norman
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). If you think about it from a plausible reasoning and constructive logic sense, QuickCheck should not be able to answer the question you desire. After all it runs a bounded number of tests, if it didn't find your case in that number of checks its not definitive. It may have been looking in the wrong spots at the wrong cases. A QuickCheck merely provides support for the plausibility of a universally quantified statement, much like how an experiment can't prove a model in physics, it can merely provide support for it. (see Polya's Mathematics and Plausible Reasoning). The scientific method can never prove anything. QuickCheck never gives you a false negative, but that one-sided error dooms your quest. You can assert that something doesn't exist with QuickCheck, but asserting that something always holds is the domain of mathematics, not experiment, unless you can exhaustively enumerate the universe of discourse, which is why SmallCheck _can_ handle existential claims. Now that said, if you can strengthen the existential to a probabalistic claim about the odds of a random sample satisfying a given property are greater than some fixed known positive real number, then you can abuse the known QuickCheck sample size to say something about the odds of your 'expectFailure' style trick failing to substantiate your claim, 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. -Ed On Tue, Oct 14, 2008 at 6:36 PM, Norman Ramsey <nr@cs.tufts.edu> wrote:
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))
Interesting. For A-E properties I can see where this approach would be helpful, especially if it's not too hard to think of a good skolem function. In my case x is empty and so I'm left with
'find a y such that P(y)'
or a bit more exactly
'find an x in the four-dimensional unit cube such that 0.9 < f(x)'
I've already written f and I'd really rather not write f-inverse; I want the computer to do some of the work for me. So perhaps SmallCheck would be a better way to go.
It does seem a pity, as almost all the QuickCheck machinery would be useful in such a search. On the other hand there are similar scenarios on which I've already given up in despair, such as writing a generator for creating well-typed terms in a nontrivial language.
Anyway, thanks for suggesting a skolem function---I'm sure I'll find use for one sooner or later.
Norman _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
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
On Sun, 19 Oct 2008 00:39:32 +0200, Norman Ramsey <nr@cs.tufts.edu> wrote:
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.
In ScalaCheck (QuickCheck for Scala, www.scalacheck.org) there is an "exists" combinator which naively tries to find a value satisfying the property. So you can do the following: val p = exists(arbitrary[Int])( n => (n > 0) ==> (n+n == n*n) ) scala> p.check + OK, proved property.
ARG_0: "2"
val q = exists(arbitrary[Int])( n => (n > 10) ==> (n+n == n*n) ) scala> q.check ! Gave up after only 0 passed tests. 500 tests were discarded. As you can see, there is a notion of proved properties in ScalaCheck, which was introduced to support the "exists" method. Of course, if the property is non-trivial ScalaCheck has a hard time finding a proof. Regards, Rickard Nilsson
Norman,
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. 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). Colin R
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
there are similar scenarios on which I've already given up in despair, such as writing a generator for creating well-typed terms in a nontrivial language.
This is something I've also struggled with. I'm coming to the conclusion that it'd really be useful for the "Gen" monad to be parameterizable with some user state, or maybe even be made into a transformer. The only alternative really seems to be passing around the extra information manually between generator-creation functions, and this quickly gets to be a pain. For me this is probably the most serious short-coming of QuickCheck. --Ben On 14 Oct 2008, at 23:36, Norman Ramsey wrote:
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))
Interesting. For A-E properties I can see where this approach would be helpful, especially if it's not too hard to think of a good skolem function. In my case x is empty and so I'm left with
'find a y such that P(y)'
or a bit more exactly
'find an x in the four-dimensional unit cube such that 0.9 < f(x)'
I've already written f and I'd really rather not write f-inverse; I want the computer to do some of the work for me. So perhaps SmallCheck would be a better way to go.
It does seem a pity, as almost all the QuickCheck machinery would be useful in such a search. On the other hand there are similar scenarios on which I've already given up in despair, such as writing a generator for creating well-typed terms in a nontrivial language.
Anyway, thanks for suggesting a skolem function---I'm sure I'll find use for one sooner or later.
Norman _______________________________________________ Haskell mailing list Haskell@haskell.org http://www.haskell.org/mailman/listinfo/haskell
participants (7)
-
Ben Moseley -
Colin Runciman -
Edward Kmett -
Koen Claessen -
Norman Ramsey -
nr＠cs.tufts.edu
-
Rickard Nilsson