Abusing quickcheck to check existential properties

9 messages
Open this post in threaded view
|
Report Content as Inappropriate

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 _______________________________________________ Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell
Open this post in threaded view
|
Report Content as Inappropriate

Re: Abusing quickcheck to check existential properties

 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 _______________________________________________ Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell
Open this post in threaded view
|
Report Content as Inappropriate

Re: Abusing quickcheck to check existential properties

 > > 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 [hidden email] http://www.haskell.org/mailman/listinfo/haskell
Open this post in threaded view
|
Report Content as Inappropriate

Re: Abusing quickcheck to check existential properties

Open this post in threaded view
|
Report Content as Inappropriate

Re: Abusing quickcheck to check existential properties

Open this post in threaded view
|
Report Content as Inappropriate

Re: Abusing quickcheck to check existential properties

 In reply to this post by Edward Kmett  > 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 _______________________________________________ Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell
Open this post in threaded view
|
Report Content as Inappropriate

Re: Abusing quickcheck to check existential properties

 On Sun, 19 Oct 2008 00:39:32 +0200, Norman Ramsey <[hidden email]> 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 _______________________________________________ Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell
Open this post in threaded view
|
Report Content as Inappropriate

Re: Abusing quickcheck to check existential properties

 In reply to this post by Norman Ramsey-2 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 _______________________________________________ Haskell mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell