Skip to content

Software Quality

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: 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)1.
  • 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. Introduced the stateful-shrinking and strategies model that most later PBT frameworks adopted.
  • TypeScript / JavaScript: fast-check. Integrates with Jest, Vitest, Mocha.
  • Rust: proptest, quickcheck. proptest is more idiomatic.
  • Haskell: QuickCheck (the original; (Claessen and Hughes 2000)2).
  • Erlang / Elixir: Quviq QuickCheck (commercial), PropEr (free).
  • Java / Kotlin: jqwik, junit-quickcheck.
  • C++: RapidCheck.
  • Go: gopter, testing/quick (standard library, limited).
  • C#: 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 enumerates Haskell values by depth; Lazy SmallCheck prunes whole sub-spaces a partially-evaluated property never forces, reaching deeper bounds.
  • Korat 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 — 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)1. 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)3.

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 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 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 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):

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

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

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.)

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 — 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 — encode P in the type, so the compiler rejects any program that could violate it (sound within what the type can express).
  • Theorem proving — 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

References

  1. Hughes, John. 2016. "Experiences with QuickCheck: Testing the Hard Stuff and Staying Sane." 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. ↩↩

  2. Claessen, Koen, and John Hughes. 2000. "QuickCheck: A Lightweight Tool for Random Testing of Haskell Programs." Proceedings of the Fifth ACM SIGPLAN International Conference on Functional Programming (ICFP '00), 268–79. https://doi.org/10.1145/351240.351266. ↩

  3. MacIver, David R., and Alastair F. Donaldson. 2019. "Hypothesis: A New Approach to Property-Based Testing." Journal of Open Source Software 4 (43): 1891. https://doi.org/10.21105/joss.01891. ↩