[Haskell] Abusing quickcheck to check existential properties

[Rickard Nilsson]

On Sun, 19 Oct 2008 00:39:32 +0200, Norman Ramsey <nr at 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