# QuickChickInterface: QuickChick Reference Manual

From QuickChick Require Import QuickChick.

Require Import ZArith Strings.Ascii Strings.String.

From ExtLib.Structures Require Import Functor Applicative.

QuickChick provides a large collection of combinators and
notations for writing property-based random tests. This file
documents the entire public interface (the module type
QuickChickSig).

# The Show Typeclass

Declare Instance showNat : Show nat.

Declare Instance showBool : Show bool.

Declare Instance showZ : Show Z.

Declare Instance showString : Show string.

Declare Instance showList :

forall {A : Type} `{Show A}, Show (list A).

Declare Instance showPair :

forall {A B : Type} `{Show A} `{Show B}, Show (A * B).

Declare Instance showOpt :

forall {A : Type} `{Show A}, Show (option A).

Declare Instance showEx :

forall {A} `{Show A} P, Show ({x : A | P x}).

Declare Instance showBool : Show bool.

Declare Instance showZ : Show Z.

Declare Instance showString : Show string.

Declare Instance showList :

forall {A : Type} `{Show A}, Show (list A).

Declare Instance showPair :

forall {A B : Type} `{Show A} `{Show B}, Show (A * B).

Declare Instance showOpt :

forall {A : Type} `{Show A}, Show (option A).

Declare Instance showEx :

forall {A} `{Show A} P, Show ({x : A | P x}).

When defining Show instance for your own datatypes, you sometimes need to
start a new line for better printing. nl is a shorthand for it.

Run a generator with a size parameter (a natural number denoting
the maximum depth of the generated A) and a random seed.

The semantics of a generator is its set of possible outcomes.

Parameter semGen : forall {A : Type} (g : G A), set A.

Parameter semGenSize : forall {A : Type} (g : G A) (size : nat), set A.

Parameter semGenSize : forall {A : Type} (g : G A) (size : nat), set A.

## Structural Combinators

Declare Instance Monad_G : Monad G.

Declare Instance Functor_G : Functor G.

Declare Instance Applicative_G : Applicative G.

A variant of monadic bind where the continuation also takes a

*proof*that the value received is within the set of outcomes of the first generator.
Parameter bindGen' : forall {A B : Type} (g : G A),

(forall (a : A), (a \in semGen g) -> G B) -> G B.

(forall (a : A), (a \in semGen g) -> G B) -> G B.

A variant of bind for the (G (option --)) monad. Useful for
chaining generators that can fail / backtrack.

## Basic Generator Combinators

Parameter listOf : forall {A : Type}, G A -> G (list A).

Parameter vectorOf : forall {A : Type}, nat -> G A -> G (list A).

Parameter vectorOf : forall {A : Type}, nat -> G A -> G (list A).

elems_ a l constructs a generator from a list l and a
default element a. If l is non-empty, the generator picks an
element from l uniformly; otherwise it always yields a.

Similar to elems_, instead of choosing from a list of As,
oneOf_ g l returns g if l is empty; otherwise it uniformly
picks a generator for A in l.

We can also choose generators with distributions other than the
uniform one. freq_ g l returns g if l is empty;
otherwise it chooses a generator from l, where the first field
indicates the chance that the second field is chosen. For example,
freq_ z [(2, x); (3, y)] has 40% probability of choosing
x and 60% probability of choosing y.

Try all generators until one returns a Some value or all failed once with
None. The generators are picked at random according to their weights
(like frequency), and each one is run at most once.

Internally, the G monad hides a size parameter that can be accessed by
generators. The sized combinator provides such access. The resize
combinator sets it.

Parameter sized : forall {A: Type}, (nat -> G A) -> G A.

Parameter resize : forall {A: Type}, nat -> G A -> G A.

Parameter resize : forall {A: Type}, nat -> G A -> G A.

Generate-and-test approach to generate data with preconditions.

Parameter suchThatMaybe :

forall {A : Type}, G A -> (A -> bool) -> G (option A).

Parameter suchThatMaybeOpt :

forall {A : Type}, G (option A) -> (A -> bool) -> G (option A).

forall {A : Type}, G A -> (A -> bool) -> G (option A).

