- Randomized property-based testing plugin for Coq; a clone of Haskell QuickCheck
- Includes a foundational verification framework for testing code
- Includes a mechanism for automatically deriving generators for inductive relations
QuickChick: Property-Based Testing in Coq (Software Foundations, Volume 4)
# 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
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
make
# To install the package:
# (proceed with caution: this will clobber your `.opam` directory)
make install
make compat
dune build
examples/Tutorial.vexamples/RedBlackexamples/stlcexamples/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.
The public API of QuickChick is summarized in BasicInterface.v.
QuickCheck cSample gDerive Arbitrary for cDerive Show for cDerive ArbitrarySizedSuchThat for (fun x => p)Derive ArbitrarySizedSuchThat for (fun x => let (x1,x2...) := x in p)QuickCheckWith args cMutateCheck c pMutateCheckWith args c pMutateCheckMany c psMutateCheckManyWith args c ps
Here is some more reading material:
- Our POPL 2018 paper on Generating Good Generators for Inductive Relations
- Our ITP 2015 paper on Foundational Property-Based Testing
- Leo's invited talk at CLA on Random Testing in the Coq Proof Assistant
- Catalin's internship topic proposals for 2015
- Catalin's presentation at CoqPL 2015 workshop (2015-01-18)
- Zoe's thesis defense at NTU Athens (2014-09-08)
- Maxime's presentation at the Coq Workshop (2014-07-18)
- Catalin's presentation at the Coq Working Group @ PPS (2014-03-19)