QuickChick / Quickchick
Licence: other
Randomized Property-Based Testing Plugin for Coq
Stars: ✭ 188
Projects that are alternatives of or similar to Quickchick
Coq Haskell
A library for formalizing Haskell types and functions in Coq
Stars: ✭ 135 (-28.19%)
Mutual labels: coq
Kami
Kami - a DSL for designing Hardware in Coq, and the associated semantics and theorems for proving its correctness. Kami is inspired by Bluespec. It is actually a complete rewrite of an older version from MIT
Stars: ✭ 158 (-15.96%)
Mutual labels: coq
Fiat
Mostly Automated Synthesis of Correct-by-Construction Programs
Stars: ✭ 119 (-36.7%)
Mutual labels: coq
Math Classes
A library of abstract interfaces for mathematical structures in Coq [[email protected]]
Stars: ✭ 133 (-29.26%)
Mutual labels: coq
Bedrock2
A work-in-progress language and compiler for verified low-level programming
Stars: ✭ 138 (-26.6%)
Mutual labels: coq
Coqhammer
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Stars: ✭ 157 (-16.49%)
Mutual labels: coq
Geocoq
A formalization of geometry in Coq based on Tarski's axiom system
Stars: ✭ 128 (-31.91%)
Mutual labels: coq
Interactiontrees
A Library for Representing Recursive and Impure Programs in Coq
Stars: ✭ 133 (-29.26%)
Mutual labels: coq
Vscoq
A Visual Studio Code extension for Coq [[email protected],@fakusb]
Stars: ✭ 138 (-26.6%)
Mutual labels: coq
Awesome Provable
A curated set of links to formal methods involving provable code.
Stars: ✭ 111 (-40.96%)
Mutual labels: coq
Advent Of Coq 2018
Advent of Code 2018, in Coq! (https://adventofcode.com/2018)
Stars: ✭ 137 (-27.13%)
Mutual labels: coq
Jscert
A Coq specification of ECMAScript 5 (JavaScript) with verified reference interpreter
Stars: ✭ 186 (-1.06%)
Mutual labels: coq
Verdi Raft
An implementation of the Raft distributed consensus protocol, verified in Coq using the Verdi framework
Stars: ✭ 143 (-23.94%)
Mutual labels: coq
QuickChick
Description
- 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
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:
- OCaml 4.01.0 and Coq 8.4pl3 or OCaml 4.02.1 and Coq 8.4pl6
- SSReflect 1.5 (http://ssr.msr-inria.inria.fr/FTP/)
- 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:
- DeepSpec QC repo. Pretty soon this will become a software foundations volume!
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)
Note that the project description data, including the texts, logos, images, and/or trademarks,
for each open source project belongs to its rightful owner.
If you wish to add or remove any projects, please contact us at [email protected].