Parameter suchThatMaybeOpt :

forall {A : Type}, G (option A) -> (A -> bool) -> G (option A).

The elems_, oneOf_, and freq_ combinators all take
default values; these are only used if their list arguments are
empty, which should not normally happen. The QcDefaultNotation
sub-module exposes notation (without the underscores) to hide this default.

elems is a shorthand for elems_ without a default argument.

Notation " 'elems' [ x ] " :=

(elems_ x (cons x nil)) : qc_scope.

Notation " 'elems' [ x ; y ] " :=

(elems_ x (cons x (cons y nil))) : qc_scope.

Notation " 'elems' [ x ; y ; .. ; z ] " :=

(elems_ x (cons x (cons y .. (cons z nil) ..))) : qc_scope.

Notation " 'elems' ( x ;; l ) " :=

(elems_ x (cons x l)) (at level 1, no associativity) : qc_scope.

(elems_ x (cons x nil)) : qc_scope.

Notation " 'elems' [ x ; y ] " :=

(elems_ x (cons x (cons y nil))) : qc_scope.

Notation " 'elems' [ x ; y ; .. ; z ] " :=

(elems_ x (cons x (cons y .. (cons z nil) ..))) : qc_scope.

Notation " 'elems' ( x ;; l ) " :=

(elems_ x (cons x l)) (at level 1, no associativity) : qc_scope.

oneOf is a shorthand for oneOf_ without a default argument.

Notation " 'oneOf' [ x ] " :=

(oneOf_ x (cons x nil)) : qc_scope.

Notation " 'oneOf' [ x ; y ] " :=

(oneOf_ x (cons x (cons y nil))) : qc_scope.

Notation " 'oneOf' [ x ; y ; .. ; z ] " :=

(oneOf_ x (cons x (cons y .. (cons z nil) ..))) : qc_scope.

Notation " 'oneOf' ( x ;; l ) " :=

(oneOf_ x (cons x l)) (at level 1, no associativity) : qc_scope.

(oneOf_ x (cons x nil)) : qc_scope.

Notation " 'oneOf' [ x ; y ] " :=

(oneOf_ x (cons x (cons y nil))) : qc_scope.

Notation " 'oneOf' [ x ; y ; .. ; z ] " :=

(oneOf_ x (cons x (cons y .. (cons z nil) ..))) : qc_scope.

Notation " 'oneOf' ( x ;; l ) " :=

(oneOf_ x (cons x l)) (at level 1, no associativity) : qc_scope.

freq is a shorthand for freq_ without a default argument.

Notation " 'freq' [ x ] " :=

(freq_ x (cons x nil)) : qc_scope.

Notation " 'freq' [ ( n , x ) ; y ] " :=

(freq_ x (cons (n, x) (cons y nil))) : qc_scope.

Notation " 'freq' [ ( n , x ) ; y ; .. ; z ] " :=

(freq_ x (cons (n, x) (cons y .. (cons z nil) ..))) : qc_scope.

Notation " 'freq' ( ( n , x ) ;; l ) " :=

(freq_ x (cons (n, x) l)) (at level 1, no associativity) : qc_scope.

End QcDefaultNotation.

(freq_ x (cons x nil)) : qc_scope.

Notation " 'freq' [ ( n , x ) ; y ] " :=

(freq_ x (cons (n, x) (cons y nil))) : qc_scope.

Notation " 'freq' [ ( n , x ) ; y ; .. ; z ] " :=

(freq_ x (cons (n, x) (cons y .. (cons z nil) ..))) : qc_scope.

Notation " 'freq' ( ( n , x ) ;; l ) " :=

(freq_ x (cons (n, x) l)) (at level 1, no associativity) : qc_scope.

End QcDefaultNotation.

The original version of QuickChick used elements, oneof and frequency
as the default-argument versions of the corresponding combinators.
These have since been deprecated in favor of a more consistent
naming scheme.

## Choosing from Intervals

Existing Class OrdType.

Declare Instance OrdBool : OrdType bool.

Declare Instance OrdNat : OrdType nat.

Declare Instance OrdZ : OrdType Z.

