Property-Based Conformance Test¶

Test method — instantiates Representation-Independent Interface Contract

Checks a contract by generating many random inputs and asserting the laws that must hold for every one, instead of a handful of hand-picked cases.

Property-Based Conformance Test checks a contract the way a mathematician checks a claim about all numbers: not by trying a few examples, but by asserting a law that must hold for every input and then hammering it with hundreds of generated cases. Instead of "insert 5, then assert the set contains 5," it states "for any element x and any set s, contains(insert(s, x), x) is true," generates x and s at random across thousands of shapes, and reports the first case where the law fails. Its defining move is the universally-quantified property: the test encodes what the contract promises about all behaviour, not what one implementation happens to do on one input — which is exactly why the same suite validates every implementation of the contract without modification.

Example¶

A library ships a Set interface with two implementations — a hash-based one and a balanced-tree one — and wants them interchangeable. Rather than write example tests, the team writes the contract's laws: inserting an element makes it a member; inserting it twice is the same as once (idempotence); size never decreases on insert; union is commutative; an element removed is not a member. Each law becomes a property quantified over randomly generated elements and sets.

Running it, the generator eventually builds a set with two distinct keys that happen to share a hash bucket, inserted in an order the hash implementation mishandles — membership returns false for a key that is present. The framework then shrinks the failing case from a tangle of forty operations down to a two-line minimal reproducer. The bug was real, representation-specific, and invisible to any example a human would have thought to write; the law found it because the law quantified over inputs no human enumerated.

How it works¶

State the contract as laws. Turn each promise into a property that holds for all inputs — round-trips (decode(encode(x)) == x), idempotence, commutativity, invariants preserved across any operation sequence.
Generate and shrink. A generator produces random inputs across the whole domain; on failure the framework shrinks the counterexample to something minimal a human can read.
Assert the representation invariant. Because it can build arbitrary operation sequences, it is uniquely able to check that the internal invariant — a tree stays balanced, a set holds no duplicates — survives every path, not only the ones a person scripts.
Reuse across implementations. The property set is written against the contract, so every conforming implementation runs the identical suite; the properties are the oracle.

Tuning parameters¶

Generator distribution — what inputs are sampled and how often the interesting ones (empty, huge, boundary, adversarial hash-collision) appear. A weak distribution passes vacuously; biasing toward edges is where the bugs live.
Case count and shrinking budget — more generated cases and deeper shrinking raise confidence and sharpen the counterexample, at the cost of test time.
Property strength — how tightly the laws pin behaviour. Loose properties are easy to satisfy and prove little; the dial is set toward the strongest law the contract actually guarantees.
Statefulness — single-call properties versus generated sequences of operations, needed to catch invariant violations that only appear after a particular history.

When it helps, and when it misleads¶

Its strength is coverage no human enumerates: one law stands in for thousands of examples, the same suite certifies every implementation, and generated operation-sequences expose invariant violations that example tests structurally cannot reach. Shrinking then hands you a minimal reproducer instead of a forty-step mess.

The failure modes live in the properties. A tautological property — one that merely restates what the implementation does — is green by construction and proves nothing; the classic misuse is writing the property after watching the code run, so it encodes the behaviour rather than the contract (the law run backwards to bless whatever exists). Weak generators that never reach the interesting region give false confidence: all-green because nothing hard was ever tried. And some contracts have no clean algebraic law to state, where a reference implementation is the more honest oracle. The discipline is to derive the properties from the specification before looking at the code, and to sanity-check the generator by confirming it can kill a deliberately broken implementation.^[1]

How it implements the components¶

Property-Based Conformance Test realises the law-checking side of verification:

law_or_algebraic_axiom_set — the properties it runs are this set, made executable: the round-trips, idempotences, and invariants the contract guarantees.
conformance_oracle — a property decides pass/fail with no hand-written expected output; the law itself is the oracle that says whether behaviour conforms.
representation_invariant — by generating arbitrary operation sequences it verifies the internal invariant survives every history, not just scripted ones.

It does not diff against a trusted second implementation — that oracle is Reference-Implementation Differential Test's — and it does not hunt for behaviour the contract never promised, which is Representation Leakage Probe's job.

Instantiates: Representation-Independent Interface Contract — it turns the contract's promises into executable laws every implementation must pass.
Consumes: a behavioural specification (Abstract Data Type Specification, Design by Contract Clause) supplies the laws it makes executable.
Sibling mechanisms: Reference-Implementation Differential Test is the complementary oracle — a reference implementation instead of a law · Metamorphic Behavior Test · Black-Box Contract Test Suite · Design by Contract Clause · Opaque Type / Module Boundary

References¶

[1] Property-based testing was popularised by QuickCheck (Claessen & Hughes), which generates random inputs and, on failure, shrinks them to a minimal counterexample. The properties stand in for the specification's laws — which is why a property derived from the implementation instead of the specification tests nothing. ↩