[m-dev.] for review: quickcheck user guide
Xiao Chun Simon MEI
xcsm at students.cs.mu.oz.au
Mon Feb 5 16:46:26 AEDT 2001
Estimated hours taken: 40
A collection of wed pages written as a user guide for quickcheck.
It covers the syntax and features supported by current version of quickcheck.
Below are the source code of those web pages. It's probably best viewed by
a web browser at www.cs.mu.oz.au/~xcsm
quickcheck/tutes/T1.html:
New file, covers the 1st topic
quickcheck/tutes/T2.html:
New file, covers the 2nd topic
quickcheck/tutes/T3.html:
New file, covers the 3rd topic
quickcheck/tutes/T4.html:
New file, covers the 4th topic
quickcheck/tutes/T5.html:
New file, covers the 5th topic
quickcheck/tutes/T6.html:
New file, covers the 6th topic
quickcheck/tutes/T7.html:
New file, covers the 7th topic
quickcheck/tutes/T8.html:
New file, covers the 8th topic
quickcheck/tutes/T9.html:
New file, covers the 9th topic
quickcheck/tutes/index.html:
New file, index page
quickcheck/tutes/mymax.m:
New file, contain sample function mymax
quickcheck/tutes/numbers.html:
New file, sub-page for T6.html
quickcheck/tutes/testrev.m:
New file, contains sample function testrev
quickcheck/tutes/testrev2.m:
New file, contains sample predicate testrev2
quickcheck/tutes/use.m:
New file, contains example for T1.html
quickcheck/tutes/use1.m:
New file, contains example for T1.html
quickcheck/tutes/use11.m:
New file, contains example for T1.html
quickcheck/tutes/use2.m:
New file, contains example for T2.html
quickcheck/tutes/use20.m:
New file, contains example for T2.html
quickcheck/tutes/use21.m:
New file, contains example for T3.html
quickcheck/tutes/use31.m:
New file, contains example for T3.html
quickcheck/tutes/use33.m:
New file, contains example for T4.html
quickcheck/tutes/use51.m:
New file, contains example for T5.html
quickcheck/tutes/use62.m:
New file, contains example for T6.html
quickcheck/tutes/use71.m:
New file, contains example for T7.html
quickcheck/tutes/use81.m:
New file, contains example for T8.html
quickcheck/tutes/use91.m:
New file, contains example for T9.html
Index: quickcheck/tutes/T1.html
===================================================================
RCS file: T1.html
diff -N T1.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T1.html Mon Feb 5 16:01:52 2001
@@ -0,0 +1,224 @@
+<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="testrev.m">testrev.m</a>
+<a href="testrev2.m">testrev2.m</a><BR>
+<a href="index.html">Back to main</a>
+
+<H1> QuickCheck Tutorial 1 </H1>
+
+
+<pre>
+In order to test the validity of a predicate/function via quickcheck,
+the user needs 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 "testrev.m", which contains testrev/1 :
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+ :- func testrev(list(T)) = list(T).
+ :- mode testrev(in) = out is det.
+ testrev([]) = [].
+ testrev([X|Xs]) = Ys :-
+ list__append(testrev(Xs), [X], Ys).
+</pre></tr></table>
+testrev/1 is the Mercury equivalent of Haskell's reverse function. We
+want to test whether testrev/1 is properly implemented.
+
+Let YYY.m be "use.m". It must contain a main/2, and an
+invariant function. If testrev/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 testrev(), define the invariant
+function as :
+<H4>
+ testing(Xs, Ys) =
+ testrev(Xs ++ Ys) `===` (testrev(Ys) ++ testrev(Xs)).
+</H4>
+`===` function returns 'property:[yes]' if the left side equals
+right side, 'property:[no]' otherwise. ( like == in Haskell, but not of
+type bool) In theory testrev/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() 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, testrev.
+
+%-------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(testing), "sample testing").
+
+%-------------------------------------------------------------------%
+% Invariant test functions
+%-------------------------------------------------------------------%
+
+:- func testing(list(int), list(int)) = property.
+testing(Xs, Ys) =
+ testrev(Xs ++ Ys) `===` (testrev(Ys) ++ testrev(Xs)).
+</pre></tr></table>
+To compiler 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>
+testrev/1 passed 100 tests and failed none.(ignore the last 3 lines
+for now)
+
+If the invariant function is wrongly specified, or testrev/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 cleaner
+(as in Haskell) than one which contains predicates. Suppose that "testrev2.m"
+defines a predicate version of reversing list:
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+ :- pred testrev2(list(T), list(T)).
+ :- mode testrev2(in, out) is det.
+ testrev2([], []).
+ testrev2([X|Xs], Ys):-
+ testrev2(Xs, Reversed),
+ list__append(Reversed, [X], Ys).
+</pre></tr></table>
+Then the invariant function looks like :
+<h4>
+ testing2(Xs, Ys) = (Left `===` Right) :-
+ testrev2((Xs ++ Ys), Left),
+ testrev2(Ys, Part_a),
+ testrev2(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, testrev2.
+
+%-------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(testing2), "testing2").
+
+%-------------------------------------------------------------------%
+% Invariant test functions
+%-------------------------------------------------------------------%
+
+:- func testing2(list(int), list(int)) = property.
+testing2(Xs, Ys) = (Left `===` Right) :-
+ testrev2((Xs ++ Ys), Left),
+ testrev2(Ys, Part_a),
+ testrev2(Xs, Part_b),
+ Right = Part_a ++ Part_b.
+</pre></tr></table>
+An alternative to write use.m which does not evolving writing a separate
+invariant function, (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, testrev.
+
+%--------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(func(Xs `with_type` list(int), Ys `with_type` list(int))
+ = testrev(Xs ++ Ys) `===` (testrev(Ys) ++ testrev(Xs))),
+ "sample testing").
+</pre></tr></table>
+Summary
+
+In YYY.m, the main should be defined as :
+<h4>
+ Main --->
+ qcheck(qcheck_f(XXXXXXXX), YYYYYYYY).
+</h4>
+Where XXXXXXXX is the (name of) invariant function and
+YYYYYYYY is a string which describe/name/comment XXXXXXXX.
+
+The invariant function is of the form
+<h4>
+ :- mode XXXXXXXX(in, in, in ...) = out.
+</h4>
+The inputs can be of any type. The output is of type 'property:[yes]' or 'peoperty:[no]'
+What ever happens inside XXXXXXXX, quickcheck does not care. If output is [yes], the
+invariant function is assumed to pass the test case satisfactory.
+
+
+</html>
Index: quickcheck/tutes/T2.html
===================================================================
RCS file: T2.html
diff -N T2.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T2.html Mon Feb 5 16:01:53 2001
@@ -0,0 +1,133 @@
+<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="mymax.m">mymax.m</a><BR>
+<a href="index.html">Back to main</a>
+<h3> Conditional law </h3>
+
+<pre>
+Conditional law
+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 only 48/100
+passed the invariant function, and none failed. However, 52/100 cases where
+the inputs failed the prec-condition.
+Note that both test cases succeeded 52/100 and failed pre-condition 48/100.
+This is not a coincident; 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>
+
+Summary:
+<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>
+All invariant functions must return a property, which is just a list of flags.
+If the list contains one or more 'condition', the test result is ignored.
+The implication combinator '===>' will add 'condition' into the property if
+its left argument is '(pred):fail' or 'bool:no'.
+</html>
\ No newline at end of file
Index: quickcheck/tutes/T3.html
===================================================================
RCS file: T3.html
diff -N T3.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T3.html Mon Feb 5 16:01:53 2001
@@ -0,0 +1,292 @@
+<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="testrev.m">testrev.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(), 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) =
+ testrev (testrev Xs) `===` Xs.
+</h4>
+add to_trivial([], Xs, XXXXXX) where XXXXXX is the ordinary output. If the 1st
+argument is equal to the 2nd argument, then that test case is labeled trivial,
+in this case, an empty list.
+<h4>
+ :- func testing2(list(float)) = property.
+ testing2(Xs) =
+ to_trivial([], Xs, testrev (testrev 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, testrev(testrev(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, testrev.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(testing1), "testing1"),
+ qcheck(qcheck__f(testing2), "testing2"),
+ qcheck(qcheck__f(testing3), "testing3").
+
+:- func testing1(list(float)) = property.
+testing1(Xs) =
+ testrev(testrev(Xs)) `===` Xs.
+
+:- func testing2(list(float)) = property.
+testing2(Xs) =
+ to_trivial([], Xs, testrev(testrev(Xs)) `===` Xs).
+
+:- func testing3(list(float)) = property.
+testing3(Xs) =
+ to_trivial(1,
+ list_length(Xs),
+ to_trivial([], Xs, testrev(testrev(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 empty lists or
+lists of only one element. It had only tested 25/100 cases where the list is
+longer than 1 element.
+
+
+<h3> Monitoring Test Data - `>>>` </h3>
+The combinator `>>>` will gather 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 generate for the previous tests :
+<h4>
+ :- func testing4(list(float)) = property.
+ testing4(Xs) =
+ list_length(Xs) `>>>` (testrev(testrev(Xs)) `===` Xs).
+</h4>
+The combinator `>>>` will convert it's left argument to a univ, and push info(univ)
+into it's right argument(which is a property == a list of flags).
+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, testrev.
+
+%---------------------------------------------------------------------------%
+
+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) =
+ testrev(testrev(Xs)) `===` Xs.
+
+:- func testing2(list(float)) = property.
+testing2(Xs) =
+ to_trivial([], Xs, testrev(testrev(Xs)) `===` Xs).
+
+:- func testing3(list(float)) = property.
+testing3(Xs) =
+ to_trivial(1,
+ list_length(Xs),
+ to_trivial([], Xs, testrev(testrev(Xs)) `===` Xs)
+ ).
+
+:- func testing4(list(float)) = property.
+testing4(Xs) =
+ list_length(Xs) `>>>` (testrev(testrev(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 lenggh == 0
+ 18 cases of length == 1
+ 16 cases of length == 2
+ ...etc...
+53+18 cases = 71 cases, which was marked trivial in testing3, likewise
+for testing2. The number will add up only if all the tests were ran within
+the same second.
+
+
+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, testrev.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(testing5), "testing5").
+
+:- func testing5(list(float)) = property.
+testing5(Xs) =
+ odd_even(Xs) `>>>`
+ (list_length(Xs) `>>>` (testrev(testrev(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>
+The display of testing5 shows that 61 cases of "even"
+ 47 cases of length == 0
+ 39 cases of "odd"
+ ...etc...
+Currently the display is sorted by the number of occurences, without any regards to
+the type.
+<h4>
+1 7
+1 5
+2 4
+2 6
+8 3
+1 B
+1 A
+2 C
+10 Z
+</h4>
+May implement to above display later....
+
+
+
+
+
+
Index: quickcheck/tutes/T4.html
===================================================================
RCS file: T4.html
diff -N T4.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T4.html Mon Feb 5 16:01:53 2001
@@ -0,0 +1,74 @@
+<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 XXXXXXXX(T, T1, T2 ...) = property
+ :- mode XXXXXXXX(in, in, in ...) = out.
+The inputs can be of most types (details next tutorial), however only arity
+0 to 4 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 XXXXXXXX, 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/crash. However not all forms of property is sensible.
+One could return [], or [yes, no, yes, no]. Quickcheck analyzes property in
+the following order:
+ 1 is condition (1 or more) in the list(flag) ?
+ if yes, increment PRE-CONDITION counter and stop analyze
+ if no, goto 2
+ 2 is trivial (1 or more) in the list ?
+ if yes, increment TRIVIAL counter, goto 3
+ if no, goto 3
+ 3 gets all the info(univ) (if any) in the list, merge that with
+ the master list for distribution, goto 4
+ 4 is no (1 or more) in the list ?
+ if no, increment YES counter and stop
+ if yes, increment NO counter and stop, other function will pick
+ up that the No counter has been increased, and stops the whole
+ qcheck.
+So, [] will increase the YES counter, and [yes, no, yes, no] will increase the
+NO 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
+
+:- func to_trivial(T, T, property) = property.
+:- mode to_trivial(in, in, in) = out is det.
+to_trivial(A, B, C) = D 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: quickcheck/tutes/T5.html
===================================================================
RCS file: T5.html
diff -N T5.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T5.html Mon Feb 5 16:01:53 2001
@@ -0,0 +1,184 @@
+<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 XXXXXXXX(T, T1, T2 ...) = property
+ :- mode XXXXXXXX(in, in, in ...) = out.
+Quickcheck generates random value for each input argument at run time.
+Currently quickcheck have default generators for the following types :
+ 0 equivalent type
+ 1 int
+ 2 char
+ 3 float
+ 4 string
+ 5 discriminated union
+ 6 some functions
+plus type 7 which is any thing the user has written a generator for.
+
+Acutally 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. So any equivalent type with real type that fits into
+types 0-7 will work.
+
+Default for int is rand_int/2, which has distribution (roughly):
+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 even distribution
+over all possible value for a float in a 32bits machine.
+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 average string length is Sum(0.1* 0.9^N * N) where N <- {0, infinity}
+<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>
+A sample qcheck which use types 0-4 (use51.m):
+<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>
+Few thing to note in use51.m :
+<h4>
+ qcheck(qcheck__f(junk), "just to show the inputs", 5, [], []).
+</h4>
+qcheck/7 takes more parameters than qcheck/4. The 3rd argument is an int,
+which specify how many times to run, 5 in use51.m (default is 100). Ignore
+other auguments.
+<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
+
+
+Possible improvement of rand_float/2 & rand_int/2 which will give higher chance
+of generating 0, or small numbers.
+
+
+
+
+
+
+
Index: quickcheck/tutes/T6.html
===================================================================
RCS file: T6.html
diff -N T6.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T6.html Mon Feb 5 16:01:53 2001
@@ -0,0 +1,330 @@
+<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 which are composed
+of any thing that fits into types 0-7. In default frequency mode, all branches
+at each level has 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 the a term's default frequency (which is evenly spread)
+to one the user have provided. An example :
+Suppose there are two bullet manufacturer.
+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, plus information of that
+branch's sub-branches.
+list(frequency) contains distribution information about 1 discrimated union, ie: the list
+should contain frequencies for all possible branches.
+list(list(frequency)) contains distribution information about a list of discrimated unions.
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+Let's try to describe Company_W's bullet, Bullet is discrimated union, so the right format is :
+ 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...}
+
+<a href="numbers.html">Click here to see what the numbers mean</a>
+
+...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/4 then the list would be length 4. OR [] when you get sick of
+specifying frequency and just want to use the default)
+
+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 1st element [] of type list(frequency) is for type int, which doesn't make
+sense, since type int is not a discriminated union. That [] will be ignore when
+generating int, but it's presence is required.
+
+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"
+
+I was hoping to run 100000 or more tests to find which bullet is better. However the
+stack overflowed at 100000 tests. The sample output is for only 10000 tests. At 10000
+tests, both bullets performs relatively the same.
+(Will look into this, make more effecient code)
+(or default compiler no garbage collection)
+
+The key advantage of Specific Frequency over General Frequency is that it allows
+different frequency for the same type, where SF don't allow.
+The draw back is that the frequency only goes as deep (down the branches) as the user
+defines it, and amount of work blows up as levels of branches increases.
+
+Walk through in generating a Company_B 's bullet :
+
+ 1 Enter generator with
+ SF = [ {50, [ [ {100, []}, {0, []} ] ] },
+ {10, [ [ {100, []}, {0, []} ] ] },
+ {40, [ [ {100, []}, {0, []} ] ] }
+ ].
+
+ 2 suppose 3rd branch is selected (40% chance of happening)
+ the 3rd branch has only 1 term, extract [ {100, []}, {0, []} ]
+ from {40, [ [ {100, []}, {0, []} ] ] }
+
+ 3 call generator that term with SF = [ {100, []}, {0, []} ]
+
+ 4 Enter generator for the sub-branch (fot color) with
+ SF = [ {100, []}, {0, []} ]
+
+ 5 suppose 1st branch is selected, extract [] from {100, []}
+
+ 6 since constructor black/0 has no argument, the generator stops
+ the recursive call.
+
+
+
+
Index: quickcheck/tutes/T7.html
===================================================================
RCS file: T7.html
diff -N T7.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T7.html Mon Feb 5 16:01:53 2001
@@ -0,0 +1,267 @@
+<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 2, an invariant function was written to test the law
+<P>
+<table border=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+ reverse (reverse xs) = xs
+
+:- func testing4(list(float)) = property.
+testing4(Xs) =
+ list_length(Xs) `>>>` (testrev(testrev(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
+
+The display of testing4 shows that 53 cases of lenggh == 0
+ 18 cases of length == 1
+ 16 cases of length == 2
+ ...etc...
+</pre></tr></table>
+The length of of the list is heavily biased towards the short end. In the limit with
+even distribution along the branchse, 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, this is due to the fact that
+<h4>
+ :- type list(T) ---> [] ; [T | list(T)].
+</h4>
+Transform the type definition to something more readable as a disciminated union:
+<h4>
+ :- type list(T) ---> [] ; .(T, list(T)).
+</h4>
+
+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 of that
+branch's sub-branches.
+list(frequency) contains distribution information about 1 discrimated union, ie: the list
+should contain frequencies for all possible branches.
+list(list(frequency)) contains distribution information about a list of discrimated 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=0 width=100% bgcolor=#eeeee0><tr><td><pre>
+list(frequency) for list(T), list has two branches, so list of 2 element
+ 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 seleting 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, testrev.
+
+%---------------------------------------------------------------------------%
+
+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) `>>>` (testrev(testrev(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 generate a term, it checks which types the term is
+ suppose to be. 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 generate the term
+ according to the specifici frequency. In cases where the specific
+ frequency is [], then Quickcheck will search the general frequency
+ list to find the matching type. (between type_of(term) and what's in
+ the list)
+3 If no matching type 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 treat 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>
+Quickquick will first find [] as specific frequency (since [] is passed to qcheck),
+then it will find general frequency list contains information on how to generate
+list(float). That information will be extracted. The function whish 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 use only once, after that the specific frequency will be [] again. So if the
+2nd branch is choosen 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 = []
+ 6 generate the subbranch with SF = []
+
+ 7a enter generator (for the sub-branch)
+ 7b SF = [],
+ 7c search GF, found, [ { 10, [] } , { 90, [] } ]
+ 7d restart the generator with SF = [ { 10, [] } , { 90, [] } ]
+ 7e SF = [ { 10, [] } , { 90, [] } ], do not search GF
+ 7f suppose 2nd branch is chosen, ie { 90, [] }
+ the sub-branch has SF = []
+ 7g generate the subbranch with SF = []
+ ....
+
+The actual code does not restart the generator.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Index: quickcheck/tutes/T8.html
===================================================================
RCS file: T8.html
diff -N T8.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T8.html Mon Feb 5 16:01:53 2001
@@ -0,0 +1,145 @@
+<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>
+
+Random function is generated using curry, currently only generate functions that
+have 1 ~ 3 inputs, and 1 output. The generated function can run on any type of
+inputs, but the output must be of type0-7 from tute 5.
+Also each input argument has 5% chance of being independent of the output.
+(currently the invariant function can only have forward mode functions as its
+input arguments)
+
+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 of the
+sample function is the same.
+
+prop3/1 shows that give 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: quickcheck/tutes/T9.html
===================================================================
RCS file: T9.html
diff -N T9.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ T9.html Mon Feb 5 16:01:53 2001
@@ -0,0 +1,167 @@
+<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>
+
+From Tute 6:
+The invariant function is of the form
+ :- func XXXXXXXX(T, T1, T2 ...) = property
+ :- mode XXXXXXXX(in, in, in ...) = out.
+Quickcheck generates random value for each input argument at run time.
+Currently quickcheck have default generators for the following types :
+ 0 equivalent type
+ 1 int
+ 2 char
+ 3 float
+ 4 string
+ 5 discriminated union
+ 6 some functions
+also type 7 which is any thing the user has written a generator for.
+
+Default generator will be called only if a user defined generator does not
+exsit. 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, is the random supply, in & out.
+(Ignore the rest of arguments) use91.m shows a user defined generater 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 argurment, and
+assign random_supply output equals 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
+generator 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 suppose to generate. Not much use; can be used
+ like an assertion.
+
+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_supply input
+
+6th input of type rnd random_supply output, let output = input if not used.
+
+Look at rand_union/6 to find out how to wrote code which extract/analysis specific frequency amd
+general frequency.
+Look at gen/7 to find out how to wrote code which extract/analysis user defined generators
+
+
+
+
+
+
+
+
+
+
+
+
+
+
Index: quickcheck/tutes/index.html
===================================================================
RCS file: index.html
diff -N index.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ index.html Mon Feb 5 16:01:53 2001
@@ -0,0 +1,36 @@
+<html>
+<head>
+ <TITLE> QuickCheck </TITLE>
+</head>
+
+<H1> Quickcheck for Mercury</H1>
+
+<H3> HTML Version </H3>
+
+<ul>
+<li> <a href="T1.html"><pre>Tutorial 1.1 Intro & `===`</pre></a>
+<li> <a href="T2.html"><pre>Tutorial 1.2 Conditional laws & `===>``</pre></a>
+<li> <a href="T3.html"><pre>Tutorial 1.3 Monitoring Data, to_trivial/3, `>>>`</pre></a>
+<li> <a href="T4.html"><pre>Tutorial 1.4 Summary - Invariant Function & Property </pre></a>
+<li> <a href="T5.html"><pre>Tutorial 2.1 Generators basic</pre></a>
+<li> <a href="T6.html"><pre>Tutorial 2.2 Discriminated union & Specific Frequency</pre></a>
+<li> <a href="T7.html"><pre>Tutorial 2.3 General Frequency</pre></a>
+<li> <a href="T8.html"><pre>Tutorial 2.4 Random Functions</pre></a>
+<li> <a href="T9.html"><pre>Tutorial 3.1 User Defined Generators</pre></a>
+</ul>
+
+<p>
+----------------
+<p>
+
+<H3> MS Word Version </H3>
+<ul>
+<li> <a href="T1.doc">Tutorial 1</a>
+<li> Tutorial 2</a>
+<li> Tutorial 3</a>
+</ul>
+
+Feedback? Mail <a href="mailto:xcsm at students.cs.mu.oz.au">Simon</a>.
+
+</BODY>
+</html>
Index: quickcheck/tutes/mymax.m
===================================================================
RCS file: mymax.m
diff -N mymax.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ mymax.m Mon Feb 5 16:01:53 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: quickcheck/tutes/numbers.html
===================================================================
RCS file: numbers.html
diff -N numbers.html
--- /dev/null Wed Nov 15 09:24:47 2000
+++ numbers.html Mon Feb 5 16:01:53 2001
@@ -0,0 +1,48 @@
+<html>
+<head>
+ <TITLE> QuickCheck </TITLE>
+</head>
+<a href="index.html">Back to main</a>
+<H1> QuickCheck Tutorial 6 </H1>
+<pre>
+
+:- type bullet
+ ---> good(color)
+ ; inaccurate(color)
+ ; defective(color).
+
+:- 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 input, however only 0 to 100 is meaningful.
+Any number smaller than zero, is treated as being zero.
+Any number greater than 100, is treated as being 100.
+
+the 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). However the 1st example is more
+effecient. The ratio determines distribution, and use of larger
+numbers add speed.
+
+
+
+
+
Index: quickcheck/tutes/testrev.m
===================================================================
RCS file: testrev.m
diff -N testrev.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ testrev.m Mon Feb 5 16:01:53 2001
@@ -0,0 +1,13 @@
+:- module testrev.
+
+:- interface.
+:- import_module list.
+
+:- func testrev(list(T)) = list(T).
+:- mode testrev(in) = out is det.
+
+:- implementation.
+
+testrev([]) = [].
+testrev([X|Xs]) = Ys :-
+ list__append(testrev(Xs), [X], Ys).
Index: quickcheck/tutes/testrev2.m
===================================================================
RCS file: testrev2.m
diff -N testrev2.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ testrev2.m Mon Feb 5 16:01:53 2001
@@ -0,0 +1,14 @@
+:- module testrev2.
+
+:- interface.
+:- import_module list.
+
+:- pred testrev2(list(T), list(T)).
+:- mode testrev2(in, out) is det.
+
+:- implementation.
+
+testrev2([], []).
+testrev2([X|Xs], Ys):-
+ testrev2(Xs, Reversed),
+ list__append(Reversed, [X], Ys).
Index: quickcheck/tutes/use.m
===================================================================
RCS file: use.m
diff -N use.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use.m Mon Feb 5 16:01:53 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, testrev.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(testing), "sample testing").
+
+%------------------------------------------------------------------------------%
+% Invariant test functions
+%------------------------------------------------------------------------------%
+
+:- func testing(list(int), list(int)) = property.
+testing(Xs, Ys) =
+ testrev(Xs ++ Ys) `===` (testrev(Ys) ++ testrev(Xs)).
+
+
Index: quickcheck/tutes/use1.m
===================================================================
RCS file: use1.m
diff -N use1.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use1.m Mon Feb 5 16:01:53 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, testrev2.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(testing2), "testing2").
+
+%------------------------------------------------------------------------------%
+% Invariant test functions
+%------------------------------------------------------------------------------%
+
+
+:- func testing2(list(int), list(int)) = property.
+testing2(Xs, Ys) = (Left `===` Right) :-
+ testrev2((Xs ++ Ys), Left),
+ testrev2(Ys, Part_a),
+ testrev2(Xs, Part_b),
+ Right = Part_a ++ Part_b.
+
+
Index: quickcheck/tutes/use11.m
===================================================================
RCS file: use11.m
diff -N use11.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use11.m Mon Feb 5 16:01:53 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, testrev.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(func(Xs `with_type` list(int), Ys `with_type` list(int))
+ = testrev(Xs ++ Ys) `===` (testrev(Ys) ++ testrev(Xs))),
+ "sample testing").
+
+
Index: quickcheck/tutes/use2.m
===================================================================
RCS file: use2.m
diff -N use2.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use2.m Mon Feb 5 16:01:53 2001
@@ -0,0 +1,311 @@
+%---------------------------------------------------------------------------%
+% file: use.m
+% author: xcsm
+%
+% Sample main moudle to call quickcheck()
+%
+%---------------------------------------------------------------------------%
+
+:- module use.
+
+:- interface.
+
+:- use_module io.
+
+:- pred main(io__state, io__state).
+:- mode main(di, uo) is det.
+
+%---------------------------------------------------------------------------%
+
+:- implementation.
+
+:- import_module int, integer, char, float, list, string, std_util, bool.
+:- import_module qcheck, rnd, somesort, testrev.
+
+%---------------------------------------------------------------------------%
+% arbitrary user-defined types for testing purposes
+%---------------------------------------------------------------------------%
+
+:- type mypoint2 == mypoint.
+:- type mypoint
+ ---> mypair(int, int).
+:- type color
+ ---> red(float)
+ ; blue(float, float)
+ ; green(char, mydays, int).
+:- type greeting
+ ---> hello
+ ; go_away
+ ; hi
+ ; i_hate_you.
+:- type wave
+ ---> good(twofaces)
+ ; bad(twofaces).
+:- type twofaces
+ ---> odd
+ ; even.
+:- type mynumber
+ ---> zero
+ ; one
+ ; two(wave, wave)
+ ; three
+ ; four
+ ; five.
+:- type mydays
+ ---> monday(char, char)
+ ; tuestday(color, color)
+ ; wednesday(int)
+ ; thursday.
+:- type strange(T1, T2)
+ ---> wierd(T1, T2, T1).
+:- type employee
+ ---> employee(
+ name :: string,
+ age :: int,
+ department :: string
+ ).
+
+:- type testtree
+ ---> node(int)
+ ; {testtree, testtree, testtree}.
+
+%---------------------------------------------------------------------------%
+main -->
+ qcheck(qcheck__f(prop1)),
+ qcheck(qcheck__f(prop2)),
+ qcheck(qcheck__f(prop3)).
+
+
+ % outputs a specific frequency list
+:- pred freq(list(list(frequency))).
+:- mode freq(out) is det.
+freq(X) :-
+ X = [[ {10, []},
+ {20, []},
+ {30, [ [{90,[[{90,[]}, {10,[]}]]}, {10,[]}],
+ [{90,[]}, {10,[]}]
+ ]},
+ {40, []},
+ {50, []},
+ {60, []}
+ ]].
+
+ % outputs a specific frequency list
+:- pred freq1(list(list(frequency))).
+:- mode freq1(out) is det.
+freq1(X) :-
+ X = [[ {10, []},
+ {90, []}
+ ],
+ [ {20, []},
+ {80, []}
+ ]
+ ].
+
+
+ % outpust a general frequency list
+:- pred freq_general(list({type_desc, list(frequency)})).
+:- mode freq_general(out) is det.
+freq_general(X) :-
+ X = [
+ {type_of(['A']), [{33, []}, {67, []}] }
+ ].
+
+
+ % user-defined generator for type int
+:- func gen_int(type_desc, list(frequency), list({type_desc, list(frequency)}),
+ list(user_gen_type), rnd, rnd) = univ.
+:- mode gen_int(in, in, in, list_skel_in(user_gen_inst), in, out) = out is det.
+gen_int(_, _, _, _, RS0, RS) = Univ :-
+ RS = RS0,
+ Univ = univ(98).
+
+
+ % user-defined generator for type char
+:- func gen_char(type_desc, list(frequency), list({type_desc, list(frequency)}),
+ list(user_gen_type), rnd, rnd) = univ.
+:- mode gen_char(in, in, in, list_skel_in(user_gen_inst), in, out) = out is det.
+gen_char(_, _, _, _, RS0, RS) = Univ :-
+ RS = RS0,
+ Univ = univ('P').
+
+
+
+ % user-defined generator for a function
+:- func r_function(type_desc, list(frequency), list({type_desc,
+ list(frequency)}), list(user_gen_type), rnd, rnd) = univ.
+:- mode r_function(in,in,in,list_skel_in(user_gen_inst),in,out) = out is det.
+r_function(_, _, _, _, RS0, RS) = Univ :-
+ Univ = univ(give_func),
+ RS = RS0.
+
+/*
+ rnd__irange(-100, 100, X, RS0, RS),
+ type_ctor_and_args(Type, _, Args),
+ (if Args = [ArgType1, RetType]
+ then
+ has_type(Arg1, ArgType1),
+ has_type(RetVal, RetType),
+ Func = dummy1(X),
+ nailFuncType(Arg1, RetVal, Func),
+ Univ = univ(Func)
+ else if Args = [ArgType1, ArgType2, RetType]
+ then
+ has_type(Arg1, ArgType1),
+ has_type(Arg2, ArgType2),
+ has_type(RetVal, RetType),
+ Func = dummy2(X),
+ nailFuncType(Arg1, Arg2, RetVal, Func),
+ Univ = univ(Func)
+ else if Args = [ArgType1, ArgType2, ArgType3, RetType]
+ then
+ has_type(Arg1, ArgType1),
+ has_type(Arg2, ArgType2),
+ has_type(Arg3, ArgType3),
+ has_type(RetVal, RetType),
+ Func = dummy3(X),
+ nailFuncType(Arg1, Arg2, Arg3, RetVal, Func),
+ Univ = univ(Func)
+ else
+ error("rand_function/3 error \n")
+ ).
+*/
+
+
+ % a function for curry
+:- func give_func(int, char, int) = int.
+:- mode give_func(in, in, in) = out is det.
+give_func(A, B, C) = D :-
+ (if B = 'B'
+ then
+ D = A + C
+ else
+ D = A - C
+ ).
+
+:- func mytest(list(char)) = bool.
+:- mode mytest(in) = out is det.
+mytest(List) = Bool :-
+ (if list_length(List) = 2
+ then
+ Bool = no
+ else
+ Bool = yes
+ ).
+
+%------------------------------------------------------------------------------%
+% Invariant test functions
+%------------------------------------------------------------------------------%
+
+:- func prop1(int) = property.
+prop1(X) =
+ testrev([X]) `===` [X].
+
+:- func prop2(list(int), list(int)) = property.
+prop2(Xs, Ys) =
+ testrev(Xs ++ Ys) `===` (testrev(Ys) ++ testrev(Xs)).
+
+:- func prop3(list(int)) = property.
+prop3(Xs) =
+ testrev(testrev(Xs)) `===` Xs.
+
+:- func prop4(list(char), list(int)) = property.
+prop4(Xs, X2) = R :-
+ (if somesort(Xs, Ys),
+ somesort(Ys, Zs),
+ Ys = Zs
+ then
+ R1 = yes
+ else
+ R1 = no
+ ),
+ R2 = to_trivial(Xs, [], R1),
+ R3 = to_condition(mytest(Xs), R2),
+ R = to_collect(list_length(Xs), R3).
+
+:- func prop5 = property.
+prop5 = R1 :-
+ (if 1 = 1
+ then
+ R1 = yes
+ else
+ R1 = no
+ ).
+
+:- func prop6(mypoint2, float, {int, string}, char) = property.
+prop6(X1, _, _, _) = R1 :-
+ ( if 1 = 1
+ then
+ R1 = yes
+ else
+ R1 = no
+ ).
+
+
+:- func prop7(strange(int, char), strange(int, char)) = property.
+prop7(_, _) = R1 :-
+ ( if 1 = 1
+ then
+ R1 = yes
+ else
+ R1 = no
+ ).
+
+
+:- func prop8(int, strange(int, char), bool) = property.
+prop8(_,_,_) = R1 :-
+ ( if 1 = 1
+ then
+ R1 = yes
+ else
+ R1 = no
+ ).
+
+
+:- func prop8a(employee) = property.
+prop8a(X1) = X1 `===` employee("hi", 7, "CS").
+
+
+:- func prop8b(mynumber) = property.
+prop8b(X1) = R :-
+ ( if X1 = zero
+ then
+ R1 = yes
+ else
+ R1 = no
+ ),
+ R2 = to_collect(X1, R1),
+ R = to_trivial(X1, zero, R2).
+
+:- func prop8c(testtree) = property.
+prop8c(X1) = R :-
+ ( if X1 = node(6)
+ then
+ R = yes
+ else
+ R = no
+ ).
+
+:- func prop9({mydays, strange(integer, list(char)), func(list(int), mydays)=int}) = property.
+:- mode prop9(in(bound({ground, ground, func(in,in)=out is det}))) = out is det.
+prop9(Y) = R1 :-
+ Y = {Mydays, _, X1},
+ ( if X1([1,2], Mydays) > 9
+ then
+ R1 = yes
+ else
+ R1 = no
+ ).
+
+:- func prop10(func(int, int) = int) = property.
+:- mode prop10(in(func(in,in)=out is det)) = out is det.
+prop10(X1) = R :-
+ ( if X1(88,1) > 9
+ then
+ R1 = yes
+ else
+ R1 = no
+ ),
+ R = to_collect(X1, R1).
+
+
Index: quickcheck/tutes/use20.m
===================================================================
RCS file: use20.m
diff -N use20.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use20.m Mon Feb 5 16:01:53 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: quickcheck/tutes/use21.m
===================================================================
RCS file: use21.m
diff -N use21.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use21.m Mon Feb 5 16:01:53 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: quickcheck/tutes/use31.m
===================================================================
RCS file: use31.m
diff -N use31.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use31.m Mon Feb 5 16:01:53 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, testrev.
+
+%---------------------------------------------------------------------------%
+
+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) =
+ testrev(testrev(Xs)) `===` Xs.
+
+:- func testing2(list(float)) = property.
+testing2(Xs) =
+ to_trivial([], Xs, testrev(testrev(Xs)) `===` Xs).
+
+:- func testing3(list(float)) = property.
+testing3(Xs) =
+ to_trivial(1,
+ list_length(Xs),
+ to_trivial([], Xs, testrev(testrev(Xs)) `===` Xs)
+ ).
+
+:- func testing4(list(float)) = property.
+testing4(Xs) =
+ list_length(Xs) `>>>` (testrev(testrev(Xs)) `===` Xs).
Index: quickcheck/tutes/use33.m
===================================================================
RCS file: use33.m
diff -N use33.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use33.m Mon Feb 5 16:01:53 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, testrev.
+
+%---------------------------------------------------------------------------%
+
+main -->
+ qcheck(qcheck__f(testing5), "testing5").
+
+:- func testing5(list(float)) = property.
+testing5(Xs) =
+ odd_even(Xs) `>>>`
+ (list_length(Xs) `>>>` (testrev(testrev(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: quickcheck/tutes/use51.m
===================================================================
RCS file: use51.m
diff -N use51.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use51.m Mon Feb 5 16:01:53 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: quickcheck/tutes/use62.m
===================================================================
RCS file: use62.m
diff -N use62.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use62.m Mon Feb 5 16:01:53 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: quickcheck/tutes/use71.m
===================================================================
RCS file: use71.m
diff -N use71.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use71.m Mon Feb 5 16:01:53 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, testrev.
+
+%---------------------------------------------------------------------------%
+
+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) `>>>` (testrev(testrev(Xs)) `===` Xs).
Index: quickcheck/tutes/use81.m
===================================================================
RCS file: use81.m
diff -N use81.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use81.m Mon Feb 5 16:01:53 2001
@@ -0,0 +1,60 @@
+:- 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] ]
+ ).
+
+
+
+
Index: quickcheck/tutes/use91.m
===================================================================
RCS file: use91.m
diff -N use91.m
--- /dev/null Wed Nov 15 09:24:47 2000
+++ use91.m Mon Feb 5 16:01:53 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