Introduction

A First Taste of Testing

Consider the following definition of a function remove, which takes a natural number x and a list of nats l and removes x from the list.
Fixpoint remove (x : nat) (l : list nat) : list nat :=
  match l with
    | [] ⇒ []
    | h::t ⇒ if h =? x then t else h :: remove x t
  end.
One possible specification for remove might be this property...
Conjecture removeP : ∀ x l, ¬(In x (remove x l)).
...which says that x never occurs in the result of remove x l for any x and l. (Conjecture foo... means the same as Theorem foo... Admitted. Formally, foo is treated as an axiom.)

Sadly, this property is false, as we would (eventually) discover if we were to try to prove it.

A different -- perhaps much more efficient -- way to discover the discrepancy between the definition and specification is to test it:
(* QuickChick removeP. *)
(Try uncommenting and evaluating the previous line.)

The QuickChick command takes an "executable" property (we'll see later exactly what this means) and attempts to falsify it by running it on many randomly generated inputs, resulting in output like this: 
       0
       [0, 0]
       Failed! After 17 tests and 12 shrinks
This means that, if we run remove with x being 0 and l being the two-element list containing two zeros, then the property removeP fails.

Overview

Property-based random testing involves four basic ingredients:
  • an executable property like removeP,
  • generators for random elements of the types of the inputs to the property (here, numbers and lists of numbers),
  • printers for converting data structures like numbers and lists to strings when reporting counterexamples, and
  • shrinkers, which are used to minimize counterexamples.

We will delve into each of these in detail later on, but first we need to make a digression to explain Coq's support for typeclasses, which QuickChick uses extensively both internally and in its programmatic interface to users. This is the Typeclasses chapter.
In the QC chapter we'll cover the core concepts and features of QuickChick itself.
The TImp chapter develops a small case study around a typed variant of the Imp language.
The QuickChickTool chapter presents a command line tool, quickChick, that supports larger-scale projects and mutation testing.
The QuickChickInterface chapter is a complete reference manual for QuickChick.
Finally, the Postscript chapter gives some suggestions for further reading.