Abusing quickcheck to check existential properties

[Norman Ramsey-2]

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

[Koen Claessen]

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

[Norman Ramsey-2]

 > > 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

[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).

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 <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell

_______________________________________________
Haskell mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell

[Ben Moseley]

 > 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
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell

_______________________________________________
Haskell mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell

[Norman Ramsey-2]

 > 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

[rickynils]

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

[Colin Runciman]

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

[Norman Ramsey-2]

 > > 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
_______________________________________________
Haskell mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell