Repository files navigation

• Randomized property-based testing plugin for Coq; a clone ofHaskell QuickCheck
• Includes afoundational verification framework for testing code
• Includes amechanism for automatically deriving generators for inductive relations

• Small tutorials on Basic Usage and Automation can be found undertutorials/
• An extended introduction can be found inQuickChick: 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/releasedopam update# Install the coq-quickchick opam packageopam install coq-quickchick

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

Runningmake 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 inQuickChickInterface.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:

• Our PLDI 2022 paper ona mechanism for automatically deriving generators, enumerators, and checkers for inductive relations
• Our POPL 2018 paper ona mechanism for automatically deriving generators for inductive relations
• Our ITP 2015 paper onFoundational Property-Based Testing
• Our PLDI 2023 paper ona mechanism for merging multiple inductive relations into one
• Leo's invited talk at CLA onRandom Testing in the Coq Proof Assistant
• Catalin'sinternship topic proposals for 2015
• Catalin'spresentation at CoqPL 2015 workshop (2015-01-18)
• Zoe'sthesis defense at NTU Athens (2014-09-08)
• Maxime'spresentation at the Coq Workshop (2014-07-18)
• Catalin'spresentation at the Coq Working Group @ PPS (2014-03-19)

Dependencies are listed incoq-quickchick.opam.

# To get the dependencies, add the Coq opam repository if you haven't alreadyopam repo add coq-released https://coq.inria.fr/opam/releasedopam updateopam install . --deps-only

dune build

dune runtest

dune install coq-quickchick  # Makes QuickChick available globallydune build @cram