euc2003

[Thomas Arts]

Hi Luke

As Björn already pointed out, the version does handle recursive
datatypes definitions. A manual would have been useful ;-/.

A generator should be made such that it does not generate an
infinite datastructure. This is solved by first selecting a random
number (i.e. number of applications of constructor rules) and
then building the datatype of that size. The Size parameter should
decrease with at least 1 in every recursive call in the
generation.

In that sense, the function below seems to me still able to
produce an infinite datastructure:

> gb_set() ->
>     ?SIZED(N, resize(min(50, N),
> frequency(
> [{6,?LET(L, list(int()),
> return({'@',gb_sets,from_list,[L]}))},
> {6,?LET(L, list(int()),
> return({'@',gb_sets,from_ordset,[{'@',ordsets,from_list,[L]}]}))},
> {6,?LET(S,gb_set(),?LET(E,int(),
>   return({'@',gb_sets,add,[E,S]})))},
> {2,return({'@',gb_sets,empty,[]})},
> {2,?LET(E,int(),
> return({'@',gb_sets,singleton,[E]}))},
> {1,?LET(P,function(bool()),?LET(S,gb_set(),
> return({'@',gb_sets,filter,[P,S]})))}
>        ]))).

A better definition would be

gd_set() ->
    ?SIZED(Size,gd_set(Size)).

gd_set(Size) ->
frequency(
  [{6,?LET(L, list(int()),
       return({'@',gb_sets,from_list,[L]}))},
  {6,?LET(L, list(int()),
      return({'@',gb_sets,from_ordset,[{'@',ordsets,from_list,[L]}]}))},
  {6,?LET(S,gb_set(Size-1),    % change here
       ?LET(E,int(),
                 return({'@',gb_sets,add,[E,S]})))},
  {2,return({'@',gb_sets,empty,[]})},
  {2,?LET(E,int(),
     return({'@',gb_sets,singleton,[E]}))},
  {1,?LET(P,function(bool()),?LET(S,gb_set(Size-1),   % change here
     return({'@',gb_sets,filter,[P,S]})))}
  ]).

Note that this Size is NOT the size of the set (i.e. number of elements),
but
the number of applications of a function to construct a set. Moreover, it is
a kind of maximum number of applications, since if the non-recursive branch
is chosen, the size will be less.

If you now feel that this set is too small for a certain property, you could
resize it for testing that property, e.g.:
instead of

prop_not_empty() ->
    ?FORALL(X,gb_set(),
           ?IMPLIES(gb_sets:size(X) /= 0, not gb_sets:is_empty(X))).

one can use:

prop_not_empty() ->
    ?FORALL(X,resize(80,gb_set()),
           ?IMPLIES(gb_sets:size(X) /= 0, not gb_sets:is_empty(X))).

Note that the sets are bigger and testing takes longer.
If you find that the numbers in the sets are to restricted, i.e.,  you
only get sets with elements between -20 and +20, then you can do the
following
in the gd_set definition:

gd_set(Size) ->
frequency(
  [{6,?LET(L, list(resize(2000,int())),
       return({'@',gb_sets,from_list,[L]}))},
  {6,?LET(L, list(resize(2000,int())),
      return({'@',gb_sets,from_ordset,[{'@',ordsets,from_list,[L]}]}))},
  {6,?LET(S,gb_set(Size-1),    % change here
       ?LET(E,resize(2000,int()),
                 return({'@',gb_sets,add,[E,S]})))},
  {2,return({'@',gb_sets,empty,[]})},
  {2,?LET(E,int(),
     return({'@',gb_sets,singleton,[E]}))},
  {1,?LET(P,function(bool()),?LET(S,gb_set(Size-1),   % change here
     return({'@',gb_sets,filter,[P,S]})))}
  ]).


making the integers taken from a larger interval.
Similar, one can take larger lists as generators by writing
resize(100,list()).

Hope this clarifies a bit our thoughts. John and I are going to
write a paper about quickcheck and make some documentation
and examples as soon as time permits.

Cool that we got so much positive feedback on this application!
Thomas

---
Dr Thomas Arts
     Program Manager
     Software Engineering and Management
IT-university in Gothenburg
Box 8718, 402 75 Gothenburg, Sweden
http://www.ituniv.se/

Tel +46 31 772 6031
Fax +46 31 772 4899