Property-based testing (PBT) frameworks come with a number of different features, but which library supports which features? For a PBT newcomer, it can be hard to tell. Strictly speaking you don't even need a PBT framework. Property-based tests can be written from scratch on a case-by-case basis using a random number generator. One can even test stateful code without a state-machine framework, e.g., as outlined here. However a framework provides reusable parts and infrastructure, thus paving the way for bigger developments, such as property-based testing automotive software against the AUTOSAR specification.
- When finding a counterexample shrinking is nice to get to the essence of an issue
- To test an imperative API a framework with state machine support would be nice.
- Integrated shrinking can be a nice feature for bigger developments where writing custom shrinkers may be out of the question.
- ...
This overview is to help myself keep track. It has been compiled over a number of years teaching PBT. As features are gradually added to a framework the table's entries may unfortunately become outdated. YMMV.
I'll be happy to accept PRs for updating entries and adding new frameworks.
| Framework | Language | Gen. EDSL | Shrinking | Int. shr. | State machine | Par. st. mach. | Cov. guidance |
|---|---|---|---|---|---|---|---|
| theft | C | ( ✔️ ) | ✔️ | ( ✔️ ) | ( ✔️ ) | ||
| DeepState | C / C++ | ( ✔️ ) | ✔️ | ✔️ | ✔️ | ||
| RapidCheck | C++ | ✔️ | ✔️ | ✔️ | ( ✔️ ) | ||
| CsCheck | C# / .Net | ✔️ | ✔️ | ✔️ | ✔️ | ✔️ | |
| test.check | Clojure | ✔️ | ✔️ | ✔️ | ? | ? | |
| check-it | Common Lisp | ✔️ | ✔️ | ||||
| cl-quickcheck | Common Lisp | ✔️ | |||||
| QuickChick | Coq / Rocq | ✔️ | ✔️ | ✔️ | |||
| PropCheck | Elixir | ✔️ | ✔️ | ✔️ | ✔️ | ✔️ | |
| StreamData | Elixir | ✔️ | ✔️ | ✔️ | |||
| elm test | Elm | ✔️ | ✔️ | ✔️ | |||
| propcheck | Emacs Lisp | ✔️ | ✔️ | ✔️ | |||
| QuickCheck | Erlang | ✔️ | ✔️ | ✔️ | ✔️ | ✔️ | |
| PropEr | Erlang | ✔️ | ✔️ | ✔️ | ✔️ | ✔️ | |
| FsCheck | F# / .Net | ✔️ | ✔️ | ✔️ | |||
| FSharp-Hedgehog | F# / .Net | ✔️ | ✔️ | ✔️ | |||
| gopter | Go | ✔️ | ✔️ | ✔️ | |||
| Rapid | Go | ✔️ | ✔️ | ✔️ | ✔️ | ||
| QuickCheck | Haskell | ✔️ | ✔️ | ( ✔️ ) | ( ✔️ ) | ||
| SmallCheck | Haskell | ✔️ | 1 | 1 | |||
| Hedgehog | Haskell | ✔️ | ✔️ | ✔️ | ✔️ | ✔️ | |
| Americium | Java / Scala | ✔️ | ✔️ | ✔️ | |||
| junit-quickcheck | Java | ✔️ | ✔️ | ( ✔️ )2 | |||
| QuickTheories | Java | ✔️ | ✔️ | ✔️ | ( ✔️ ) | ( ✔️ ) | ✔️ |
| jqwik | Java | ✔️ | ✔️ | ✔️ | ✔️ | ||
| fast-check | JS / TS | ✔️ | ✔️ | ✔️ | ✔️ | ( ✔️ )3 | |
| propCheck | Kotlin | ✔️ | ✔️ | ✔️ | ✔️ | ✔️ | |
| Lua-QuickCheck | Lua | ✔️ | ✔️ | ✔️ | ✔️ | ||
| Fox | Obj.C / Swift | ✔️ | ✔️ | ✔️ | ✔️ | ( ✔️ ) | |
| QCheck | OCaml | ✔️ | ✔️ | ✔️4 | ✔️ | ✔️ | |
| Crowbar | OCaml | ✔️ | ( ✔️ )5 | ✔️ | |||
| Monolith | OCaml | ✔️ | ( ✔️ )5 | ✔️ | |||
| Base_quickcheck | OCaml | ✔️ | ✔️ | ||||
| Popper | OCaml | ✔️ | ✔️ | ✔️ | |||
| quickcheck | Prolog | ✔️ | ✔️ | ||||
| Hypothesis | Python | ✔️ | ✔️ | ✔️ | ✔️ | ( ✔️ )3 | ( ✔️ ), ( ✔️ ) |
| TSTL | Python | 6 | ✔️ | ✔️ | ✔️ | ✔️ | |
| R-Hedgehog | R | ✔️ | ✔️ | ✔️ | ✔️ | ||
| racket-quickcheck | Racket | ✔️ | |||||
| PropCheck | Ruby | ✔️ | ✔️ | ✔️ | |||
| PBT | Ruby | ✔️ | ✔️ | ||||
| Rantly | Ruby | ✔️ | ✔️ | ||||
| quickcheck | Rust | ✔️ | ✔️ | ||||
| propcheck | Rust | ✔️ | ✔️ | ✔️ | |||
| Scala-Hedgehog | Scala / JVM | ✔️ | ✔️ | ✔️ | ✔️ | ✔️ | |
| ScalaCheck | Scala / JVM | ✔️ | ✔️ | ✔️ | ✔️ | ||
| scalaprops | Scala / JVM | ✔️ | ✔️ | ||||
| Echidna | Solidity / EVM | ✔️ | ✔️ | ✔️ | ✔️ | ||
| qcheck | Standard ML | ✔️ | ✔️ | ||||
| SwiftCheck | Swift | ✔️ | ✔️ | ||||
| ... |
Legend:
- Language denotes the frameworks's language or platform
- Generator EDSL denotes whether the framework has an expressive, embedded domain-specific language for programming custom generators (
int,list,map, ...) - Shrinking denotes whether the framework has built-in support for reducing counterexamples.
- Integrated shrinking denotes whether a shrinker automatically preserves any invariants of an EDSL-based custom generator (sorted lists, non-empty array, valid JSON, ...)
- State machine denotes whether the framework has a state-machine library for model-based testing.
- Parallel state machine denotes whether the framework supports parallel state-machine testing for race conditons, etc.
- Coverage guidance denotes whether the framework's generators (and shrinkers) can be guided by code coverage information obtained via instrumentation.
Footnotes
- 1 Contrary to QuickCheck and its descendants, SmallCheck's generators enumerate values starting from the smallest ones (up to some bound). SmallCheck will therefore encounter a minimal counterexample first and hence doesn't require shrinking.
- 2 JQF and the underlying Zest supports multiple forms feedback guidance beyond coverage.
- 3 Hypothesis and fast-check support asynchronous state machine testing, which can find race conditions (although it is strictly speaking not using parallel testing).
- 4 QCheck supports integrated shrinking in the generators from the QCheck2 module, whereas the original QCheck module does not.
- 5 Crowbar and Monolith both use AFL which trims each test input as part of its core genetic algorithm. In addition they support test case reduction via
afl-tminwhich is unaware of (and hence may break) OCaml typing. - 6 TSTL instead uses an external DSL.
The term property-based testing seems to originate from 'Towards a Property-based Testing Environment with Applications to Security-Critical Software' by Fink, Ko, Archer, and Levitt (Irvine Software Symposium, 1994). It was later the topic of Fink's 1995 UC Davis PhD dissertation 'Discovering security and safety flaws using property-based testing' and the paper 'Property-Based Testing; A New Approach to Testing for Assurance' by Fink and Bishop (SE Notes 1997). The approach was popularized as an embedded domain-specific language in 'QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs' by Claessen and Hughes (ICFP 2000) which inspired ports to many other languages.
Integrated shrinking is explained in more detail in
- an early design thread on the Haskell mailing list
- a Reddit thread announcing Hedgehog
- a talk by Jacob Stanley on Hedgehog's design
- a blog post by Edsko de Vries with pro/cons
- McIver's Hypothesis article advocating the approach
- 'Test-Case Reduction via Test-Case Generation: Insights From the Hypothesis Reducer' by MacIver and Donaldson (ECOOP 2020)
- Everything You Ever Wanted to Know About Test-Case Reduction, But Didn’t Know to Ask - describing DeepState's reducer/shrinker
State machines to test protocols and systems with state are described in
- 'Testing reactive systems with GAST' by Koopman and Plasmeijer (TFP 2003, revised 2005) - which describes a model-based framework for Clean's Gast library
- 'Testing Telecoms Software with Quviq QuickCheck' Arts, Hughes, and Johansson (Erlang 2006) - which describes Erlang's first
eqc_commandsmodule - 'QuickCheck Testing for Fun and Profit' by Hughes (PADL 2007) describes a later revision
- the API documentation of Quviq's latest (commercial) version
- 'A Note on State-Machine Frameworks for Property-Based Testing' - a tutorial which reconstructs
qcstmfor OCaml
Parallel state-machine tests for race conditions were later introduced in
- 'QuickCheck Testing for Fun and Profit' by Hughes (PADL 2007) - Sec.8 mentions running 2 parallel command sequences and a property searching for an interleaving
- 'Finding Race Conditions in Erlang with QuickCheck and PULSE' by Claessen et al. (ICFP 2009) -- along with a scheduler and a process visualizer
- 'Testing a Database for Race Conditions with QuickCheck' by Hughes and Bolinder (Erlang 2011)