We also expect the random function to be able to pick every element in any
given interval.

Existing Class ChoosableFromInterval.

QuickChick has provided some instances for ordered data types that are
choosable from intervals, including bool, nat, and Z.

Declare Instance ChooseBool : ChoosableFromInterval bool.

Declare Instance ChooseNat : ChoosableFromInterval nat.

Declare Instance ChooseZ : ChoosableFromInterval Z.

Declare Instance ChooseNat : ChoosableFromInterval nat.

Declare Instance ChooseZ : ChoosableFromInterval Z.

choose l r generates a value between l and r, inclusive the two
extremes. It causes a runtime error if r < l.

## The Gen and GenSized Typeclasses

Here are some basic instances for generators:

Declare Instance genBoolSized : GenSized bool.

Declare Instance genNatSized : GenSized nat.

Declare Instance genZSized : GenSized Z.

Declare Instance genListSized :

forall {A : Type} `{GenSized A}, GenSized (list A).

Declare Instance genList :

forall {A : Type} `{Gen A}, Gen (list A).

Declare Instance genOption :

forall {A : Type} `{Gen A}, Gen (option A).

Declare Instance genPairSized :

forall {A B : Type} `{GenSized A} `{GenSized B}, GenSized (A*B).

Declare Instance genPair :

forall {A B : Type} `{Gen A} `{Gen B}, Gen (A * B).

Declare Instance genNatSized : GenSized nat.

Declare Instance genZSized : GenSized Z.

Declare Instance genListSized :

forall {A : Type} `{GenSized A}, GenSized (list A).

Declare Instance genList :

forall {A : Type} `{Gen A}, Gen (list A).

Declare Instance genOption :

forall {A : Type} `{Gen A}, Gen (option A).

Declare Instance genPairSized :

forall {A B : Type} `{GenSized A} `{GenSized B}, GenSized (A*B).

Declare Instance genPair :

forall {A B : Type} `{Gen A} `{Gen B}, Gen (A * B).

## Generators for Data Satisfying Inductive Predicates

## The Shrink Typeclass

Declare Instance shrinkBool : Shrink bool.

Declare Instance shrinkNat : Shrink nat.

Declare Instance shrinkZ : Shrink Z.

Declare Instance shrinkList {A : Type} `{Shrink A} : Shrink (list A).

Declare Instance shrinkPair {A B} `{Shrink A} `{Shrink B} : Shrink (A * B).

Declare Instance shrinkOption {A : Type} `{Shrink A} : Shrink (option A).

Declare Instance shrinkNat : Shrink nat.

Declare Instance shrinkZ : Shrink Z.

Declare Instance shrinkList {A : Type} `{Shrink A} : Shrink (list A).

Declare Instance shrinkPair {A B} `{Shrink A} `{Shrink B} : Shrink (A * B).

Declare Instance shrinkOption {A : Type} `{Shrink A} : Shrink (option A).

## The Arbitrary Typeclass

## The Generator Typeclass Hierarchy

The Checkable class indicates we can check a type A.
Class Checkable (A : Type) : Type :=
{
checker : A -> Checker
}.
Boolean checkers always pass or always fail.

The unit checker is always discarded (that is, it represents a
useless test). It is used, for example, in the implementation of
the "implication Checker" combinator ==>.

Parameter forAll :

forall {A prop : Type} `{Checkable prop} `{Show A}

(gen : G A) (pf : A -> prop), Checker.

forall {A prop : Type} `{Checkable prop} `{Show A}

(gen : G A) (pf : A -> prop), Checker.

A variant of forAll that provides evidence that the generated
values are members of the semantics of the generator. (Such evidence
can be useful when constructing dependently typed data, such as
bounded integers.)

Parameter forAllProof :

forall {A prop : Type} `{Checkable prop} `{Show A}

(gen : G A) (pf : forall (x : A), semGen gen x -> prop), Checker.

forall {A prop : Type} `{Checkable prop} `{Show A}

(gen : G A) (pf : forall (x : A), semGen gen x -> prop), Checker.

Parameter forAllShrink :

forall {A prop : Type} `{Checkable prop} `{Show A}

