__Checking properties defined from built-in types__

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:

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

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

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

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