Skip to content

Software Quality

Property-based testing

Property-based testing is testing in which a framework generates inputs that try to falsify a property, a claim the author writes about every valid input. When a counterexample is found, the framework shrinks it to a minimal failing case. One property assertion ranges over infinitely many inputs — though any single run samples only a bounded number of them.

Unlike an example test, a property-based test does not depend on the author having imagined the specific failing input.

What it catches

  • Edge cases the author didn't enumerate. Generators reach empty inputs, single elements, the maximum integer, negative zero and Unicode boundaries without the author listing them.
  • Algorithmic violations. A single property catches sort(x) doesn't return a sorted permutation of x whatever input triggers it.
  • State-machine bugs. With stateful PBT, the framework generates sequences of operations and shrinks one that violates an invariant to a minimal sequence.
  • 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

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 small-scope hypothesis holds that most faults surface on small inputs, so the bound must be large enough to cover those inputs and small enough to enumerate. 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 and dets.

Don't:

  • When the property is hard to state. "It should look right to the user" is not a property, and example tests fit that case.
  • When inputs cannot be generated — driving a real UI, or exercising live third-party APIs.
  • As the only method. PBT properties can be wrong, and example tests pin down the known cases.

Evidence

  • Quviq's industrial experience report records 200+ issues found in the Volvo AUTOSAR program, and Erlang dets race conditions that six weeks of manual bug-hunting had missed (Hughes 2016)1.
  • Hypothesis has found bugs in astropy and numpy (MacIver et al. 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., Zac Hatfield-Dodds, et al. 2019. "Hypothesis: A New Approach to Property-Based Testing." Journal of Open Source Software 4 (43): 1891. https://doi.org/10.21105/joss.01891. ↩