(gen : G A) (shrinker : A -> list A) (pf : A -> prop), Checker.

forall {A prop : Type} `{Checkable prop} `{Show A}

(gen : G A) (shrinker : A -> list A) (pf : A -> prop), Checker.

Lift (Show, Gen, Shrink) instances for A
to a Checker for functions A -> prop. This is what makes it
possible to write (for some example property foo := fun x => x >?
0, say) QuickChick foo instead of QuickChick (forAllShrink
arbitrary shrink foo).

Declare Instance testFun :

forall {A prop : Type} `{Show A} `{Arbitrary A} `{Checkable prop},

Checkable (A -> prop).

forall {A prop : Type} `{Show A} `{Arbitrary A} `{Checkable prop},

Checkable (A -> prop).

Lift products similarly.

Declare Instance testProd :

forall {A : Type} {prop : A -> Type} `{Show A} `{Arbitrary A}

`{forall x : A, Checkable (prop x)},

Checkable (forall (x : A), prop x).

forall {A : Type} {prop : A -> Type} `{Show A} `{Arbitrary A}

`{forall x : A, Checkable (prop x)},

Checkable (forall (x : A), prop x).

Lift polymorphic functions by instantiating to 'nat'. :-)

Declare Instance testPolyFun :

forall {prop : Type -> Type} `{Checkable (prop nat)},

Checkable (forall T, prop T).

forall {prop : Type -> Type} `{Checkable (prop nat)},

Checkable (forall T, prop T).

Record an expectation that a property should fail, i.e.
the property will fail if all the tests succeed.

Collect statistics across all tests.

Set the reason for failure. Will only count shrinks as valid if
they preserve the tag.

Form the conjunction / disjunction of a list of checkers.

Parameter conjoin : forall (l : list Checker), Checker.

Parameter disjoin : forall (l : list Checker), Checker.

Parameter disjoin : forall (l : list Checker), Checker.

Define a checker for a conditional property. Invalid generated
inputs (ones for which the antecedent fails) are discarded.

Notation for implication. Clashes with many other notations in
other libraries, so it lives in its own module. Note that this
includes the notations for the generator combinators above
to avoid needing to import two modules.

Module QcNotation.

Export QcDefaultNotation.

Notation "x ==> y" :=

(implication x y) (at level 55, right associativity)

: Checker_scope.

End QcNotation.

Export QcDefaultNotation.

Notation "x ==> y" :=

(implication x y) (at level 55, right associativity)

: Checker_scope.

End QcNotation.

## The Dec Typeclass

Decidability typeclass using ssreflect's 'decidable'.
Logic Combinator instances.

Declare Instance Dec_neg {P} {H : Dec P} : Dec (~ P).

Declare Instance Dec_conj {P Q} {H : Dec P} {I : Dec Q} : Dec (P /\ Q).

Declare Instance Dec_disj {P Q} {H : Dec P} {I : Dec Q} : Dec (P \/ Q).

Declare Instance Dec_conj {P Q} {H : Dec P} {I : Dec Q} : Dec (P /\ Q).

Declare Instance Dec_disj {P Q} {H : Dec P} {I : Dec Q} : Dec (P \/ Q).

A convenient notation for coercing a decidable proposition to a bool.

## The Dec_Eq Typeclass

Since deciding equalities is a very common requirement in testing,
QuickChick provides a tactic that can define instances of the form
Dec (x = y).
Ltac dec_eq.
QuickChick also lifts common decidable instances to the Dec typeclass.

Declare Instance Dec_eq_bool (x y : bool) : Dec (x = y).

Declare Instance Dec_eq_nat (m n : nat) : Dec (m = n).

Declare Instance Dec_eq_opt (A : Type) (m n : option A)

`{_ : forall (x y : A), Dec (x = y)} : Dec (m = n).

Declare Instance Dec_eq_prod (A B : Type) (m n : A * B)

`{_ : forall (x y : A), Dec (x = y)}

`{_ : forall (x y : B), Dec (x = y)}

: Dec (m = n).

Declare Instance Dec_eq_list (A : Type) (m n : list A)

`{_ : forall (x y : A), Dec (x = y)} : Dec (m = n).

