**Installation**

- Copy the quickcheck.pure file to your working directory (in pure, type > ! pwd (without >) to know where is it and > ! cd
*mydir*to change it if you wish). - Start pure (if it not already started).

**Working with quickcheck**

__Checking logical propositions__(built-ins).

> using quickcheck;

Suppose we want to check Pierce's law : $((a \Rightarrow b) \Rightarrow a) \Leftrightarrow a$.

First, declare some new operators (with arbitrarily the same priority as ||):

> infix (||) ==> <=>;

in order to define some helper functions:

> p ==> q = ~p || q;

> p <=> q = (p ==> q) && (q ==> p);

Then define the proposition (for the moment - May 2nd 2013 - it is impossible to include the arguments as lambdas in the definitions so the following proposition can't be defined as prop_Pierce = \ a::bool b::bool -> ((a ==> b) ==> a) <=> a yet):

> prop_Pierce a::bool b::bool = ((a ==> b) ==> a) <=> a;

This function is nothing but the mathematical predicate where the free variables have been explicitely given a type. Note that these (boolean here) types

*are*mandatory since this is the only way for the program to decide what the possible values for $a$ and $b$ are.

Finally, run the tests:

> quickcheck prop_Pierce;

The answer:

OK, passed 100 tests.

()

>

means that no contradiction was found (of course, a lot of the tests are redondant here since with 2 possible values for 2 variables, we could have get this result in 4 tests.)

__Checking numerical properties__(built-ins)

> distrib_mult_over_add_big a::bigint b::bigint c::bigint = a*(b+c) == a*b+a*c;

> quickcheck distrib_mult_over_add_big;

OK, tests are passed, we could have guessed. What about:

> distrib_mult_over_add a::int b::int c::int = a*(b+c) == a*b+a*c;

> quickcheck distrib_mult_over_add;

> quickcheck distrib_mult_over_add;

> quickcheck distrib_mult_over_add;

Tests always pass. But wait, isn't it surprinsing despite the possible overflows ? Well, it isn't since the int type is a sort of modular ring but we have to be

*careful with interpretation*and remember, for instance, that even if 2*(1500 000 000+1500 000 000) = 2*1500 000 000+2*1500 000 000, each member equals 1705032704.

Indeed, with:

> distrib_mult_over_add_mix a::int b::bigint c::int = a*(b+c) == a*b+a*c;

> quickcheck distrib_mult_over_add_mix;

the output:

Falsifiable, after 0 tests:

[-795755684,-9167850166993051345L,-1459775657]

>

warns that, with triple (a,b,c) where a=-795755684, b=-9167850166993051345L and c=-1459775657, the equality doesn't hold.

to be continued...

## Aucun commentaire:

## Enregistrer un commentaire