# Property-based testing

Property-based testing checks a *property* the author writes against
inputs the framework generates to try to falsify it. The property is a
claim that should hold for all valid inputs. When a counterexample is
found, the framework *shrinks* it to the minimal failing case. One
property assertion ranges over infinitely many inputs — though any
single run samples only a bounded number of them.

Property-based testing is the structural counterpoint to
[example-based testing](https://quality.stereobooster.com/example-tests.md): the test does not depend on
the author having imagined the specific failing input.

## What it catches

- **Edge cases the author didn't enumerate.** Empty inputs, single
  elements, maximum integer, negative zero, Unicode boundaries.
- **Algorithmic violations.** *sort(x) doesn't return a sorted
  permutation of x*. Caught by a single property regardless of
  input.
- **State-machine bugs.** With *stateful* PBT, the framework
  generates sequences of operations and finds the shortest
  sequence that violates an invariant.
- **Concurrency bugs.** Quviq QuickCheck caught race conditions
  in Erlang `dets` (Hughes 2016)[^hughes2016].
- **Round-trip bugs.** `decode(encode(x)) == x` covers an entire
  serialization surface in one assertion.

It does not catch a bug the property itself misses. Generating more
inputs tests the property as written, not the specification behind it,
so a wrong property passes every run — the oracle problem.

## Tools

- **Python:** [Hypothesis](https://hypothesis.readthedocs.io/). Introduced the
  stateful-shrinking and strategies model that most later PBT
  frameworks adopted.
- **TypeScript / JavaScript:** [fast-check](https://fast-check.dev/). Integrates with
  [Jest](https://jestjs.io/), [Vitest](https://vitest.dev/), [Mocha](https://mochajs.org/).
- **Rust:** [proptest](https://github.com/proptest-rs/proptest), quickcheck. proptest is more idiomatic.
- **Haskell:** [QuickCheck](https://hackage.haskell.org/package/QuickCheck) (the original; (Claessen and Hughes 2000)[^claessen2000]).
- **Erlang / Elixir:** Quviq QuickCheck (commercial), [PropEr](https://proper-testing.github.io/) (free).
- **Java / Kotlin:** [jqwik](https://jqwik.net/), junit-quickcheck.
- **C++:** [RapidCheck](https://github.com/emil-e/rapidcheck).
- **Go:** gopter, testing/quick (standard library, limited).
- **C#:** [FsCheck](https://fscheck.github.io/FsCheck/).

## Bounded-exhaustive enumeration

Random generation samples the input space; *bounded-exhaustive*
generation enumerates it completely up to a size or depth bound. The
same property is the oracle, but instead of trying *n* random values
the framework tries *every* value with up to *k* constructors, list
elements, or recursion levels. Within that bound the result is no
longer "the cases tried passed" but "no case up to size *k* fails" —
the guarantee climbs from Empirical to Exhaustive, paid for by a
search space that grows sharply with *k*.

- [SmallCheck](https://hackage.haskell.org/package/smallcheck) enumerates Haskell values by depth;
  [Lazy SmallCheck](https://hackage.haskell.org/package/lazysmallcheck) prunes whole sub-spaces a
  partially-evaluated property never forces, reaching deeper bounds.
- [Korat](https://korat.sourceforge.net/) enumerates all non-isomorphic structures that
  satisfy a `repOk` class invariant up to a bound, driving
  bounded-exhaustive testing of linked data structures.

The bound must be small enough to enumerate and large enough that the
[small-scope hypothesis](https://quality.stereobooster.com/exhaustive-coverage.md) — most
faults surface on small inputs — does the work. Beyond the bound the
method claims nothing, which is why it complements rather than
replaces random generation.

## When to use, when not

**Use:**

- Pure logic with clearly statable properties (round-trip,
  idempotence, ordering, monotonicity, conservation).
- Parsers and serializers — round-trip is a free oracle.
- Data structures — invariants over operation sequences.
- Protocols — stateful PBT models the protocol; Quviq has done
  this for AUTOSAR, Riak, `dets` and ZeroMQ.

**Don't:**

- When the property is hard to state. *"It should look right to
  the user"* is not a property. Use example tests there.
- When inputs cannot be generated — driving a real UI, or
  exercising live third-party APIs.
- As your *only* method. PBT properties can be wrong; complement
  with example tests for known cases.

## Evidence

- **The Quviq industrial studies** raised 200+ issues in the Volvo
  AUTOSAR program, and surfaced Erlang `dets` race conditions that six
  weeks of manual bug-hunting had missed (Hughes 2016)[^hughes2016]. The
  vendor-quoted 5–8× effort-reduction multiplier is unverified.
- **Hypothesis** documented bug finds in numpy, astropy, and
  Mercurial despite their mature test suites
  (MacIver and Donaldson 2019)[^maciver2019].

## Related

**Exhaustive enumeration of a bounded input space, compressed several ways**

These methods all exhaustively enumerate a bounded input space; each compresses
the exponential blow-up a different way. [Decision
tables](https://quality.stereobooster.com/decision-tables.md) compress *losslessly*: a "don't-care"
entry folds together combinations that share an outcome, so every case still
maps to one rule, and the row carries its own expected decision. [Combinatorial
and pairwise testing](https://quality.stereobooster.com/combinatorial-testing.md) *sample*: a
covering array keeps every *t*-way interaction and drops the higher-order ones,
with the oracle supplied separately. Bounded-exhaustive property
testing *bounds the size*: it
enumerates every value up to a depth/size *k* (SmallCheck), relying on the
small-scope hypothesis that faults surface small. [Exhaustive
coverage](https://quality.stereobooster.com/exhaustive-coverage.md) runs from MCC (the full 2ⁿ
truth table) down to MC/DC's *n*+1 independence criterion, and audits an
existing suite rather than generating one. Type systems reach the same
completeness by construction: an exhaustiveness check on a `match` / `switch`
over a sum type has the compiler verify every variant is handled, with no case
written by hand. State-, path-, and schedule-space
enumerators such as model checking, symbolic execution, and systematic
concurrency testing share the idea over a different space; see the reachability
clusters.

**Generative testing**

These methods blur together because they all run the code and check the result
without a hand-written expected value. Two roles pull them apart, and a single test
picks one of each.

**Input generators** choose the input, and differ by the steering signal (the
Generative subtree of the [input axis](https://quality.stereobooster.com/input.md)):

- Random: property-based testing samples
  from a generator or schema.
- Coverage feedback: [fuzzing](https://quality.stereobooster.com/fuzzing.md) mutates inputs steered by
  coverage (raw bytes); [automated test generation](https://quality.stereobooster.com/automated-test-generation.md)
  runs the same feedback loop as a fitness-guided search over structured call sequences.
- Solver: [symbolic execution](https://quality.stereobooster.com/symbolic-execution.md) derives an input
  that reaches a chosen path.
- Systematic: [combinatorial testing](https://quality.stereobooster.com/combinatorial-testing.md) builds a
  covering array over every t-way combination.

**Oracle suppliers** provide the verdict when no expected value is written:

- [Metamorphic testing](https://quality.stereobooster.com/metamorphic-testing.md) checks a relation between
  the outputs of two related inputs.
- [Differential testing](https://quality.stereobooster.com/differential-testing.md) compares against a
  trusted second implementation.

Pick one generator and one oracle: they compose. A coverage-guided fuzzer that checks a
metamorphic relation is fuzzing and metamorphic at once. (The written-answer end, where
the author picks rows and answers by hand, is [example / parameterized
tests](https://quality.stereobooster.com/example-tests.md).)

**Oracle: predicate**

All four answer the same question — *does property P hold?* — and differ only in
how that answer is obtained, from cheapest-and-weakest to strongest:

- [Runtime contracts](https://quality.stereobooster.com/contracts-and-runtime-assertions.md) —
  *check* P during execution, on the inputs you actually run, and crash if it's
  violated.
- Property-based testing — *check* P
  on many generated inputs; empirical, with no guarantee past what was sampled.
- [Refinement & dependent types](https://quality.stereobooster.com/refinement-and-dependent-types.md)
  — *encode* P in the type, so the compiler rejects any program that could
  violate it (sound within what the type can express).
- [Theorem proving](https://quality.stereobooster.com/theorem-proving.md) — *prove* P holds for all
  inputs, ahead of time.

## Classification

- **Quality dimensions:** Functionality, Reliability.
- **Area:** Pure logic, parsers and serializers, data structures, protocols, state machines (with stateful PBT).
- **Guarantee:** Empirical, Exhaustive (bounded-exhaustive).

## Referenced by

- [Quality dimensions](https://quality.stereobooster.com/quality-dimensions.md) · Quality dimensions
- [Effect scope](https://quality.stereobooster.com/effect.md) · The axes
- [The axes](https://quality.stereobooster.com/axes.md) · The axes
- [Automated test generation](https://quality.stereobooster.com/automated-test-generation.md) · Methods
- [Combinatorial and pairwise testing](https://quality.stereobooster.com/combinatorial-testing.md) · Methods
- [Differential testing](https://quality.stereobooster.com/differential-testing.md) · Methods
- [Example tests](https://quality.stereobooster.com/example-tests.md) · Methods
- [Executable specifications](https://quality.stereobooster.com/executable-specifications.md) · Methods
- [Exhaustive coverage (MC/DC, MCC)](https://quality.stereobooster.com/exhaustive-coverage.md) · Methods
- [Formal methods](https://quality.stereobooster.com/formal.md) · Methods
- [Fuzzing](https://quality.stereobooster.com/fuzzing.md) · Methods
- [Microbenchmarking](https://quality.stereobooster.com/microbenchmarking.md) · Methods
- [Model checking](https://quality.stereobooster.com/model-checking.md) · Methods
- [Profiling](https://quality.stereobooster.com/profiling.md) · Methods
- [Refinement and dependent types](https://quality.stereobooster.com/refinement-and-dependent-types.md) · Methods
- [Snapshot and approval testing](https://quality.stereobooster.com/snapshot-testing.md) · Methods
- [State machines and statecharts](https://quality.stereobooster.com/state-machines.md) · Methods
- [Statistical and sampling testing](https://quality.stereobooster.com/statistical-testing.md) · Methods
- [Temporal-logic falsification](https://quality.stereobooster.com/temporal-logic-falsification.md) · Methods
- [Testing machine-learning systems](https://quality.stereobooster.com/testing-ml-systems.md) · Methods
- [Verifying numerical code](https://quality.stereobooster.com/numbers.md) · Methods
- [Verifying time and date handling](https://quality.stereobooster.com/time-and-date.md) · Methods
- [TypeScript](https://quality.stereobooster.com/typescript.md) · Recipes
- [How AI fits into software quality](https://quality.stereobooster.com/ai.md) · AI

## References

[^hughes2016]: Hughes, John. 2016. "[Experiences with QuickCheck: Testing the Hard Stuff and Staying Sane](https://www.cs.tufts.edu/~nr/cs257/archive/john-hughes/quviq-testing.pdf)." In *A List of Successes That Can Change the World*, edited by Sam Lindley, Conor McBride, Phil Trinder, and Don Sannella. Lecture Notes in Computer Science 9600. Springer. [https://doi.org/10.1007/978-3-319-30936-1\\\_9](https://doi.org/10.1007/978-3-319-30936-1\_9).
[^claessen2000]: Claessen, Koen, and John Hughes. 2000. "[QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs](https://www.cs.tufts.edu/~nr/cs257/archive/john-hughes/quick.pdf)." *Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00)*, 268–79. <https://doi.org/10.1145/351240.351266>.
[^maciver2019]: MacIver, David R., and Alastair F. Donaldson. 2019. "[Hypothesis: A New Approach to Property-Based Testing](https://joss.theoj.org/papers/10.21105/joss.01891.pdf)." *Journal of Open Source Software* 4 (43): 1891. <https://doi.org/10.21105/joss.01891>.

## Acronyms

- MC/DC — modified condition/decision coverage
- MCC — multiple-condition coverage
- PBT — property-based testing