[Haskell] Abusing quickcheck to check existential properties

Norman Ramsey nr at cs.tufts.edu
Sun Oct 12 13:38:05 EDT 2008


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


More information about the Haskell mailing list