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.

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

Framework	Language	Gen. EDSL	Shrinking	Int. shr.	State machine	Par. st. mach.	Cov. guidance
theft	C	( :heavy_check_mark: )	:heavy_check_mark:	( :heavy_check_mark: )			( :heavy_check_mark: )
DeepState	C / C++	( :heavy_check_mark: )	:heavy_check_mark:	:heavy_check_mark:			:heavy_check_mark:
RapidCheck	C++	:heavy_check_mark:	:heavy_check_mark:		:heavy_check_mark:	( :heavy_check_mark: )
CsCheck	C# / .Net	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
test.check	Clojure	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	?	?
check-it	Common Lisp	:heavy_check_mark:	:heavy_check_mark:
cl-quickcheck	Common Lisp	:heavy_check_mark:
QuickChick	Coq / Rocq	:heavy_check_mark:	:heavy_check_mark:				:heavy_check_mark:
PropCheck	Elixir	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
StreamData	Elixir	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
elm test	Elm	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
propcheck	Emacs Lisp	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
QuickCheck	Erlang	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
PropEr	Erlang	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
FsCheck	F# / .Net	:heavy_check_mark:	:heavy_check_mark:		:heavy_check_mark:
FSharp-Hedgehog	F# / .Net	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
gopter	Go	:heavy_check_mark:	:heavy_check_mark:		:heavy_check_mark:
Rapid	Go	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
QuickCheck	Haskell	:heavy_check_mark:	:heavy_check_mark:		( :heavy_check_mark: )	( :heavy_check_mark: )
SmallCheck	Haskell	:heavy_check_mark:	1	1
Hedgehog	Haskell	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
Americium	Java / Scala	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
junit-quickcheck	Java	:heavy_check_mark:	:heavy_check_mark:				( :heavy_check_mark: )2
QuickTheories	Java	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	( :heavy_check_mark: )	( :heavy_check_mark: )	:heavy_check_mark:
jqwik	Java	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
fast-check	JS / TS	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	( :heavy_check_mark: )3
propCheck	Kotlin	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
Lua-QuickCheck	Lua	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
Fox	Obj.C / Swift	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	( :heavy_check_mark: )
QCheck	OCaml	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:4	:heavy_check_mark:	:heavy_check_mark:
Crowbar	OCaml	:heavy_check_mark:	( :heavy_check_mark: )5				:heavy_check_mark:
Monolith	OCaml	:heavy_check_mark:	( :heavy_check_mark: )5				:heavy_check_mark:
Base_quickcheck	OCaml	:heavy_check_mark:	:heavy_check_mark:
Popper	OCaml	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
quickcheck	Prolog	:heavy_check_mark:	:heavy_check_mark:
Hypothesis	Python	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	( :heavy_check_mark: )3	( :heavy_check_mark: ), ( :heavy_check_mark: )
TSTL	Python	6	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:		:heavy_check_mark:
R-Hedgehog	R	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
racket-quickcheck	Racket	:heavy_check_mark:
PropCheck	Ruby	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
PBT	Ruby	:heavy_check_mark:	:heavy_check_mark:
Rantly	Ruby	:heavy_check_mark:	:heavy_check_mark:
quickcheck	Rust	:heavy_check_mark:	:heavy_check_mark:
proptest	Rust	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
Scala-Hedgehog	Scala / JVM	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:
ScalaCheck	Scala / JVM	:heavy_check_mark:	:heavy_check_mark:		:heavy_check_mark:	:heavy_check_mark:
scalaprops	Scala / JVM	:heavy_check_mark:	:heavy_check_mark:
Echidna	Solidity / EVM		:heavy_check_mark:	:heavy_check_mark:	:heavy_check_mark:		:heavy_check_mark:
qcheck	Standard ML	:heavy_check_mark:	:heavy_check_mark:
SwiftCheck	Swift	:heavy_check_mark:	:heavy_check_mark:
...

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.
• ² JQF and the underlying Zest supports multiple forms feedback guidance beyond coverage.
• ³ Hypothesis and fast-check support asynchronous state machine testing, which can find race conditions (although it is strictly speaking not using parallel testing).
• ⁴ 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.
• ⁶ TSTL instead uses an external DSL.

Background:

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, Johansson, and Wiger (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

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

Additional resources:

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