Declare Instance Dec_ascii (m n : Ascii.ascii) : Dec (m = n).

Declare Instance Dec_string (m n : string) : Dec (m = n).

Declare Instance Dec_eq_nat (m n : nat) : Dec (m = n).

Declare Instance Dec_eq_opt (A : Type) (m n : option A)

`{_ : forall (x y : A), Dec (x = y)} : Dec (m = n).

Declare Instance Dec_eq_prod (A B : Type) (m n : A * B)

`{_ : forall (x y : A), Dec (x = y)}

`{_ : forall (x y : B), Dec (x = y)}

: Dec (m = n).

Declare Instance Dec_eq_list (A : Type) (m n : list A)

`{_ : forall (x y : A), Dec (x = y)} : Dec (m = n).

Declare Instance Dec_ascii (m n : Ascii.ascii) : Dec (m = n).

Declare Instance Dec_string (m n : string) : Dec (m = n).

# Automatic Instance Derivation

- A paper on deriving QuickChick generators for a large class of
inductive relations.
http://www.cis.upenn.edu/~llamp/pdf/GeneratingGoodGenerators.pdf
- Leo's PhD dissertation.
https://lemonidas.github.io/pdf/Leo-PhD-Thesis.pdf
- examples/DependentTest.v

# Top-level Commands and Settings

Record Args :=

MkArgs

{

replay : option (RandomSeed * nat);

maxSuccess : nat;

maxDiscard : nat;

maxShrinks : nat;

maxSize : nat;

chatty : bool

}.

MkArgs

{

replay : option (RandomSeed * nat);

maxSuccess : nat;

maxDiscard : nat;

maxShrinks : nat;

maxSize : nat;

chatty : bool

}.

Instead of record updates, you should overwrite extraction constants.
Extract Constant defNumTests => "10000".
Extract Constant defNumDiscards => "(2 * defNumTests)".
Extract Constant defNumShrinks => "1000".
Extract Constant defSize => "7".

# The quickChick Command-Line Tool

- Batch processing, compilation and execution of tests
- Mutation testing
- Sectioning of tests and mutants

## Test Annotations

## Mutant Annotations

## Section Annotations

## Command-Line Tool Flags

- -s <section>: Specify which sections properties and mutants to test
- -v: Verbose mode for debugging
- -failfast: Stop as soon as a problem is detected
- -color: Use colors on an ANSI-compatible terminal
- -cmd <command>: What compile command is used to compile the current directory if it is not make
- -top <name>: Specify the name of the top-level logical module. That should be the same as the -Q or -R directive in _CoqProject or Top which is the default
- -ocamlbuild <args>: Any arguments necessary to pass to ocamlbuild when compiling the extracted code (e.g. linked libraries)
- -nobase: Pass this option to not test the base mutant
- -m <number>: Pass this to only test a mutant with a specific id number
- -tag <name>: Pass this to only test a mutant with a specific tag
- -include <name>: Specify a to include in the compilation
- -exclude <names>: Specify files to be excluded from compilation. Must be the last argument passed.

# Deprecated Features

Module QcDoNotation.

Notation "'do!' X <- A ; B" :=

(bindGen A (fun X => B))

(at level 200, X ident, A at level 100, B at level 200).

Notation "'do\'' X <- A ; B" :=

(bindGen' A (fun X H => B))

(at level 200, X ident, A at level 100, B at level 200).

Notation "'doM!' X <- A ; B" :=

(bindGenOpt A (fun X => B))

(at level 200, X ident, A at level 100, B at level 200).

End QcDoNotation.

End QuickChickSig.

Notation "'do!' X <- A ; B" :=

(bindGen A (fun X => B))

(at level 200, X ident, A at level 100, B at level 200).

Notation "'do\'' X <- A ; B" :=

(bindGen' A (fun X H => B))

(at level 200, X ident, A at level 100, B at level 200).

Notation "'doM!' X <- A ; B" :=

(bindGenOpt A (fun X => B))

(at level 200, X ident, A at level 100, B at level 200).

End QcDoNotation.

End QuickChickSig.