Qcheck
QuickCheck inspired property-based testing for OCaml.
Install / Use
/learn @c-cube/QcheckREADME
= QCheck :toc: macro :toclevels: 4 :source-highlighter: pygments
QuickCheck inspired property-based testing for OCaml.
image::https://github.com/c-cube/qcheck/actions/workflows/main.yml/badge.svg[alt="build", link=https://github.com/c-cube/qcheck/actions/workflows/main.yml]
== Overview
QCheck consists of a collection of opam packages and extensions:
qcheck-core- provides the core property-based testing API and depends only onunixanddune.qcheck-ounit- provides an integration layer for https://github.com/gildor478/ounit[OUnit]qcheck-alcotest- provides an integration layer for https://github.com/mirage/alcotest[alcotest]qcheck- provides a compatibility API with older versions ofqcheck, using bothqcheck-coreandqcheck-ounit.ppx_deriving_qcheck- provides a preprocessor to automatically derive generators
In addition, the https://github.com/ocaml-multicore/multicoretests[multicoretests]
repository offers
qcheck-stm- for running sequential and parallel model-based testsqcheck-lin- for testing an API for sequential consistencyqcheck-multicoretests-util- a small library of utility extensions, such as properties with time outs
To construct advanced random generators, the following libraries might also be of interest:
- https://gitlab.inria.fr/fpottier/feat/[
feat] - a library for functional enumeration and sampling of algebraic data types - https://github.com/gasche/random-generator/[
random-generator] - a library experimenting with APIs for random generation
Earlier qcheck spent some time in https://github.com/vincent-hugot/iTeML[qtest],
but was since made standalone again.
== Documentation
The documentation for the 5 opam packages https://c-cube.github.io/qcheck/[is available here].
The section <<examples>> below offer a brief introduction to the library. These examples are based on an earlier https://cedeela.fr/quickcheck-for-ocaml[blog post by Simon] that also discusses some design choices; however, be warned that the API changed since then, so the blog post code will not work as is.
Jan's http://janmidtgaard.dk/quickcheck/index.html[course material on FP and property-based testing] also offers an introduction to QCheck.
The OCaml textbook from Cornell University also contains https://cs3110.github.io/textbook/chapters/correctness/randomized.html[a chapter about property-based testing with QCheck].
== Build and Install
You can install QCheck via opam:
$ opam install qcheck-core
This provides a minimal installation without needless dependencies.
Install the bigger qcheck package instead for compatibility with qcheck.0.8
and before:
$ opam install qcheck
To build the library from source
$ make
Normally, for contributors, opam pin https://github.com/c-cube/qcheck
will pin the 5 opam packages from this repository.
== License
The code is now released under the BSD license.
[[examples]] == An Introduction to the Library
First, let's see a few tests. Let's open a toplevel (e.g. utop) and type the following to load QCheck:
[source,OCaml]
#require "qcheck-core";;
NOTE: alternatively, it is now possible to locally do: dune utop src
to load qcheck.
=== List Reverse is Involutive
We write a random test for checking that List.rev (List.rev l) = l for
any list l:
[source,OCaml]
let test = QCheck.Test.make ~count:1000 ~name:"list_rev_is_involutive" QCheck.(list nat_small) (fun l -> List.rev (List.rev l) = l);;
(* we can check right now the property... *) QCheck.Test.check_exn test;;
In the above example, we applied the combinator list to
the random generator nat_small (ints between 0 and 100), to create a
new generator of lists of random integers. These builtin generators
come with printers and shrinkers which are handy for outputting and
minimizing a counterexample when a test fails.
Consider the buggy property List.rev l = l:
[source,OCaml]
let test = QCheck.Test.make ~count:1000 ~name:"my_buggy_test" QCheck.(list nat_small) (fun l -> List.rev l = l);;
When we run this test we are presented with a counterexample:
[source,OCaml]
QCheck.Test.check_exn test;;
Exception:
test my_buggy_test failed on ≥ 1 cases: [0; 1] (after 11 shrink steps)
In this case QCheck found the minimal counterexample [0;1] to the property
List.rev l = l and it spent 11 steps shrinking it.
Now, let's run the buggy test with a decent runner that will print the results nicely (the exact output will change at each run, because of the random seed):
#require "qcheck-core.runner";;
QCheck_base_runner.run_tests [test];;
random seed: 452768242
--- Failure --------------------------------------------------------------------
Test my_buggy_test failed (14 shrink steps):
[0; 1]
failure (1 tests failed, 0 tests errored, ran 1 tests)
- : int = 1
For an even nicer output QCheck_base_runner.run_tests also accepts an optional
parameter ~verbose:true.
=== Mirrors and Trees
QCheck provides many useful combinators to write generators, especially for
recursive types, algebraic types, and tuples.
Let's see how to generate random trees:
[source,OCaml]
type tree = Leaf of int | Node of tree * tree
let leaf x = Leaf x let node x y = Node (x,y)
let tree_gen = QCheck.Gen.(sized @@ fix (fun self n -> match n with | 0 -> map leaf nat | n -> oneof_weighted [1, map leaf nat; 2, map2 node (self (n/2)) (self (n/2))] ));;
(* generate a few trees, just to check what they look like: *) QCheck.Gen.generate ~n:20 tree_gen;;
let arbitrary_tree = let open QCheck.Iter in let rec print_tree = function | Leaf i -> "Leaf " ^ (string_of_int i) | Node (a,b) -> "Node (" ^ (print_tree a) ^ "," ^ (print_tree b) ^ ")" in let rec shrink_tree = function | Leaf i -> QCheck.Shrink.int i >|= leaf | Node (a,b) -> of_list [a;b] <+> (shrink_tree a >|= fun a' -> node a' b) <+> (shrink_tree b >|= fun b' -> node a b') in QCheck.make tree_gen ~print:print_tree ~shrink:shrink_tree;;
Here we write a generator of random trees, tree_gen, using
the fix combinator. fix is sized (it is a function from int to
a random generator; in particular for size 0 it returns only leaves).
The sized combinator first generates a random size, and then applies
its argument to this size.
Other combinators include monadic abstraction, lifting functions, generation of lists, arrays, and a choice function.
Then, we define arbitrary_tree, a tree QCheck.arbitrary value, which
contains everything needed for testing on trees:
- a random generator (mandatory), weighted with
oneof_weightedto increase the chance of generating deep trees - a printer (optional), very useful for printing counterexamples
- a shrinker (optional), very useful for trying to reduce big counterexamples to small counterexamples that are usually more easy to understand.
The above shrinker strategy is to
- reduce the integer leaves, and
- substitute an internal
Nodewith either of its subtrees or by splicing in a recursively shrunk subtree.
A range of combinators in QCheck.Shrink and QCheck.Iter are available
for building shrinking functions.
We can write a failing test using this generator to see the printer and shrinker in action:
[source,OCaml]
let rec mirror_tree (t:tree) : tree = match t with | Leaf _ -> t | Node (a,b) -> node (mirror_tree b) (mirror_tree a);;
let test_buggy = QCheck.Test.make ~name:"buggy_mirror" ~count:200 arbitrary_tree (fun t -> t = mirror_tree t);;
QCheck_base_runner.run_tests [test_buggy];;
This test fails with:
[source,OCaml]
--- Failure --------------------------------------------------------------------
Test mirror_buggy failed (6 shrink steps):
Node (Leaf 0,Leaf 1)
failure (1 tests failed, 0 tests errored, ran 1 tests)
- : int = 1
With the (new found) understanding that mirroring a tree changes its structure, we can formulate another property that involves sequentializing its elements in a traversal:
[source,OCaml]
let tree_infix (t:tree): int list = let rec aux acc t = match t with | Leaf i -> i :: acc | Node (a,b) -> aux (aux acc b) a in aux [] t;;
let test_mirror = QCheck.Test.make ~name:"mirror_tree" ~count:200 arbitrary_tree (fun t -> List.rev (tree_infix t) = tree_infix (mirror_tree t));;
QCheck_base_runner.run_tests [test_mirror];;
=== Integrated shrinking with QCheck2
You may have noticed the shrink_tree function above to reduce tree
counterexamples. With the newer QCheck2 module, this is not needed
as shrinking is built into its generators.
For example, we can rewrite the above tree generator to QCheck2 by just
changing the QCheck occurrences to QCheck2:
[source,OCaml]
type tree = Leaf of int | Node of tree * tree
let leaf x = Leaf x let node x y = Node (x,y)
let tree_gen = QCheck2.Gen.(sized @@ fix (fun self n -> match n with | 0 -> map leaf nat | n -> oneof_weighted [1, map leaf nat; 2, map2 node (self (n/2)) (self (n/2))] ));;
(* generate a few trees with QCheck2, just to check what they look like: *) QCheck2.Gen.generate ~n:20 tree_gen;;
QCheck2.Test.make has a slightly different API than QCheck.Test.make,
in that it accepts an optional ~print argument and consumes generators
directly built with QCheck2.Gen:
[source,OCaml]
let rec print_tree = function | Leaf i -> "Leaf " ^ (string_of_int i) | Node (a,b) -> "Node (" ^ (print_tree a) ^ "," ^ (print_tree b) ^ ")";;
let rec mirror_tree (t:tree) : tree = match t with | Leaf _ -> t | Node (a,b) -> node (mirror_tree b) (mirror_tree a);;
let test_buggy =
