quickcheck tutorial 0.0.1

This post follows this one.

• Checking properties defined from built-in types

So far, we have seen how to define properties when their free variables were of types  bool, int or bigint. Other primary types are handled by default. These are double, complex, char and string.

Whereas any value of the bool and int types is equiprobable ($\frac{1}{2}$ for bool, $\frac{1}{2^{32}}$ for int), some assumptions were made  for the possible values returned by the other types. A produced bigint value, for instance, can't have a length greater than 256 in decimal. The same restriction applies to string values. Also, some restrictions have been added to concentrate the distribution of the double and complex values around 0. Finally, only 573 possible characters for char values have been kept from the unicode set without any justification and this decision affects the content of any string values.

Two useful types have also been integrated by default:

1. shortint, represents an integer between 0 and 255. Its values are equiprobable;
2. probability, represents a double between 0 and 1. Its values are uniformly distributed.

For instance, let's check the equality $E((X-E(X))^2)=E(X^2)-E(X)^2$ for the variance of $X$, say for 3 values.

> prop_Var p::probability q::probability x1::shortint x2::shortint x3::shortint =
>  E (map ((^2).(+-EX)) X) == E (map (^2) X) - EX^2
>    when X  = [x1,x2,x3];
>         EX = E X end 
>      with
>         E = foldr1 (+) . zipwith (*) [p, (1-p)*q, (1-p)*(1-q)];
>         a == b = abs (1-a/b) < 1e-11 end;

 You can call an evaluation for a particular set of arguments:
> prop_Var 0.3 0.4 3 5 8;
1
>

or run the tests:
> quickcheck prop_Var ;
OK, passed 100 tests.
()
>

If these defaults don't match your needs or if you want to build specific rules, see next section.

• User-defined types

Three steps are required for any new type definition.

1. Declaration of a nonfix symbol with the same name as the type name.
2. Definition of the new type.
3. Implementation of the rule which describes the creation of an arbitrary value of that type.

As an example, suppose we're trying to find a small counterexample of the wrong proposition saying that if $a$ is prime with $b$ and if $a$ prime with $c$ then $b$ is prime with $c$.

Of course, we could simply define:

> infix (mod) primewith;
> a primewith b = gcd a b == 1;

> prop_wrong_may_pass a::shortint b::shortint c::shortint =
>     a > 59 || b > 59 || c > 59 || ~ a primewith b || ~ a primewith c || b primewith c;

> quickcheck prop_wrong_may_pass ;
OK, passed 100 tests.
()
> quickcheck prop_wrong_may_pass ;
Falsifiable, after 30 tests:
[49,40,18]
()
>

 But, as the example shows, a single run could make believe that the proposition is true.

Instead, let's define a specific type in order to get rid of all the ignored cases:
> nonfix my_adequate_triple;
> type my_adequate_triple t::matrix =
>     all (>0) t && all (<60) t && t!0 primewith t!1 && t!0 primewith t!2;
> arbitrary  my_adequate_triple = {a,b,c}
>     when a = rnd;
>          b = primewith_ a;
>          c = primewith_ a end
>     with rnd = 1 + (abs random) mod 59;
>          primewith_ x =
>              if y primewith x then y
>                               else primewith_ x
>           when y = rnd end
>      end;

You can test if an arbitrary value fits the requirements:
> arbitrary my_adequate_triple ;
{29,34,38}
>
Then the property:
> prop_wrong t::my_adequate_triple = t!1 primewith t!2;
> quickcheck prop_wrong;
 Falsifiable, after 0 tests:
[{4,35,49}]
()
> quickcheck prop_wrong ;
Falsifiable, after 15 tests:
[{29,26,16}]
()
> quickcheck prop_wrong ;
Falsifiable, after 0 tests:
[{9,52,50}]
()
>

See you next time...