Randomized Property-Based Testing Plugin for Coq
tutorials/
# 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
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.
The public API of QuickChick is summarized in QuickChickInterface.v
.
QuickCheck c
Sample g
Derive Arbitrary for c
Derive Show for c
Derive ArbitrarySizedSuchThat for (fun x => p)
Derive DecOpt for p
Derive EnumSizedSuchThat 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
Here is some more reading material:
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
dune build
dune runtest
dune install coq-quickchick # Makes QuickChick available globally
dune build @cram