Randomized Property-Based Testing Plugin for Coq
Branch: 8.9
Clone or download

README.md

QuickChick

Build Status

Description

For more information on QuickChick, look at the tutorial available under the qc folder of the deep spec summer school: https://github.com/DeepSpec/dsss17

Current release dependencies:

  • Branch master:
    • Coq 8.8
    • OCaml >= 4.04.0
    • mathcomp-ssreflect-1.6.4
    • coq-ext-lib-0.9.7
    • coq-simple-io-0.2

Installation

From OPAM

# Add the Coq opam repository (if you haven't already)
opam repo add coq-released https://coq.inria.fr/opam/released
opam update
# Install the coq-quickchick opam package
opam install coq-quickchick

From source

# To get the dependencies, you still need to add the Coq opam repository (if you haven't already)
opam repo add coq-released https://coq.inria.fr/opam/released
opam update
opam install coq-mathcomp-ssreflect coq-ext-lib coq-simple-io

# Then:
make && make install

Simple Examples

  • examples/Tutorial.v
  • examples/RedBlack
  • examples/stlc
  • examples/ifc-basic

Running make tests in the top-level QuickChick folder will check and execute all of these. If successful, you should see "success" at the end.

Top-level Commands

  • QuickCheck c
  • Sample g
  • Derive Arbitrary for c
  • Derive Show for c
  • Derive ArbitrarySizedSuchThat for (fun x => p)
  • Derive ArbitrarySizedSuchThat for (fun x => let (x1,x2...) := x in p)
  • QuickCheckWith args c
  • MutateCheck c p
  • MutateCheckWith args c p
  • MutateCheckMany c ps
  • MutateCheckManyWith args c ps

Other tags

  • coq 8.4pl6:
  • coq 8.5-*:
    • Coq 8.5pl2
    • OCaml 4.03.0
    • mathcomp-ssreflect v1.5
    • 8.5-legacy contains the old typeclass hierarchy
    • 8.5-automation contains the new one
  • coq 8.6:
    • Coq 8.6
    • OCaml 4.03.0
    • mathcomp-ssreflect-1.6.1

Documentation

The public API of QuickChick is summarized in BasicInterface.v.

The main documentation is the DeepSpec summer school tutorial:

Here is some more reading material: