/QuickChick

Randomized Property-Based Testing Plugin for Coq

Primary LanguageCoqOtherNOASSERTION

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: