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

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.
• ⁴ 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
• ...