README.md

Overview of Property-Based Testing Functionality

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.

• 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 functionality

Framework	Language	Gen. EDSL	Shrinking	Int. shr.	State machine	Par. st. mach.	Cov. guidance
QuickCheck	Erlang	✔️	✔️	✔️	✔️	✔️
PropEr	Erlang	✔️	✔️	✔️	✔️	✔️
QuickCheck	Haskell	✔️	✔️		( ✔️ )	( ✔️ )
SmallCheck	Haskell	✔️	1	1
Hedgehog	Haskell	✔️	✔️	✔️	✔️	✔️
Scala-Hedgehog	Scala / JVM	✔️	✔️	✔️	✔️	✔️
R-Hedgehog	R	✔️	✔️	✔️	✔️
FSharp-Hedgehog	F# / .Net	✔️	✔️	✔️
Hypothesis	Python	✔️	✔️	✔️	✔️	( ✔️ )2	( ✔️ ), ( ✔️ )
TSTL	Python	3	✔️	✔️	✔️		✔️
ScalaCheck	Scala / JVM	✔️	✔️		✔️	✔️
gopter	Go	✔️	✔️		✔️
Rapid	Go	✔️	✔️	✔️	✔️
propCheck	Kotlin	✔️	✔️	✔️	✔️	✔️
FsCheck	F# / .Net	✔️	✔️		✔️
CsCheck	C# / .Net	✔️	✔️	✔️	✔️	✔️
fast-check	JS / TS	✔️	✔️	✔️	✔️	( ✔️ )2
QCheck	OCaml	✔️	✔️	✔️4	✔️	✔️
Crowbar	OCaml	✔️	( ✔️ )5				✔️
Monolith	OCaml	✔️	( ✔️ )5				✔️
Base_quickcheck	OCaml	✔️	✔️
Popper	OCaml	✔️	✔️	✔️
junit-quickcheck	Java	✔️	✔️				( ✔️ )6
QuickTheories	Java	✔️	✔️	✔️	( ✔️ )	( ✔️ )	✔️
jqwik	Java	✔️	✔️	✔️	✔️
quickcheck	Rust	✔️	✔️
propcheck	Rust	✔️	✔️	✔️
Fox	Obj.C / Swift	✔️	✔️	✔️	✔️	( ✔️ )
SwiftCheck	Swift	✔️	✔️
RapidCheck	C++	✔️	✔️		✔️	( ✔️ )
test.check	Clojure	✔️	✔️	✔️	?	?
Lua-QuickCheck	Lua	✔️	✔️	✔️	✔️
theft	C	( ✔️ )	✔️	( ✔️ )			( ✔️ )
DeepState	C / C++	( ✔️ )	✔️	✔️			✔️
Echidna	Solidity / EVM		✔️	✔️	✔️		✔️
...

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

• ¹ 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.
• ² Hypothesis and fast-check support asynchronous state machine testing, which can find race conditions (although it is strictly speaking not using parallel testing).
• ³ TSTL instead uses an external DSL.
• ⁴ QCheck supports integrated shrinking in the generators from the QCheck2 module, whereas the original QCheck module does not.
• ⁵ 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-tmin which is unaware of (and hence may break) OCaml typing.
• ⁶ JQF and the underlying Zest supports multiple forms feedback guidance beyond coverage.

Background:

The term property-based testing seems to originate from '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_commands module
• '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 qcstm for OCaml

Parallel state-machine tests for race conditions were later introduced in

• '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)

Additional resources:

• A shrinking challenge for comparing frameworks
• 'QuickCheck Advice' by Jesper L. Andersen
• A recent course by John Hughes
• My own course material
• ...