[m-dev.] for review: quickcheck user guide
Xiao Chun Simon MEI
xcsm at students.cs.mu.oz.au
Sat Feb 24 04:26:48 AEDT 2001
For Mark to review.
The tutes are probably best viewed by a web browser at www.cs.mu.oz.au/~xcsm
Estimated hours taken : 70
A collection of web pages written as a user guide for quickcheck.
It covers the syntax and features supported by the current version of
quickcheck.
extras/quickcheck/tutes/T1.html:
extras/quickcheck/tutes/T2.html:
extras/quickcheck/tutes/T3.html:
extras/quickcheck/tutes/T4.html:
extras/quickcheck/tutes/T5.html:
extras/quickcheck/tutes/T6.html:
extras/quickcheck/tutes/T7.html:
extras/quickcheck/tutes/T8.html:
extras/quickcheck/tutes/T9.html:
extras/quickcheck/tutes/T10.html:
New files, each html covers a topic.
extras/quickcheck/tutes/index.html:
New file, the index.
extras/quickcheck/tutes/mymax.m:
extras/quickcheck/tutes/nrev.m:
extras/quickcheck/tutes/nrev2.m:
New files, contains mymax/2, nrev/1 and nrev/2.
extras/quickcheck/tutes/use.m:
extras/quickcheck/tutes/use1.m:
extras/quickcheck/tutes/use11.m:
extras/quickcheck/tutes/use20.m:
extras/quickcheck/tutes/use21.m:
extras/quickcheck/tutes/use22.m:
extras/quickcheck/tutes/use31.m:
extras/quickcheck/tutes/use33.m:
extras/quickcheck/tutes/use51.m:
extras/quickcheck/tutes/use62.m:
extras/quickcheck/tutes/use71.m:
extras/quickcheck/tutes/use81.m:
extras/quickcheck/tutes/use91.m:
New files, contains examples shown in each tutorial.
Index: mercury/extras/quickcheck/tutes/T1.html
===================================================================
RCS file: T1.html
diff -N T1.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T1.html Sat Feb 24 03:23:44 2001
@@ -0,0 +1,245 @@
+<html>
+<head>
+ <TITLE> QuickCheck </TITLE>
+</head>
+Files :
+<a href="use.m">use.m</a>
+<a href="use1.m">use1.m</a>
+<a href="use11.m">use11.m</a>
+<a href="nrev.m">nrev.m</a>
+<a href="nrev2.m">nrev2.m</a><BR>
+<a href="index.html">Back to main</a>
+
+<H1> QuickCheck Tutorial 1 </H1>
+
+
+<pre>
+Quickcheck is a tool which aids the Mercury programmer in formulating and
+testing properties of programs. The programmer must supply invariant
+functions which test certain properties of the programs. Those invariant
+functions can then be automatically tested on random inputs. It is
+possible to alter the test data distribution or define a custom test
+data generator.
+
+In order to test the validity of a predicate/function via quickcheck,
+you need the following components :
+ qcheck.m -- quickcheck module (supplied)
+ rnd.m -- required by quickcheck module (supplied)
+ XXX.m -- module containing the predicate/function
+ the user is trying to validate
+ YYY.m -- main module, which calls qcheck/4
+
+A Simple Example
+Let XXX.m be "nrev.m", which contains nrev/1 :
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+ :- func nrev(list(T)) = list(T).
+ :- mode nrev(in) = out is det.
+ nrev([]) = [].
+ nrev([X|Xs]) = Ys :-
+ list__append(nrev(Xs), [X], Ys).
+</pre></tr></table>
+We want to test whether nrev/1 is properly implemented.
+
+Let YYY.m be "use.m". It must contain a main/2, and an
+invariant function. If nrev/1 is correctly implemented then it
+should satisfy the following rules:
+<H4>
+ reverse [x] = [x]
+ reverse (xs+ys) = reverse ys + reverse xs
+ reverse (reverse xs) = xs
+</H4>
+To test whether 2nd rule holds for nrev/1, define the invariant
+function as :
+<H4>
+ testing(Xs, Ys) =
+ nrev(Xs ++ Ys) `===` (nrev(Ys) ++ nrev(Xs)).
+</H4>
+`===` function returns 'property:[yes]' if the left side equals
+right side, 'property:[no]' otherwise.
+In theory nrev/1 can take a list(T), however in order for
+quickcheck to automatically generate Xs and Ys, the programmer must
+specify a fixed type at which the law is to be tested, eg:
+<H4>
+ :- func testing(list(int), list(int)) = property.
+ Or
+ :- func testing(list(char), list(char)) = property.
+</H4>
+Now define the main/2 as
+<H4>
+ main --- >
+ qcheck(qcheck_f(testing), "sample testing").
+</H4>
+The complete use.m looks like this:
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+
+:- module use.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%-------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, list.
+:- import_module qcheck, nrev.
+
+%-------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(testing), "sample testing").
+
+%-------------------------------------------------------------------%
+% Invariant test functions
+%-------------------------------------------------------------------%
+
+:- func testing(list(int), list(int)) = property.
+testing(Xs, Ys) =
+ nrev(Xs ++ Ys) `===` (nrev(Ys) ++ nrev(Xs)).
+</pre></tr></table>
+To compile the program, do "mmake use.depend", then "mmake use".
+After running, the statistics should be displayed like :
+<H4>
+ Test Description : sample testing
+ Number of test cases that succeeded : 100
+ Number of trivial tests : 0
+ Number of tests cases which failed the pre-condition : 0
+ Distributions of selected argument(s) :
+</H4>
+nrev/1 passed 100 tests and failed none (ignore the last 3 lines
+for now).
+
+If the invariant function is wrongly specified, or nrev/1 is not
+properly implemented, then the statistics may look like :
+<H4>
+ Test description : sample testing
+ Falsifiable :
+ [2]
+ [-2, 1]
+</H4>
+where running [2] as Xs and [-2, 1] as Ys failed the invariant function.
+
+Defining an invariant function which contains only functions is more
+concise than one which contains predicates. Suppose that "nrev2.m"
+defines a predicate version of reversing list:
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+ :- pred nrev2(list(T), list(T)).
+ :- mode nrev2(in, out) is det.
+ nrev2([], []).
+ nrev2([X|Xs], Ys):-
+ nrev2(Xs, Reversed),
+ list__append(Reversed, [X], Ys).
+</pre></tr></table>
+Then the invariant function looks like :
+<h4>
+ testing2(Xs, Ys) = (Left `===` Right) :-
+ nrev2((Xs ++ Ys), Left),
+ nrev2(Ys, Part_a),
+ nrev2(Ys, Part_b),
+ Right = Part_a ++ Part_b.
+</h4>
+Above code is effectively the same as testing/2, however it requires a few extra
+lines to extract the intermediate values, (use1.m) :
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- module use1.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%-------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, list.
+:- import_module qcheck, nrev2.
+
+%-------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(testing2), "testing2").
+
+%-------------------------------------------------------------------%
+% Invariant test functions
+%-------------------------------------------------------------------%
+
+:- func testing2(list(int), list(int)) = property.
+testing2(Xs, Ys) = (Left `===` Right) :-
+ nrev2((Xs ++ Ys), Left),
+ nrev2(Ys, Part_a),
+ nrev2(Xs, Part_b),
+ Right = Part_a ++ Part_b.
+</pre></tr></table>
+An alternative to writing a separate invariant function is to
+use Mercury's syntax for higher order terms. When doing this,
+the `with_type` operator can be useful to provide fixed types
+for the arguments of the invariant function. For example (use11.m):
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- module use11.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%--------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, list.
+:- import_module qcheck, nrev.
+
+%--------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(func(Xs `with_type` list(int), Ys `with_type` list(int))
+ = nrev(Xs ++ Ys) `===` (nrev(Ys) ++ nrev(Xs))),
+ "sample testing").
+</pre></tr></table>
+
+In YYY.m, the main/2 should be defined as :
+<h4>
+ main --->
+ qcheck(qcheck_f(Invariant_Function_X), Test_Desc_Y).
+</h4>
+Where Invariant_Function_X is a higher order term (function) and
+Test_Desc_Y is a string which describe/name/comment Invariant_Function_X.
+
+The invariant function is of the form
+<h4>
+ :- mode Invariant_Function_X(in, in, in ...) = out.
+</h4>
+The invariant function can only take 0 to 10 arguments, but the inputs can
+be of any type. All invariant functions must return a property, which is just
+a list of flags.
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+ :- type property == list(flag).
+
+ :- type flag
+ ---> yes
+ ; no
+ ; trivial
+ ; info(univ)
+ ; condition.
+</pre></tr></table>
+What ever happens inside Invariant_Function_X, quickcheck does not care. If
+the output does not contain 'flag:no' the invariant function is assumed to
+pass the testcase satisfactory.
+
+<a href="T4.html">Click here to get the details on each individual flag.</a>
+</html>
Index: mercury/extras/quickcheck/tutes/T10.html
===================================================================
RCS file: T10.html
diff -N T10.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T10.html Sat Feb 24 03:23:44 2001
@@ -0,0 +1,54 @@
+<html>
+<head>
+ <TITLE> QuickCheck </TITLE>
+</head>
+<a href="index.html">Back to main</a>
+<H1> QuickCheck Tutorial 10 </H1>
+<h3> Summary - Generators </h3>
+<pre>
+
+Quickcheck is able to generate random values for each input
+argument at run time, provided that there is a default/custom
+generator for that type. The master seed for randomness is the
+current time.
+
+Quickcheck generates value via the following steps:
+
+ 1 The master generator is called with 7 arguments.
+ Arg1 type_desc of the required term
+ Arg2 SF for the current term
+ Arg3 a list of all GF
+ Arg4 a list of all custom generators
+ Arg5 ouputs a univ of the generated term
+ Arg6 random number supply input
+ Arg7 random number supply output
+
+ 2a Quickcheck searches through the list of custom generators,
+ if there is a custum generator for the current term, then
+ call the custom generator with Arg1, 2, 3, 4, 6, 7.
+ The master generator will return what ever is returned by the
+ custom generator.
+
+ 2b If Quickcheck fails to locate a custom generator, then it will
+ classify the current term as of type int, char, float, string,
+ discriminated union, and other.
+
+ 3b1 If it's type int, call rand_int/2 with Arg6 and Arg7
+
+ 3b2 If it's type char, call rand_char/2 with Arg6 and Arg7
+
+ 3b3 If it's type float, call rand_float/2 with Arg6 and Arg7
+
+ 3b4 If it's type string, call rand_string/2 with Arg6 and Arg8
+
+ 3b5 If it's type discriminated union, call rand_union/6 with
+ Arg1, Arg2, Arg3, Arg4, Arg6, Arg7.
+
+ 3b6 If it's classified as other, then call rand_function with Arg1,
+ Arg6 and Arg7. Quickcheck will generates the appropriate value if
+ Arg1 is of a function with arity 0 to 10. Otherwise an error will
+ be thrown :
+ "no default generator for this type"
+
+
+
Index: mercury/extras/quickcheck/tutes/T2.html
===================================================================
RCS file: T2.html
diff -N T2.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T2.html Sat Feb 24 03:23:44 2001
@@ -0,0 +1,164 @@
+<html>
+<head>
+ <TITLE> QuickCheck </TITLE>
+</head>
+<H1> QuickCheck Tutorial 2 </H1>
+Files :
+<a href="use20.m">use20.m</a>
+<a href="use21.m">use21.m</a>
+<a href="use22.m">use22.m</a>
+<a href="mymax.m">mymax.m</a><BR>
+<a href="index.html">Back to main</a>
+<h3> Conditional law </h3>
+
+<pre>
+In general many laws hold only under certain conditions. Quickcheck provides
+an implication combinator to represent such conditional laws. Eg, the law
+ X =< Y => max x y == y
+can be represented by the definition :
+<h4>
+ :- func law(int, int) = property.
+ law(X, Y) = (X =< Y) `===>` (mymax(X, Y) `===` Y).
+</h4>
+or alternatively can be represented as :
+<h4>
+ :- func law2(int, int) = property.
+ law2(X, Y) = is_less_equal(X, Y) `===>` (mymax(X, Y) `===` Y).
+
+ :- func is_less_equal(int, int) = bool.
+ is_less_equal(X, Y) = Bool :-
+ (if X =< Y
+ then
+ Bool = yes
+ else
+ Bool = no
+ ).
+</h4>
+The difference between law1 and law2 is the left argument of `===>`.
+(X =< Y) is type (pred) and is_less_equal(X, Y) returns type bool.
+`===>` is overloaded to take both types.
+
+
+The complete use20.m :
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- module use20.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, list, bool.
+:- import_module qcheck, mymax.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(law), "testing mymax using `===>` for (pred)"),
+ qcheck(qcheck__f(law2), "testing mymax using `===>` for bool").
+
+:- func law(int, int) = property.
+law(X, Y) = (X =< Y) `===>` (mymax(X, Y) `===` Y).
+
+:- func law2(int, int) = property.
+law2(X, Y) = is_less_equal(X, Y) `===>`
+ (mymax(X, Y) `===` Y).
+
+:- func is_less_equal(int, int) = bool.
+is_less_equal(X, Y) = Bool :-
+ (if X =< Y
+ then
+ Bool = yes
+ else
+ Bool = no
+ ).
+</pre></tr></table>
+After running the program, test statistics will be something like:
+<h4>
+ Test Description : testing mymax using `===>` for (pred)
+ Number of test cases that succeeded : 52
+ Number of trivial tests : 0
+ Number of tests cases which failed the pre-condition : 48
+ Distributions of selected argument(s) :
+
+ Test Description : testing mymax using `===>` for bool
+ Number of test cases that succeeded : 52
+ Number of trivial tests : 0
+ Number of tests cases which failed the pre-condition : 48
+ Distributions of selected argument(s) :
+</h4>
+The default number of tests to run is 100. In the above test, 48/100 cases
+passed the invariant function, and none failed. However, there are 52/100
+cases where the inputs failed the pre-condition.
+
+Note that both test cases succeeded 52/100 and failed pre-condition 48/100.
+qcheck.m seeds the random generator on local time, if qcheck is called twice
+within the same second, the number generated will be the same.
+
+The implication combinator can be compounded. For example, suppose mymax is
+designed that if mymax(X, Y) is called, Y will never be zero. Thus test cases
+with Y=0 should also be disregarded (use21.m) :
+<h4>
+ :- func law(int, int) = property.
+ law(X, Y) = notzero(Y) `===>` ((X =< Y) `===>` (mymax(X, Y) `===` Y)).
+
+ :- pred notzero(int).
+ :- mode notzero(in) is semidet.
+ notzero(X) :- X \= 0.
+</h4>
+
+The right argument of `===>` is also overload, as shown in use22.m :
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- module use22.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, bool.
+:- import_module qcheck.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(law1), "passing property"),
+ qcheck(qcheck__f(law2), "passing (func) = property").
+
+:- func law1(int, int) = property.
+law1(X, Y) = notzero(Y) `===>` qcheck__f( (func) = ((X // Y) `===` (X // Y)) ).
+
+:- func law2(int, int) = property.
+law2(X, Y) = notzero(Y) `===>` ( (X // Y) `===` (X // Y) ).
+
+:- pred notzero(int).
+:- mode notzero(in) is semidet.
+notzero(X) :- X \= 0.
+</pre></tr></table>
+The difference between law1/2 and law2/2 is the right argument of `===>`.
+law1/2 passed (func), while law2/2 passed property. In law2/2, (X // Y) is
+always evaluated, which will cause error if Y is zero. However, in law1/2
+(X // Y) is not evaluated if `===>`'s left argument is 'bool:no' or
+'(pred):failure'.
+
+The implication combinator '===>' marks a test that has failed pre-condition
+by inserting 'flag:condition' into the property in cases where the right
+argument is a property; in cases where the right argument is (func), then
+`===>` will just return 'property:[condition]'.
+If the property list contains one or more 'condition', the test result is
+ignored.
+</html>
Index: mercury/extras/quickcheck/tutes/T3.html
===================================================================
RCS file: T3.html
diff -N T3.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T3.html Sat Feb 24 03:23:44 2001
@@ -0,0 +1,273 @@
+<html>
+<head>
+ <TITLE> QuickCheck </TITLE>
+</head>
+<H1> QuickCheck Tutorial 3 </H1>
+Files :
+<a href="use31.m">use31.m</a>
+<a href="use33.m">use33.m</a>
+<a href="nrev.m">nrev.m</a><BR>
+<a href="index.html">Back to main</a>
+<h3> Monitoring Test Data - to_trivial/3 </h3>
+
+<pre>
+In Tutorial 1, the 3rd rule for reverse is that:
+ reverse (reverse xs) = xs
+It's not much of a test if xs is empty list or list with only 1 element.
+
+Quickcheck can label a test being trivial via the function
+to_trivial/3, which does not change the meaning of a law, but it classifies
+some of the test cases. Without classifying the invariant function could be :
+<h4>
+ :- func testing1(list(float)) = property.
+ testing1(Xs) =
+ nrev (nrev Xs) `===` Xs.
+</h4>
+If the 1st argument of to_trivial/3 is equal to the 2nd argument, then that test
+case will be labeled trivial by pushing flag:trivial into the third argument
+( which is a list of flags ).
+testing2/1 treats empty list as trivial test.
+<h4>
+ :- func testing2(list(float)) = property.
+ testing2(Xs) =
+ to_trivial([], Xs, nrev (nrev Xs) `===` Xs).
+</h4>
+Use compounded to_trivial to also classify list of 1 element as trivial
+<h4>
+ :- func testing3(list(float)) = property.
+ testing3(Xs) =
+ to_trivial(1,
+ list_length(Xs),
+ to_trivial([], Xs, nrev(nrev(Xs)) `===` Xs)
+ ).
+</h4>
+The complete code (use31.m) :
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- module use31.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, list, bool.
+:- import_module qcheck, nrev.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(testing1), "testing1"),
+ qcheck(qcheck__f(testing2), "testing2"),
+ qcheck(qcheck__f(testing3), "testing3").
+
+:- func testing1(list(float)) = property.
+testing1(Xs) =
+ nrev(nrev(Xs)) `===` Xs.
+
+:- func testing2(list(float)) = property.
+testing2(Xs) =
+ to_trivial([], Xs, nrev(nrev(Xs)) `===` Xs).
+
+:- func testing3(list(float)) = property.
+testing3(Xs) =
+ to_trivial(1,
+ list_length(Xs),
+ to_trivial([], Xs, nrev(nrev(Xs)) `===` Xs)
+ ).
+</pre></tr></table>
+A sample output :
+<h4>
+ Test Description : testing1
+ Number of test cases that succeeded : 100
+ Number of trivial tests : 0
+ Number of tests cases which failed the pre-condition : 0
+ Distributions of selected argument(s) :
+
+ Test Description : testing2
+ Number of test cases that succeeded : 100
+ Number of trivial tests : 53
+ Number of tests cases which failed the pre-condition : 0
+ Distributions of selected argument(s) :
+
+ Test Description : testing3
+ Number of test cases that succeeded : 100
+ Number of trivial tests : 75
+ Number of tests cases which failed the pre-condition : 0
+ Distributions of selected argument(s) :
+</h4>
+Note test1, the original, has no trivial cases. With test2, 53/100 tests have
+an empty list as its input. Test3 shows 75/100 tests have either an empty list
+or a list of only one element. It only tested 25/100 cases where the list is
+longer than 1 element.
+
+
+<h3> Monitoring Test Data - `>>>` </h3>
+The combinator `>>>` gathers all values that are passed to it, and prints out
+a histogram of these values.
+Let's use `>>>` to find out exactly what lists are generated for the previous
+tests :
+<h4>
+ :- func testing4(list(float)) = property.
+ testing4(Xs) =
+ list_length(Xs) `>>>` (nrev(nrev(Xs)) `===` Xs).
+</h4>
+The combinator `>>>` will convert its left argument to a univ, and push
+info(univ) into the property list.
+The complete code (use31.m) :
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- module use31.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, list, bool.
+:- import_module qcheck, nrev.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(testing1), "testing1"),
+ qcheck(qcheck__f(testing2), "testing2"),
+ qcheck(qcheck__f(testing3), "testing3"),
+ qcheck(qcheck__f(testing4), "testing4").
+
+:- func testing1(list(float)) = property.
+testing1(Xs) =
+ nrev(nrev(Xs)) `===` Xs.
+
+:- func testing2(list(float)) = property.
+testing2(Xs) =
+ to_trivial([], Xs, nrev(nrev(Xs)) `===` Xs).
+
+:- func testing3(list(float)) = property.
+testing3(Xs) =
+ to_trivial(1,
+ list_length(Xs),
+ to_trivial([], Xs, nrev(nrev(Xs)) `===` Xs)
+ ).
+
+:- func testing4(list(float)) = property.
+testing4(Xs) =
+ list_length(Xs) `>>>` (nrev(nrev(Xs)) `===` Xs).
+</pre></tr></table>
+A sample output :
+<h4>
+Test Description : testing1
+Number of test cases that succeeded : 100
+Number of trivial tests : 0
+Number of tests cases which failed the pre-condition : 0
+Distributions of selected argument(s) :
+
+Test Description : testing2
+Number of test cases that succeeded : 100
+Number of trivial tests : 53
+Number of tests cases which failed the pre-condition : 0
+Distributions of selected argument(s) :
+
+Test Description : testing3
+Number of test cases that succeeded : 100
+Number of trivial tests : 71
+Number of tests cases which failed the pre-condition : 0
+Distributions of selected argument(s) :
+
+Test Description : testing4
+Number of test cases that succeeded : 100
+Number of trivial tests : 0
+Number of tests cases which failed the pre-condition : 0
+Distributions of selected argument(s) :
+1 8
+1 4
+1 6
+2 5
+8 3
+16 2
+18 1
+53 0
+</h4>
+The display of testing4 shows that 53 cases of length == 0
+ 18 cases of length == 1
+ 16 cases of length == 2
+ ...etc...
+53+18 cases = 71 cases, which were marked trivial in testing3, likewise
+for testing2. The numbers will add up only if all the tests were run with
+the same random number seed.
+
+
+The value passed to `>>>` does not have to be the same type, and `>>>` can
+be compounded like to_trivial/3, eg (use33.m):
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- module use33.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, list, bool.
+:- import_module qcheck, nrev.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(testing5), "testing5").
+
+:- func testing5(list(float)) = property.
+testing5(Xs) =
+ odd_even(Xs) `>>>`
+ (list_length(Xs) `>>>` (nrev(nrev(Xs)) `===` Xs)).
+
+:- func odd_even(list(T)) = string.
+:- mode odd_even(in) = out is det.
+odd_even(Xs) = Y :-
+ (if list_length(Xs) mod 2 = 1
+ then
+ Y = "odd"
+ else
+ Y = "even"
+ ).
+</pre></tr></table>
+testing5 collects the list_length, and also collect "odd" or "even"
+A sample output :
+<h4>
+Test Description : testing5
+Number of test cases that succeeded : 100
+Number of trivial tests : 0
+Number of tests cases which failed the pre-condition : 0
+Distributions of selected argument(s) :
+1 7
+1 5
+2 4
+2 6
+8 3
+10 2
+29 1
+39 "odd"
+47 0
+61 "even"
+</h4>
+
+</html>
+
Index: mercury/extras/quickcheck/tutes/T4.html
===================================================================
RCS file: T4.html
diff -N T4.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T4.html Sat Feb 24 03:23:44 2001
@@ -0,0 +1,88 @@
+<html>
+<head>
+ <TITLE> QuickCheck </TITLE>
+</head>
+<H1> QuickCheck Tutorial 4 </H1>
+
+<a href="index.html">Back to main</a>
+<h3> Summary - Invariant Function & Property </h3>
+
+<pre>
+The invariant function is of the form
+ :- func Invariant_Function_X(T, T1, T2 ...) = property
+ :- mode Invariant_Function_X(in, in, in ...) = out.
+The inputs can be of most types (details next tutorial), however only arity
+0 to 10 are implemented. The output must be property, defined as :
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+ :- type property == list(flag).
+
+ :- type flag
+ ---> yes
+ ; no
+ ; trivial
+ ; info(univ)
+ ; condition.
+</pre></tr></table>
+What ever happens inside Invariant_Function_X, quickcheck does not care; it only
+looks at the output property. Any form of property is valid, in the sense that
+the qcheck will not abort. However not all forms of property is sensible.
+One could return [], or [yes, no, yes, no]. Quickcheck analyzes the property in
+the following order:
+ 1 Firstly, qcheck determines whether the invariant function has
+ failed. This only occurs if the property list contains at least
+ one 'flag:no' and does not contain 'flag:condition'. In this
+ case the NOFLAG will be switched to 'bool:yes', and the message
+ "Falsifiable ... ..." is printed. Otherwise move to step 2.
+ 2 qcheck will then test if the 'condition' flag (1 or more) is
+ in the property list. If it is, then the FAILEDCONDITION counter
+ is incremented and stops analyzing. If the 'condition' flag is
+ not within the property list, then move to step 3.
+ 3 qcheck increments the YES counter.
+ 4 qcheck increments the TRIVIAL counter if it finds the 'trivial'
+ flag (1 or more) is within the list.
+ 5 Then qcheck gets all the info(univ) (if any) in the list and
+ merge that with the master list for distribution.
+So, [] will increase the YES counter, and [yes, no, yes, no] will switch the
+NOFLAG counter.
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- func T `===` T = property.
+:- mode in `===` in = out is det.
+Left `===` Right Left == Right return [yes]
+ Left != Right return [no]
+
+:- func (pred) `===>` property = property.
+:- mode in((pred) is semidet) `===>` in = out is det.
+Left `===>` Right Left fails return [condition | Right]
+ Left succeeds return Right
+
+:- func bool `===>` property = property.
+:- mode in `===>` in = out is det.
+Left `===>` Right Left == no return [condition | Right]
+ Left == yes return Right
+
+Note: :- type f0
+ ---> f((func) = property).
+
+:- func (pred) `===>` f0 = property.
+:- mode in((pred) is semidet) `===>` in = out is det.
+Left `===>` Right Left fails return [condition]
+ Left succeeds return apply(Right)
+
+:- func bool `===>` f0 = property.
+:- mode in `===>` in = out is det.
+Left `===>` Right Left == no return [condition]
+ Left == yes return apply(Right)
+
+:- func to_trivial(T, T, property) = property.
+:- mode to_trivial(in, in, in) = out is det.
+to_trivial(A, B, C) A == B return [trivial | C]
+ A != B return C
+
+:- func T `>>>` property = property.
+:- mode in `>>>` in = out is det.
+Left `>>>` Right return [ info(univ(Left)) | Right ]
+</pre></tr></table>
+
+
Index: mercury/extras/quickcheck/tutes/T5.html
===================================================================
RCS file: T5.html
diff -N T5.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T5.html Sat Feb 24 03:23:44 2001
@@ -0,0 +1,181 @@
+<html>
+<head>
+ <TITLE> QuickCheck </TITLE>
+</head>
+Files :
+<a href="use51.m">use51.m</a><BR>
+<a href="index.html">Back to main</a>
+<H1> QuickCheck Tutorial 5 </H1>
+<h3> Generators - Basic </h3>
+
+<pre>
+The invariant function is of the form
+ :- func Invariant_Function_X(T, T1, T2 ...) = property
+ :- mode Invariant_Function_X(in, in, in ...) = out.
+Quickcheck generates random values for each input argument at run time.
+The following types have default generators:
+ - int
+ - char
+ - float
+ - string
+ - some functions (more detail in Tutorial 8)
+ - any type defined as a discriminated union, provided
+ that all types in the body of the definition have
+ default/custom generators
+ - any type defined as being equivalent to a type with a
+ default/custom generator
+
+There is no code written to handle equivalent types. But it works
+as if the compiler replaced all the equivalent types with their real type
+before compiling.
+
+The default generator for int is rand_int/2, which has distribution:
+50% even distribution between [-100, 100]
+50% even distribution between [-2^31, 2^31]
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- func rand_int(rnd, rnd) = int.
+:- mode rand_int(in, out) = out is det.
+rand_int(BS0, BS) = Int :-
+ Temp = rand_allint(BS0, BS1) rem 2,
+ (if Temp = 0
+ then
+ irange(-100, 100, Int, BS1, BS)
+ else
+ Int = rand_allint(BS1, BS)
+ ).
+
+:- func rand_allint(rnd, rnd) = int.
+:- mode rand_allint(in, out) = out is det.
+rand_allint(BS0, BS) = Int :-
+ next(1, Sign, BS0, BS1),
+ next(31, TempInt, BS1, BS),
+ ( Sign > 0 ->
+ Int = TempInt
+ ;
+ Int = -TempInt
+ ).
+</pre></tr></table>
+Default for char is rand_char/2, with even spread over
+char__to_int(Char, X) where X is (-1000, 1000).
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- func rand_char(rnd, rnd) = char.
+:- mode rand_char(in, out) = out is det.
+rand_char(RS0, RS) = Char :-
+ Int = rand_allint(RS0, RS1) rem 1000,
+ (if char__to_int(Char0, Int)
+ then
+ Char = Char0,
+ RS = RS1
+ else
+ Char = rand_char(RS1, RS)
+ ).
+</pre></tr></table>
+Default for float is rand_float/2, which has roughly even
+distribution over all discrete values for a 32-bit float.
+If machine is less then 32bits, overfloat occurs. It should still
+cover all possible values, but may alter distribution.
+If machine is more than 32bits, rand_float/2 will miss some values
+but retains even distribution.
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- func rand_float(rnd, rnd) = float.
+:- mode rand_float(in, out) = out is det.
+rand_float(BS0, BS) = Flt :-
+ next(31, Mant0, BS0, BS1),
+ next(1, Sign, BS1, BS2),
+ ( Sign > 0 ->
+ Mant = Mant0
+ ;
+ Mant = -Mant0
+ ),
+ next(7, Exp, BS2, BS3),
+ next(1, ExpSign, BS3, BS),
+ Flt0 = float(Mant) * pow(2.0, Exp),
+ ( ExpSign > 0, Flt0 \= 0.0 ->
+ Flt = 1.0/Flt0
+ ;
+ Flt = Flt0
+ ).
+</pre></tr></table>
+Default for string is rand_string/2, each element is generated by
+rand_char/2.
+0.9^0 * 0.1 chance being string length == 0
+0.9^1 * 0.1 chance being string length == 1
+0.9^2 * 0.1 chance being string length == 2
+...etc...
+So the mean string length is Sum(0.1* 0.9^N * N) where N <- {0, infinity},
+which converges to 9.
+
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- func rand_string(rnd, rnd) = string.
+:- mode rand_string(in, out) = out is det.
+rand_string(RS0, RS) = X :-
+ gen(Charlist, [], [ {type_of(['A']), [{10,[]},{90,[]}]} ],
+ [], RS0, RS),
+ string__from_char_list(Charlist,X).
+</pre></tr></table>
+Note that the default generator for stirng actually uses the default generator
+for discriminated union (indirectly).
+use51.m gives an illustration of generating int, char, float, string.
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- module use51.
+
+:- interface.
+
+:- type marks == int.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, char, float, string, list.
+:- import_module qcheck.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(junk), "just to show the inputs", 5, [], []).
+
+:- func junk(marks, char, float, string) = property.
+junk(A, B, C, D) =
+ {A,B,C,D} `>>>` [yes].
+</pre></tr></table>
+There are a few thing to note about use51.m :
+<h4>
+ qcheck(qcheck__f(junk), "just to show the inputs", 5, [], []).
+</h4>
+The 3rd argument is an int, which specifies how many times to run. In this
+example 5 tests are run , but the default is 100. The other auguments will
+be described later.
+<h4>
+ junk(A, B, C, D) =
+ {A,B,C,D} `>>>` [yes].
+</h4>
+the invariant function doesn't do any testing, it always succeeds. But
+`>>>` collects all the inputs.
+A Sample output
+<h4>
+ Test Description : just to show the inputs
+ Number of test cases that succeeded : 5
+ Number of trivial tests : 0
+ Number of tests cases which failed the pre-condition : 0
+ Distributions of selected argument(s) :
+ 1 {-50, '4', -3.55475907854864e+25, "\241r\371~~\316\002LJ~\204\246"}
+ 1 {27, '\342', -311727734390784., "\377g.\001"}
+ 1 {1389908257, '8', 2.63071847153664e+15, "\342"}
+ 1 {-90973704, '<', -2.10559053720692e-22, ""}
+ 1 {-896549770, 's', 7.72155851221736e+30, "[\230m\304\2561\254Q"}
+</h4>
+The char and string output doesn't look pretty, since most are not printable,
+eg: \342, \254
+
+
Index: mercury/extras/quickcheck/tutes/T6.html
===================================================================
RCS file: T6.html
diff -N T6.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T6.html Sat Feb 24 03:23:44 2001
@@ -0,0 +1,363 @@
+<html>
+<head>
+ <TITLE> QuickCheck </TITLE>
+</head>
+Files :
+<a href="use62.m">use62.m</a><BR>
+<a href="index.html">Back to main</a>
+<H1> QuickCheck Tutorial 6 </H1>
+<h3> Generators - Discriminated union & Specific Frequency</h3>
+<pre>
+Default generator is able to generate discriminated unions provided that all types
+in the body of the definition have default/custom generators. In default frequency
+mode, all branches at each level have the same chance of being selected.
+
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- func rand_union(type_desc, list(frequency), list({type_desc,
+ list(frequency)}), list(user_gen_type), rnd, rnd) = univ.
+:- mode rand_union(in,in,in,list_skel_in(user_gen_inst),in,out) = out is det.
+</pre></tr></table>
+use61.m shows the randomly generated value for the type bullet, with default
+frequency :
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- module use61.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module list.
+:- import_module qcheck.
+
+%---------------------------------------------------------------------------%
+% arbitrary user-defined types for testing purposes
+%---------------------------------------------------------------------------%
+
+:- type bullet
+ ---> good(color)
+ ; inaccurate(color)
+ ; defective(color).
+
+:- type color
+ ---> black
+ ; white.
+
+%---------------------------------------------------------------------------%
+main -->
+ qcheck(qcheck__f(prop1), "even distribution", 1000, [], []).
+
+:- func prop1(bullet) = property.
+prop1(X) = X `>>>` [yes].
+</pre></tr></table>
+Sample output shows the expected distribution :
+<h4>
+ Test Description : even distribution
+ Number of test cases that succeeded : 1000
+ Number of trivial tests : 0
+ Number of tests cases which failed the pre-condition : 0
+ Distributions of selected argument(s) :
+ 150 inaccurate(white)
+ 153 defective(black)
+ 165 inaccurate(black)
+ 176 good(white)
+ 178 defective(white)
+ 178 good(black)
+</h4>
+
+<h3> Specific Frequency</h3>
+Specific Frequency changes a term's default frequency (which is evenly spread)
+to one the user has provided. General Frequency changes a type's default frequency
+to one the user has provided. An example :
+<h4>
+ :- func Invariant_Function_X(bullet, bullet) = property.
+</h4>
+Different SF can be passed to the first and second bullet. For example, the first
+bullet can have 80% chance of being black, while the second argument has 20% chance
+of being black. However there can only be one GF for each type.
+The key advantage of Specific Frequency over General Frequency is that it allows
+different frequencies for the same type, where GF doesn't allow.
+The draw back is that SF only goes as deep (down the branches) as the user
+defines it, and the amount of work blows up as the depth of branches increases.
+
+Suppose there are two bullet manufacturers.
+Company_W 's bullet are painted black, and 50% good ones, 10% inaccurate, 40% defective.
+Company_B 's bullet are painted white, and 40% good ones, 30% inaccurate, 30% defective.
+A good bullet always hits its target, inaccurate one misses 50% of time, defective bullet
+always misses. And color does affect performance.
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- type frequency
+ ---> {int, list(list(frequency))}.
+</pre></tr></table>
+frequency defines the relative chance of a branch being selected, and gives information
+of that branch's sub-branches.
+list(frequency) contains distribution information about 1 discrimated union, ie: the list
+must contain a frequency for each possible branch.
+list(list(frequency)) contains distribution information about a list of discrimated unions.
+<P>
+<table border=1 width=100%><tr><td><pre>
+Let's try to describe Company_W's bullet, Bullet is discrimated union, so the list is 3 length long :
+ list(frequency)
+There are 3 top level branches for Type Bullet, so the list is 3 length long :
+ [frequency_good, frequency_inaccurate, frequency_defective]
+
+ :- type frequency = {int, list(list(frequency))}.
+ frequency_good = {50, ...something_good...}
+ frequency_inaccurate = {10, ...something_inaccurate...}
+ frequency_defective = {40, ...something_defective...}
+
+Any int is a valid 1st argument of frequency, however negative numbers is viewed
+by qcheck as zeros.
+
+chance of good-bullet is 50 / (50 + 10 + 40)
+the chance of inaccurate is 10 / (50 + 10 + 40)
+the chance of defective is 40 / (50 + 10 + 40)
+
+Another example (for type bullet):
+
+:- type frequency = {int, list(list(frequency))}.
+frequency_good = {5, ...something_good...}
+frequency_inaccurate = {1, ...something_inaccurate...}
+frequency_defective = {4, ...something_defective...}
+
+the chance of good-bullet is 5 / (5 + 1 + 4)
+the chance of inaccurate is 1 / (5 + 1 + 4)
+the chance of defective is 4 / (5 + 1 + 4)
+
+In both example the result distribution is the same. ie (50% good,
+10% inaccurate, 40% defective).
+
+...something_good... has format list(list(frequency)), and should describe the argument(s) of good/1.
+good/1 only has 1 arguments, thus the list of 1 element,
+ [ info_color ]
+info_color has format list(frequency), color has 2 branches, thus this list is of 2 elements.
+ [ frequency_black, frequency_white ]
+
+ :- type frequency = {int, list(list(frequency))}.
+ frequency_black = {100, ...something_black...}
+ frequency_white = {0, ...something_white...}
+
+something_black has format list(list(frequency)), and should describe the argument(s) of black/0.
+black/0 has no argument, thus the list is [], likewise for white/0.
+If instead of black/0, it's black/3, eg:
+<h4>
+ :- type color
+ ---> black(paint_manufacturer, warranty_type, warranty_provider)
+ ; white(paint_manufacturer, warranty_type, warranty_provider)
+</h4>
+Then you can either use [] to use default frequeny for generating paint_manufacturer, warranty_type,
+and warranty_provider. Or you can specify a list of 3 element ; each element describing the frequency
+of paint_manufacturer, warranty_type or warranty_provider.
+
+So far: info_color = [ frequency_black, frequency_white ]
+ = [ {100, []}, {0, []} ]
+Then: frequency_good = {50, ...something_good...}
+ = {50, [ info_color ] }
+ = {50, [ [ {100, []}, {0, []} ] ] }
+
+in this case ...something_good..., ...something_inaccurate... and ...something_defective are the same,
+since they all describe a list which contains Color that has the same distribution.
+
+So: frequency_good = {50, [ [ {100, []}, {0, []} ] ] }
+ frequency_inaccurate = {10, [ [ {100, []}, {0, []} ] ] }
+ frequency_defective = {40, [ [ {100, []}, {0, []} ] ] }
+
+Then: [frequency_good, frequency_inaccurate, frequency_defective]
+ = [ {50, [ [ {100, []}, {0, []} ] ] },
+ {10, [ [ {100, []}, {0, []} ] ] },
+ {40, [ [ {100, []}, {0, []} ] ] }
+ ]
+
+For Company_W 's bullet , it's list(frequency) would be :
+ [frequency_good, frequency_inaccurate, frequency_defective]
+ = [ {40, [ [ {0, []}, {100, []} ] ] },
+ {30, [ [ {0, []}, {100, []} ] ] },
+ {30, [ [ {0, []}, {100, []} ] ] }
+ ]
+</pre></tr></table>
+The complete code (use62.m) :
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- module use62.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, list, string.
+:- import_module qcheck, rnd.
+
+%---------------------------------------------------------------------------%
+% arbitrary user-defined types for testing purposes
+%---------------------------------------------------------------------------%
+
+:- type bullet
+ ---> good(color)
+ ; inaccurate(color)
+ ; defective(color).
+
+:- type color
+ ---> black
+ ; white.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ { freq_B(B) },
+ { freq_W(W) },
+ qcheck(qcheck__f(prop2), "bullet fight", 10000, [[],B,W], []).
+
+:- pred freq_B(list(frequency)).
+:- mode freq_B(out) is det.
+freq_B(Out) :-
+ Out = [ {50, [ [ {100, []}, {0, []} ] ] },
+ {10, [ [ {100, []}, {0, []} ] ] },
+ {40, [ [ {100, []}, {0, []} ] ] }
+ ].
+
+:- pred freq_W(list(frequency)).
+:- mode freq_W(out) is det.
+freq_W(Out) :-
+ Out = [ {40, [ [ {0, []}, {100, []} ] ] },
+ {30, [ [ {0, []}, {100, []} ] ] },
+ {30, [ [ {0, []}, {100, []} ] ] }
+ ].
+
+:- func prop2(int, bullet, bullet) = property.
+prop2(Seed, B, W) = fight(Seed, B, W) `>>>`
+ ({"ComB",B} `>>>`
+ ({"ComW", W} `>>>` [yes])
+ ).
+
+:- func fight(int, bullet, bullet) = string.
+:- mode fight(in, in, in) = out is det.
+fight(Seed, B, W) = String :-
+ rnd__init(Seed, RS0),
+ B_hit = is_hit(B, RS0, RS1),
+ W_hit = is_hit(W, RS1, _),
+ (if B_hit = W_hit
+ then
+ String = "draw"
+ else if B_hit > W_hit
+ then
+ String = "B win"
+ else
+ String = "W win"
+ ).
+
+:- func is_hit(bullet, rnd, rnd) = int.
+:- mode is_hit(in, in, out) = out is det.
+is_hit(Bullet, RS0, RS) = Int :-
+ Temp = rand_allint(RS0, RS) rem 2,
+ (
+ Bullet = good(_),
+ Int = 1
+ ;
+ Bullet = inaccurate(_),
+ (if Temp = 0
+ then
+ Int = 1
+ else
+ Int = 0
+ )
+ ;
+ Bullet = defective(_),
+ Int = 0
+ ).
+</pre></tr></table>
+In use62.m
+<h4>
+main -->
+ { freq_B(B) },
+ { freq_W(W) },
+ qcheck(qcheck__f(prop2), "bullet fight", 10000, [[],B,W], []).
+</h4>
+The 4th argument of qcheck/7 is for passing Specific Frequency. Because the
+invariant function has three input arguments, qcheck/7 's 4th argument must
+be list of 3.
+ [[],B,W]
+
+The first argument of prop2/3 is of type int, and I've passed [] as
+it's SF. When qcheck is trying to generate that int, it will completely
+ignore the [] since an int is not a discriminated union. In that sense,
+one can replace that [] with anything, as long as it's the correct format ;
+ie, a list(frequency). However the presence of [] will allow qcheck to
+recognize that [] is for the first argument, B is for the second argument and
+W is for the third argument.
+
+A sample output:
+<h4>
+ Test Description : bullet fight
+ Number of test cases that succeeded : 10000
+ Number of trivial tests : 0
+ Number of tests cases which failed the pre-condition : 0
+ Distributions of selected argument(s) :
+ 909 {"ComB", inaccurate(black)}
+ 2403 "B win"
+ 2533 "W win"
+ 2949 {"ComW", defective(white)}
+ 3012 {"ComW", inaccurate(white)}
+ 4017 {"ComB", defective(black)}
+ 4039 {"ComW", good(white)}
+ 5064 "draw"
+ 5074 {"ComB", good(black)}
+</h4>
+Regroup the output to make comparison :
+
+5074 {"ComB", good(black)
+909 {"ComB", inaccurate(black)}
+4017 {"ComB", defective(black)}
+
+4039 {"ComW", good(white)}
+3012 {"ComW", inaccurate(white)}
+2949 {"ComW", defective(white)}
+
+Note that ComB only makes black bullet; ComW only white. And their bullet quality is
+what was expected of them.
+
+2403 "B win"
+2533 "W win"
+5064 "draw"
+
+
+Walk through in generating a Company_B 's bullet :
+
+ 1 The program first enters the generator with
+ SF = [ {50, [ [ {100, []}, {0, []} ] ] },
+ {10, [ [ {100, []}, {0, []} ] ] },
+ {40, [ [ {100, []}, {0, []} ] ] }
+ ].
+
+ 2 Suppose the 3rd branch is selected, then qcheck will extract
+ [ {100, []}, {0, []} ] from {40, [ [ {100, []}, {0, []} ] ] }
+
+ 3 It then calls the generator with SF = [ {100, []}, {0, []} ]
+
+ 4 So qcheck enters generator for the sub-branch (for color) with
+ SF = [ {100, []}, {0, []} ]
+
+ 5 Suppose the 1st branch is selected, then qcheck will extract []
+ from {100, []}
+
+ 6 Since constructor black/0 has no argument, the program will stop
+ the recursive call.
+
+
+
+
Index: mercury/extras/quickcheck/tutes/T7.html
===================================================================
RCS file: T7.html
diff -N T7.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T7.html Sat Feb 24 03:23:44 2001
@@ -0,0 +1,258 @@
+<html>
+<head>
+ <TITLE> QuickCheck </TITLE>
+</head>
+Files :
+<a href="use71.m">use71.m</a><BR>
+<a href="index.html">Back to main</a>
+<H1> QuickCheck Tutorial 7 </H1>
+<h3> Generators - General Frequency</h3>
+<pre>
+
+General Frequency follows the ideas in Specific Frequency. You must understand
+the format of Specific Frequency in order to write General Frequency. However
+the amount of work in GF is usually less then in SP. In GF, the user should
+specify one level down in branches, where a practicl SP may be 3+ level down.
+
+Back in Tutorial 3, an invariant function was written to test the law :
+ reverse (reverse xs) = xs
+<h4>
+:- func testing4(list(float)) = property.
+testing4(Xs) =
+ list_length(Xs) `>>>` (nrev(nrev(Xs)) `===` Xs).
+
+Test Description : testing4
+Number of test cases that succeeded : 100
+Number of trivial tests : 0
+Number of tests cases which failed the pre-condition : 0
+Distributions of selected argument(s) :
+1 8
+1 4
+1 6
+2 5
+8 3
+16 2
+18 1
+53 0
+</h4>
+The display of testing4 shows that 53 cases of lenggh == 0
+ 18 cases of length == 1
+ 16 cases of length == 2
+ ...etc...
+The length of of the list is heavily biased towards the short end. In the limit with
+even distribution along the branches, the list will have :
+50% length == 0
+25% length == 1
+12.5% length == 2
+6.25% length == 3
+3.125% length == 4
+...etc... halfing the probability in eash step.
+<h4>
+ :- type list(T)
+ ---> []
+ ; [T | list(T)].
+</h4>
+At any given length accumulated so far, there is a 50-50 chance of either
+stopping there (if the first branch is chosen) or going on to a longer
+list (if the second branch is chosen).
+
+The 5th argument of qcheck/7 takes General Frequency, it's of type
+ list({type_desc, list(frequency)})
+each element of the list contains the General Frequency for a type.
+The list length can be increased if the 2nd branch if favoured over the 1st branch.
+<h4>
+From Tute6 :
+frequency defines the relative chance of a branch being selected, plus information about that
+branch's sub-branches.
+list(frequency) contains distribution information about 1 discriminated union, ie: the list
+should contain frequencies for all possible branches.
+list(list(frequency)) contains distribution information about a list of discriminated unions.
+</h4>
+A list is a discriminated union. To describe it, the correct format will be list(frequency),
+which matches the 2nd term of list({type_desc, list(frequency)})
+<P>
+<table border=1 width=100%><tr><td><pre>
+The list(frequency) for list(T) should have two elements, since the definition of list/1 has
+two branches.
+ Output = [ frequency_a, frequency_b ]
+
+ frequency_a = { 10, ...something_a... }
+ frequency_b = { 90, ...something_b... }
+That is 10% take 1st branch, 90% take the 2nd branch.
+
+The constrctor []/0 takes no argument, thus something_a is [], ie:
+frequency_a = { 10, [] }
+
+The 2nd branch constructor .(T, list(T)) takes 2 arguments. In specific frequency that would
+mean a list of two elements (or choose defalut []) :
+ something_b = list(list(frequency)) = [ A, B ]
+In General Frequency the user can specify down more than 1 level, however it is not required
+in this case. Define something_b = { 90, [] }.
+
+Put it all together:
+ list(frequency)
+ = [ frequency_a, frequency_b ]
+ = [ { 10, [] } , { 90, [] } ]
+
+Then
+ { type_desc, list(frequency) }
+ = { type_of([0.0]), [ { 10, [] } , { 90, [] } ] }
+
+Now for type list(float), there is 10% chance of selecting 1st branch, and 90% chance of selecting
+2nd branch at EVERY level.
+</pre></tr></table>
+
+The complete code (use71.m) :
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- module use71.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, float, list, std_util.
+:- import_module qcheck, nrev.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ { freq_list(F) },
+ qcheck(qcheck__f(testing4), "testing4", 1000, [], [F]).
+
+:- pred freq_list({type_desc, list(frequency)}).
+:- mode freq_list(out) is det.
+freq_list(F) :-
+ F = { type_of([0.0]), [ { 10, [] } , { 90, [] } ] }.
+
+:- func testing4(list(float)) = property.
+testing4(Xs) =
+ list_length(Xs) `>>>` (nrev(nrev(Xs)) `===` Xs).
+</pre></tr></table>
+A sample output shows the lists are much longer :
+<h4>
+Test Description : testing4
+Number of test cases that succeeded : 1000
+Number of trivial tests : 0
+Number of tests cases which failed the pre-condition : 0
+Distributions of selected argument(s) :
+1 39
+1 56
+2 40
+2 36
+2 38
+2 46
+2 61
+2 28
+2 50
+2 33
+2 53
+2 41
+3 43
+3 32
+4 34
+4 37
+4 31
+5 26
+5 30
+7 21
+7 35
+8 25
+8 29
+9 22
+9 23
+11 19
+14 24
+14 17
+15 27
+16 18
+16 20
+18 14
+19 16
+23 13
+25 15
+30 11
+32 12
+34 9
+42 10
+43 8
+49 7
+49 6
+62 4
+63 3
+69 5
+72 2
+91 1
+95 0
+</h4>
+
+Summary on default frequency, specific frequency, general frequency :
+
+1 Before Quickcheck generates a term, it considesr the term's type.
+ If it's not a discriminated union, all the frequency input is ignored
+ and lost forever.
+2 If it is a discriminated union, then Quickcheck generates the term
+ according to the specific frequency. In cases where the specific
+ frequency is [], then Quickcheck will search the general frequency
+ list to find the matching type.
+3 If no matching type is found, then generate the term (at this level) evenly
+ eg: :- type coin
+ ---> small(face)
+ ; large(color).
+ :- type face
+ ---> head
+ ; tail.
+ The chance between small/large is even, but that doesn't mean chance
+ between face:head/tail is even.
+4 If matching type is found, then Quickcheck copies that frequency information,
+ and treats that as the specific frequency.
+
+In the list(float) example:
+<h4>
+ qcheck(qcheck__f(testing4), "testing4", 1000, [], [F])
+ F = { type_of([0.0]), [ { 10, [] } , { 90, [] } ] }
+</h4>
+Quickcheck will first find [] as specific frequency (since [] is passed to qcheck),
+so it will look in the general frequency list for the information on how to generate
+list(float). That information will be extracted. The function which generates
+discriminated union will behave as if it was called with specific frequency equal to
+that of the information extracted. The information in GF is only 1 level deep, it can
+be used only once, after that the specific frequency will be [] again. So if the
+2nd branch is chosen and another list(float) is needed, then quickcheck will find []
+as specific frequency, then it will find general frequency list contains information on
+how to generate list(float). That information will be copied over...etc...
+That is:
+ 0 enter generator
+ 1 SF = [],
+ 2 search GF, found, [ { 10, [] } , { 90, [] } ]
+ 3 restart the generator with SF = [ { 10, [] } , { 90, [] } ]
+ 4 SF = [ { 10, [] } , { 90, [] } ], do not search GF
+ 5 suppose 2nd branch is chosen, ie { 90, [] }
+ the sub-branch has SF = []
+ ( If the 1st branch is chosen, then stop the looping. )
+ 6 generate the sub-branch with SF = []
+
+ 7 enter generator (for the sub-branch), SF = [], go back to step 1
+
+The actual code does not restart the generator.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Index: mercury/extras/quickcheck/tutes/T8.html
===================================================================
RCS file: T8.html
diff -N T8.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T8.html Sat Feb 24 03:23:44 2001
@@ -0,0 +1,146 @@
+<html>
+<head>
+ <TITLE> QuickCheck </TITLE>
+</head>
+Files :
+<a href="use81.m">use81.m</a><BR>
+<a href="index.html">Back to main</a>
+<H1> QuickCheck Tutorial 8 </H1>
+<h3> Generators - Random Functions</h3>
+<pre>
+
+Currently Quickcheck only has default generators for random functions that
+have 0 to 10 inputs, 1 output, and is in forward mode. This generated function
+can run on any type of inputs, but the output must be a type for which there is
+a custom/default generator.
+The output may be indepedent of zero or more of the input arguments.
+By this we mean that the value of an input argument may have no bearing upon the
+calculation of the output. There is a 5% chance per argument of this occurring.
+
+An example (use81.m)
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- module use81.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, char, std_util, list.
+:- import_module qcheck, rnd.
+
+:- type strange(T1, T2)
+ ---> wierd(T1, T2, T1).
+
+main -->
+ qcheck(qcheck__f(prop1), "prop1", 1000, [], []),
+ qcheck(qcheck__f(prop2), "prop2", 1000, [], []),
+ qcheck(qcheck__f(prop3), "prop3", 1000, [], []),
+ qcheck(qcheck__f(prop4), "prop4", 1000, [], []).
+
+:- func prop1( func(strange(int, char), int) = list(int) ) = property.
+:- mode prop1( in( func(in,in)=out is det) ) = out is det.
+prop1(FFF) =
+ FFF(wierd(1, '0', 2), 999) `===` FFF(wierd(1, '0', 2), 999).
+
+:- func prop2(func(strange(int, char), int) = list(int)) = property.
+prop2(FFF) =
+ (if FFF(wierd(1, '0', 2), 999) = FFF(wierd(1, '0', 2), 888)
+ then
+ [ info(univ("equal")) | [yes] ]
+ else
+ [ info(univ("not equal")) | [yes] ]
+ ).
+
+:- func prop3(func(int) = int) = property.
+prop3(FFF) =
+ (if FFF(1) = FFF(0)
+ then
+ [ info(univ("equal")) | [yes] ]
+ else
+ [ info(univ("not equal")) | [yes] ]
+ ).
+
+:- func prop4(func(int, int) = int) = property.
+prop4(FFF) =
+ (if FFF(101, 10) = FFF(11, 15)
+ then
+ [ info(univ("equal")) | [yes] ]
+ else
+ [ info(univ("not equal")) | [yes] ]
+ ).
+</pre></tr></table>
+
+A sample output:
+<h4>
+Test Description : prop1
+Number of test cases that succeeded : 1000
+Number of trivial tests : 0
+Number of tests cases which failed the pre-condition : 0
+Distributions of selected argument(s) :
+
+Test Description : prop2
+Number of test cases that succeeded : 1000
+Number of trivial tests : 0
+Number of tests cases which failed the pre-condition : 0
+Distributions of selected argument(s) :
+256 "equal"
+744 "not equal"
+
+Test Description : prop3
+Number of test cases that succeeded : 1000
+Number of trivial tests : 0
+Number of tests cases which failed the pre-condition : 0
+Distributions of selected argument(s) :
+60 "equal"
+940 "not equal"
+
+Test Description : prop4
+Number of test cases that succeeded : 1000
+Number of trivial tests : 0
+Number of tests cases which failed the pre-condition : 0
+Distributions of selected argument(s) :
+1 "equal"
+999 "not equal"
+</h4>
+
+prop1/1 just shows that given the same input, the output of the
+sample function is the same.
+
+prop3/1 shows that given different input, the random function will
+usually give different output (940/1000 cases). For the rest 60/1000
+cases, either the output is independent of input (most likely). Or
+it just so happens the output is the same for FFF(0) and FFF(1).
+(Noet 60/1000 is roughly 5%)
+
+prop2/1 shows 256/1000 cases shows that the random function returned the
+same output for different inputs. The real differenct between prop3/1 and
+prop2/1 is that the output of prop2/1 is list(int), which means the chance
+of generating [] is high (50% chance), and that's where 256/1000 cases come
+from.
+
+prop4/1 's random function takes two inputs, the chance of both inputs being
+independent of output is less compare to a random function which only takes
+1 input. eg FFF(in) = out, out independent of in is 5% chance
+ FFF(in, in) = out, out independent of in is 5% * 5% chance
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Index: mercury/extras/quickcheck/tutes/T9.html
===================================================================
RCS file: T9.html
diff -N T9.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T9.html Sat Feb 24 03:23:45 2001
@@ -0,0 +1,154 @@
+<html>
+<head>
+ <TITLE> QuickCheck </TITLE>
+</head>
+Files :
+<a href="use91.m">use91.m</a><BR>
+<a href="index.html">Back to main</a>
+<H1> QuickCheck Tutorial 9 </H1>
+<h3> User Defined generators</h3>
+<pre>
+
+The default generator will be called only if a user defined generator does not.
+The user definded generator must conform to the following format:
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- func gen_f(type_desc, list(frequency), list({type_desc, list(frequency)}),
+ list(user_gen_type), rnd, rnd) = univ.
+:- mode gen_f(in, in, in, list_skel_in(user_gen_inst), in, out) = out is det.
+
+:- type user_gen_type
+ ---> { type_desc,
+ func(type_desc, list(frequency),
+ list({type_desc, list(frequency)}),
+ list(user_gen_type), rnd, rnd) = univ
+ }.
+
+ % inst declaration for each user-defined generator
+:- inst user_gen_inst
+ = bound({ ground,
+ func(in, in, in,
+ list_skel_in(user_gen_inst), in, out) = out is det
+ }).
+</pre></tr></table>
+The last two arguments of type rnd, are the random supply, in & out.
+(Ignore the rest of arguments) use91.m shows a user defined generator for type :
+<h4>
+ func fff(int) = int
+ mode fff(in) = out
+
+</h4>
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+:- module use91.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, list, std_util.
+:- import_module qcheck, rnd.
+
+main -->
+ qcheck(qcheck__f(prop1), "user function", 100, [], [],
+ [{type_of(some_function), gen_f}]),
+ qcheck(qcheck__f(prop1), "no user function", 100, [], [], []).
+
+:- func gen_f(type_desc, list(frequency), list({type_desc, list(frequency)}),
+ list(user_gen_type), rnd, rnd) = univ.
+:- mode gen_f(in, in, in, list_skel_in(user_gen_inst), in, out) = out is det.
+gen_f(_, _, _, _, RS, RS) = Univ :-
+ Univ = univ(some_function).
+
+:- func some_function(int) = int.
+:- mode some_function(in) = out is det.
+some_function(X) = Y :-
+ Y = 2 * X.
+
+:- func prop1(func(int)=int) = property.
+:- mode prop1(in(func(in)=out is det)) = out is det.
+prop1(FFF) = FFF(8) `===` (8 * 2).
+
+Sample output:
+ Test Description : user function
+ Number of test cases that succeeded : 100
+ Number of trivial tests : 0
+ Number of tests cases which failed the pre-condition : 0
+ Distributions of selected argument(s) :
+
+ Test description : no user function
+ Falsifiable :
+ '<<predicate>>'
+</pre></tr></table>
+
+The user defined generator is gen_f/6, which ignores the first 4 arguments, and
+assigns rnd output equal to the input since gen_f doesn't use it.
+(all that was trivial, basiclly gen_f/6 ignores all of the inputs) And it returns
+some_function/1 in a univ.
+
+<h4>
+:- pred qcheck(T, string, int, list(list(frequency)),
+ list({type_desc, list(frequency)}),
+ list(user_gen_type), io__state, io__state) <= testable(T).
+:- mode qcheck(in, in, in, in, in, list_skel_in(user_gen_inst), di, uo) is det.
+qcheck(qcheck__f(prop1), "user function", 100, [], [],
+ [{type_of(some_function), gen_f}]),
+</h4>
+qcheck/8 is used in use91.m. The last argument takes in the user-defined
+generators. The format is list(user_gen_type), since there is only 1 user
+defined generator, the list contains 1 element : {type_of(some_function), gen_f}.
+ type_of(some_function) : describes what type gen_f generates
+ gen_f : is the actual generator
+
+the invariant function is true only if FFF(8) `===` (8 * 2). The 2nd test shows a random
+function will 'never' do that, but the 1st test with user defined generator will always
+generate the functions Y = 2 * X
+<h4>
+:- func gen_f(type_desc, list(frequency), list({type_desc, list(frequency)}),
+ list(user_gen_type), rnd, rnd) = univ.
+:- mode gen_f(in, in, in, list_skel_in(user_gen_inst), in, out) = out is det.
+</h4>
+
+1st input of type type_desc is the type_of of the current term the generator
+ is required to generate. It could be useful if the
+ generator is able to generate more than one type,
+ thus the type_desc can be used to determine wihch
+ one.
+
+2st input of type list(frequency) is the specific frequency for this term, meaningless
+ if the term is not a discriminated union. The user
+ can choose to ignore the setting even if the term is
+ a discriminated union.
+
+3rd input of type list({type_desc, list(frequency)}) is a list of general frequency
+
+4th input of type list(user_gen_type) is a list of user defined generators
+
+5th input of type rnd random number supply
+
+6th input of type rnd random number return, let return = supply if not used.
+
+Look at rand_union/6 to find out how to write code which extracts/analyses specific frequency
+and eneral frequency.
+Look at gen/7 to find out how to wrote code which extract/analysis user defined generators.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Index: mercury/extras/quickcheck/tutes/index.html
===================================================================
RCS file: index.html
diff -N index.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ index.html Sat Feb 24 03:23:45 2001
@@ -0,0 +1,26 @@
+<html>
+<head>
+ <TITLE> QuickCheck </TITLE>
+</head>
+
+<H1> Quickcheck for Mercury</H1>
+
+<H3> HTML Version </H3>
+
+<ul>
+<li> <a href="T1.html"><pre>Tutorial 1 Intro & `===`</pre></a>
+<li> <a href="T2.html"><pre>Tutorial 2 Conditional laws & `===>``</pre></a>
+<li> <a href="T3.html"><pre>Tutorial 3 Monitoring Data, to_trivial/3, `>>>`</pre></a>
+<li> <a href="T4.html"><pre>Tutorial 4 Summary - Invariant Function & Property </pre></a>
+<li> <a href="T5.html"><pre>Tutorial 5 Generators basic</pre></a>
+<li> <a href="T6.html"><pre>Tutorial 6 Discriminated union & Specific Frequency</pre></a>
+<li> <a href="T7.html"><pre>Tutorial 7 General Frequency</pre></a>
+<li> <a href="T8.html"><pre>Tutorial 8 Random Functions</pre></a>
+<li> <a href="T9.html"><pre>Tutorial 9 User Defined Generators</pre></a>
+<li> <a href="T10.html"><pre>Tutorial 10 Summary - Generators</pre></a>
+</ul>
+
+Feedback? Mail <a href="mailto:xcsm at students.cs.mu.oz.au">Simon</a>.
+
+</BODY>
+</html>
Index: mercury/extras/quickcheck/tutes/mymax.m
===================================================================
RCS file: mymax.m
diff -N mymax.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ mymax.m Sat Feb 24 03:23:45 2001
@@ -0,0 +1,18 @@
+:- module mymax.
+
+:- interface.
+:- import_module int.
+
+:- func mymax(int, int) = int.
+:- mode mymax(in, in) = out is det.
+
+:- implementation.
+
+mymax(X, Y) = Z :-
+ (if Y >= X
+ then
+ Z = Y
+ else
+ Z = X
+ ).
+
Index: mercury/extras/quickcheck/tutes/nrev.m
===================================================================
RCS file: nrev.m
diff -N nrev.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ nrev.m Sat Feb 24 03:23:45 2001
@@ -0,0 +1,13 @@
+:- module nrev.
+
+:- interface.
+:- import_module list.
+
+:- func nrev(list(T)) = list(T).
+:- mode nrev(in) = out is det.
+
+:- implementation.
+
+nrev([]) = [].
+nrev([X|Xs]) = Ys :-
+ list__append(nrev(Xs), [X], Ys).
Index: mercury/extras/quickcheck/tutes/nrev2.m
===================================================================
RCS file: nrev2.m
diff -N nrev2.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ nrev2.m Sat Feb 24 03:23:45 2001
@@ -0,0 +1,14 @@
+:- module nrev2.
+
+:- interface.
+:- import_module list.
+
+:- pred nrev2(list(T), list(T)).
+:- mode nrev2(in, out) is det.
+
+:- implementation.
+
+nrev2([], []).
+nrev2([X|Xs], Ys):-
+ nrev2(Xs, Reversed),
+ list__append(Reversed, [X], Ys).
Index: mercury/extras/quickcheck/tutes/use.m
===================================================================
RCS file: use.m
diff -N use.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use.m Sat Feb 24 03:23:45 2001
@@ -0,0 +1,30 @@
+:- module use.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, list.
+:- import_module qcheck, nrev.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(testing), "sample testing").
+
+%------------------------------------------------------------------------------%
+% Invariant test functions
+%------------------------------------------------------------------------------%
+
+:- func testing(list(int), list(int)) = property.
+testing(Xs, Ys) =
+ nrev(Xs ++ Ys) `===` (nrev(Ys) ++ nrev(Xs)).
+
+
Index: mercury/extras/quickcheck/tutes/use1.m
===================================================================
RCS file: use1.m
diff -N use1.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use1.m Sat Feb 24 03:23:45 2001
@@ -0,0 +1,34 @@
+:- module use1.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, list.
+:- import_module qcheck, nrev2.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(testing2), "testing2").
+
+%------------------------------------------------------------------------------%
+% Invariant test functions
+%------------------------------------------------------------------------------%
+
+
+:- func testing2(list(int), list(int)) = property.
+testing2(Xs, Ys) = (Left `===` Right) :-
+ nrev2((Xs ++ Ys), Left),
+ nrev2(Ys, Part_a),
+ nrev2(Xs, Part_b),
+ Right = Part_a ++ Part_b.
+
+
Index: mercury/extras/quickcheck/tutes/use11.m
===================================================================
RCS file: use11.m
diff -N use11.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use11.m Sat Feb 24 03:23:45 2001
@@ -0,0 +1,24 @@
+:- module use11.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, list.
+:- import_module qcheck, nrev.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(func(Xs `with_type` list(int), Ys `with_type` list(int))
+ = nrev(Xs ++ Ys) `===` (nrev(Ys) ++ nrev(Xs))),
+ "sample testing").
+
+
Index: mercury/extras/quickcheck/tutes/use20.m
===================================================================
RCS file: use20.m
diff -N use20.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use20.m Sat Feb 24 03:23:45 2001
@@ -0,0 +1,39 @@
+:- module use20.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, list, bool.
+:- import_module qcheck, mymax.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(law), "testing mymax using `===>` for bool"),
+ qcheck(qcheck__f(law2), "testing mymax using `===>` for (pred)").
+
+:- func law(int, int) = property.
+law(X, Y) = (X =< Y) `===>` (mymax(X, Y) `===` Y).
+
+:- func law2(int, int) = property.
+law2(X, Y) = is_less_equal(X, Y) `===>`
+ (mymax(X, Y) `===` Y).
+
+:- func is_less_equal(int, int) = bool.
+is_less_equal(X, Y) = Bool :-
+ (if X =< Y
+ then
+ Bool = yes
+ else
+ Bool = no
+ ).
+
+
Index: mercury/extras/quickcheck/tutes/use21.m
===================================================================
RCS file: use21.m
diff -N use21.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use21.m Sat Feb 24 03:23:45 2001
@@ -0,0 +1,29 @@
+:- module use21.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, list, bool.
+:- import_module qcheck, mymax.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(law), "2 conditions : x<=Y, Y!=0").
+
+:- func law(int, int) = property.
+law(X, Y) = notzero(Y) `===>` ((X =< Y) `===>` (mymax(X, Y) `===` Y)).
+
+:- pred notzero(int).
+:- mode notzero(in) is semidet.
+notzero(X) :- X \= 0.
+
+
Index: mercury/extras/quickcheck/tutes/use22.m
===================================================================
RCS file: use22.m
diff -N use22.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use22.m Sat Feb 24 03:23:45 2001
@@ -0,0 +1,33 @@
+:- module use22.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, bool.
+:- import_module qcheck.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(law1), "passing property"),
+ qcheck(qcheck__f(law2), "passing (func) = property").
+
+:- func law1(int, int) = property.
+law1(X, Y) = notzero(Y) `===>` qcheck__f( (func) = ((X // Y) `===` (X // Y)) ).
+
+:- func law2(int, int) = property.
+law2(X, Y) = notzero(Y) `===>` ( (X // Y) `===` (X // Y) ).
+
+:- pred notzero(int).
+:- mode notzero(in) is semidet.
+notzero(X) :- X \= 0.
+
+
Index: mercury/extras/quickcheck/tutes/use31.m
===================================================================
RCS file: use31.m
diff -N use31.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use31.m Sat Feb 24 03:23:45 2001
@@ -0,0 +1,42 @@
+:- module use31.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, list, bool.
+:- import_module qcheck, nrev.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(testing1), "testing1"),
+ qcheck(qcheck__f(testing2), "testing2"),
+ qcheck(qcheck__f(testing3), "testing3"),
+ qcheck(qcheck__f(testing4), "testing4").
+
+:- func testing1(list(float)) = property.
+testing1(Xs) =
+ nrev(nrev(Xs)) `===` Xs.
+
+:- func testing2(list(float)) = property.
+testing2(Xs) =
+ to_trivial([], Xs, nrev(nrev(Xs)) `===` Xs).
+
+:- func testing3(list(float)) = property.
+testing3(Xs) =
+ to_trivial(1,
+ list_length(Xs),
+ to_trivial([], Xs, nrev(nrev(Xs)) `===` Xs)
+ ).
+
+:- func testing4(list(float)) = property.
+testing4(Xs) =
+ list_length(Xs) `>>>` (nrev(nrev(Xs)) `===` Xs).
Index: mercury/extras/quickcheck/tutes/use33.m
===================================================================
RCS file: use33.m
diff -N use33.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use33.m Sat Feb 24 03:23:45 2001
@@ -0,0 +1,43 @@
+:- module use33.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, list, bool.
+:- import_module qcheck, nrev.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(testing5), "testing5").
+
+:- func testing5(list(float)) = property.
+testing5(Xs) =
+ odd_even(Xs) `>>>`
+ (list_length(Xs) `>>>` (nrev(nrev(Xs)) `===` Xs)).
+
+:- func odd_even(list(T)) = string.
+:- mode odd_even(in) = out is det.
+odd_even(Xs) = Y :-
+ (if list_length(Xs) mod 2 = 1
+ then
+ Y = "odd"
+ else
+ Y = "even"
+ ).
+
+
+
+
+
+
+
+
Index: mercury/extras/quickcheck/tutes/use51.m
===================================================================
RCS file: use51.m
diff -N use51.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use51.m Sat Feb 24 03:23:45 2001
@@ -0,0 +1,30 @@
+:- module use51.
+
+:- interface.
+
+:- type marks == int.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, char, float, string, list.
+:- import_module qcheck.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(junk), "just to show the inputs", 5, [], []).
+
+:- func junk(marks, char, float, string) = property.
+junk(A, B, C, D) =
+ {A,B,C,D} `>>>` [yes].
+
+
+
+
Index: mercury/extras/quickcheck/tutes/use62.m
===================================================================
RCS file: use62.m
diff -N use62.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use62.m Sat Feb 24 03:23:45 2001
@@ -0,0 +1,100 @@
+:- module use62.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, list, string.
+:- import_module qcheck, rnd.
+
+%---------------------------------------------------------------------------%
+% arbitrary user-defined types for testing purposes
+%---------------------------------------------------------------------------%
+
+:- type bullet
+ ---> good(color)
+ ; inaccurate(color)
+ ; defective(color).
+
+:- type color
+ ---> black
+ ; white.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ { freq_B(B) },
+ { freq_W(W) },
+ qcheck(qcheck__f(prop2), "bullet fight", 10000, [[],B,W], []).
+
+:- pred freq_B(list(frequency)).
+:- mode freq_B(out) is det.
+freq_B(Out) :-
+ Out = [ {50, [ [ {100, []}, {0, []} ] ] },
+ {10, [ [ {100, []}, {0, []} ] ] },
+ {40, [ [ {100, []}, {0, []} ] ] }
+ ].
+
+:- pred freq_W(list(frequency)).
+:- mode freq_W(out) is det.
+freq_W(Out) :-
+ Out = [ {40, [ [ {0, []}, {100, []} ] ] },
+ {30, [ [ {0, []}, {100, []} ] ] },
+ {30, [ [ {0, []}, {100, []} ] ] }
+ ].
+
+:- func prop2(int, bullet, bullet) = property.
+prop2(Seed, B, W) = fight(Seed, B, W) `>>>`
+ ({"ComB",B} `>>>`
+ ({"ComW", W} `>>>` [yes])
+ ).
+
+:- func fight(int, bullet, bullet) = string.
+:- mode fight(in, in, in) = out is det.
+fight(Seed, B, W) = String :-
+ rnd__init(Seed, RS0),
+ B_hit = is_hit(B, RS0, RS1),
+ W_hit = is_hit(W, RS1, _),
+ (if B_hit = W_hit
+ then
+ String = "draw"
+ else if B_hit > W_hit
+ then
+ String = "B win"
+ else
+ String = "W win"
+ ).
+
+:- func is_hit(bullet, rnd, rnd) = int.
+:- mode is_hit(in, in, out) = out is det.
+is_hit(Bullet, RS0, RS) = Int :-
+ Temp = rand_allint(RS0, RS) rem 2,
+ (
+ Bullet = good(_),
+ Int = 1
+ ;
+ Bullet = inaccurate(_),
+ (if Temp = 0
+ then
+ Int = 1
+ else
+ Int = 0
+ )
+ ;
+ Bullet = defective(_),
+ Int = 0
+ ).
+
+
+
+
+
+
+
Index: mercury/extras/quickcheck/tutes/use71.m
===================================================================
RCS file: use71.m
diff -N use71.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use71.m Sat Feb 24 03:23:45 2001
@@ -0,0 +1,30 @@
+:- module use71.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, float, list, std_util.
+:- import_module qcheck, nrev.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ { freq_list(F) },
+ qcheck(qcheck__f(testing4), "testing4", 1000, [], [F]).
+
+:- pred freq_list({type_desc, list(frequency)}).
+:- mode freq_list(out) is det.
+freq_list(F) :-
+ F = { type_of([0.0]), [ { 10, [] } , { 90, [] } ] }.
+
+:- func testing4(list(float)) = property.
+testing4(Xs) =
+ list_length(Xs) `>>>` (nrev(nrev(Xs)) `===` Xs).
Index: mercury/extras/quickcheck/tutes/use81.m
===================================================================
RCS file: use81.m
diff -N use81.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use81.m Sat Feb 24 03:23:45 2001
@@ -0,0 +1,63 @@
+:- module use81.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, char, std_util, list.
+:- import_module qcheck, rnd.
+
+:- type strange(T1, T2)
+ ---> wierd(T1, T2, T1).
+
+main -->
+ qcheck(qcheck__f(prop1), "prop1", 1000, [], []),
+ qcheck(qcheck__f(prop2), "prop2", 1000, [], []),
+ qcheck(qcheck__f(prop3), "prop3", 1000, [], []),
+ qcheck(qcheck__f(prop4), "prop4", 1000, [], []).
+
+:- func prop1(func(strange(int, char), int) = list(int)) = property.
+:- mode prop1(in(func(in,in)=out is det)) = out is det.
+prop1(FFF) =
+ FFF(wierd(1, '0', 2), 999) `===` FFF(wierd(1, '0', 2), 999).
+
+:- func prop2(func(strange(int, char), int) = list(int)) = property.
+:- mode prop2(in(func(in,in)=out is det)) = out is det.
+prop2(FFF) =
+ (if FFF(wierd(1, '0', 2), 999) = FFF(wierd(1, '0', 2), 888)
+ then
+ [ info(univ("equal")) | [yes] ]
+ else
+ [ info(univ("not equal")) | [yes] ]
+ ).
+
+:- func prop3(func(int) = int) = property.
+:- mode prop3(in(func(in)=out is det)) = out is det.
+prop3(FFF) =
+ (if FFF(1) = FFF(0)
+ then
+ [ info(univ("equal")) | [yes] ]
+ else
+ [ info(univ("not equal")) | [yes] ]
+ ).
+
+:- func prop4(func(int, int) = int) = property.
+:- mode prop4(in(func(in, in)=out is det)) = out is det.
+prop4(FFF) =
+ (if FFF(101, 10) = FFF(11, 15)
+ then
+ [ info(univ("equal")) | [yes] ]
+ else
+ [ info(univ("not equal")) | [yes] ]
+ ).
+
+
+
+
Index: mercury/extras/quickcheck/tutes/use91.m
===================================================================
RCS file: use91.m
diff -N use91.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use91.m Sat Feb 24 03:23:45 2001
@@ -0,0 +1,40 @@
+:- module use91.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, list, std_util.
+:- import_module qcheck, rnd.
+
+main -->
+ qcheck(qcheck__f(prop1), "user function", 100, [], [],
+ [{type_of(some_function), gen_f}]),
+ qcheck(qcheck__f(prop1), "no user function", 100, [], [], []).
+
+:- func gen_f(type_desc, list(frequency), list({type_desc, list(frequency)}),
+ list(user_gen_type), rnd, rnd) = univ.
+:- mode gen_f(in, in, in, list_skel_in(user_gen_inst), in, out) = out is det.
+gen_f(_, _, _, _, RS, RS) = Univ :-
+ Univ = univ(some_function).
+
+:- func some_function(int) = int.
+:- mode some_function(in) = out is det.
+some_function(X) = Y :-
+ Y = 2 * X.
+
+:- func prop1(func(int)=int) = property.
+:- mode prop1(in(func(in)=out is det)) = out is det.
+prop1(FFF) = FFF(8) `===` (8 * 2).
+
+
+
+
+
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to: mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions: mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------
More information about the developers
mailing list