/QuickChick

Randomized Property-Based Testing Plugin for Coq

Primary LanguageCoqOtherNOASSERTION

QuickChick CircleCI

Description

Tutorial

QuickChick: Property-Based Testing in Coq (Software Foundations, Volume 4)

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

Dependencies are listed in coq-quickchick.opam.

# To get the dependencies, 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 --deps-only

Build using Make

make

# To install the package:
# (proceed with caution: this will clobber your `.opam` directory)
make install

Build using Dune

make compat
dune build

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.

Documentation

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

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

More resources

Here is some more reading material: