Property-Based Equivalence Test¶
Generative equivalence test — instantiates Equivalence-Preserving Rewrite Optimization
Machine-generates a large input space, runs the original and rewritten forms side by side against declared properties, and shrinks any disagreement to a minimal counterexample.
Where a golden test compares against a frozen recording and a metamorphic suite checks relations when no reference exists, the Property-Based Equivalence Test does something else: it generates the inputs. You declare the properties a correct rewrite must satisfy — most powerfully, "the rewritten form agrees with the original" — and the tool manufactures hundreds or thousands of varied, deliberately nasty inputs, runs both forms on each, and checks the property every time. Its defining move, which no sibling shares, is shrinking: when it finds an input on which the two forms disagree, it automatically reduces that input to the smallest version that still fails, handing you a minimal counterexample instead of a haystack. It turns "I think these are equivalent" into a broad, self-searching interrogation that keeps trying to break the claim.
Example¶
A team rewrites the hot serialize() routine in a messaging library for speed, keeping the old one alongside. They write two properties. Differential: for any message m, deserialize(fast_serialize(m)) equals deserialize(slow_serialize(m)). Round-trip: for any m, deserialize(fast_serialize(m)) == m. Then the generator takes over, producing messages across the whole shape of the type — empty strings, deeply nested maps, negative and boundary integers, non-ASCII text, absurd field counts.
Thousands pass. Then the differential property fails on some large, random record. Left as-is that record is unreadable — but shrinking kicks in, repeatedly simplifying it while the failure persists, and lands on the minimal case: a single map field whose key is the empty string. The fast path packed empty keys one byte short. The bug was never in a corpus a human would have hand-written; the generator found it, and shrinking pointed straight at it.
How it works¶
You specify properties, not examples — executable predicates any behaviour-preserving rewrite must satisfy, chiefly that old and new agree, plus structural invariants like round-tripping. A generator then samples the input space (guided by the inputs' types and by tunable distributions), runs both forms, and checks every property on each case. Two things set it apart from the recording- and relation-based oracles. First, it supplies its own oracle by running the trusted original beside the rewrite, so no frozen reference is needed. Second, on failure it shrinks — searching down from the failing input to a locally-minimal one that still violates the property — so debugging starts from the simplest possible witness. What it can never do is prove equivalence: it samples, so it shows the presence of a difference, never its absence.
Tuning parameters¶
- Property strength — how tightly the declared properties pin things down. Full old-versus-new equality is the strongest; weaker invariants (round-trip, ordering) catch less but apply where no reference form exists.
- Generator distribution — which inputs get sampled, and how far the odds are skewed toward edge cases (empty, boundary, adversarial). Bias toward the nasty regions and you find bugs faster; over-bias and you miss the ordinary middle.
- Case count / effort — how many inputs per run. More widens coverage of a vast space at linear time cost.
- Shrinking aggressiveness — how hard the tool works to minimise a failing case. Better shrinking yields a cleaner counterexample but spends time once a failure is found.
- Seed / reproducibility — whether runs replay from a fixed seed. Fixing it makes a failure reproducible; varying it explores more of the space over time.
When it helps, and when it misleads¶
Its strength is that it explores inputs no one would hand-write, and having found a failure, shrinking makes it actionable — a minimal counterexample rather than a giant random blob. Because it runs the original as its own oracle, it needs neither a captured golden set nor a cleverly-devised relation; declaring "the two agree" is often enough, which makes it the natural check of a rewrite against the very code it replaced.
Its failure modes follow from sampling. A green run is evidence, not proof — testing shows the presence of differences, not their absence,[1] and a rare input the generator never drew can still differ. Coverage is only as good as the generator: if the distribution never reaches the regime where the rewrite breaks (a specific Unicode category, a huge allocation), the bug hides. It also needs the property stated correctly — a wrong property fails good rewrites or, worse, passes broken ones. The classic misuse is running a thin generator briefly and treating the pass as certification. The discipline: make old-versus-new agreement the core property, skew the generator toward the edges, run enough cases, and pair it with an exact oracle where one exists.
How it implements the components¶
Property-Based Equivalence Test fills the checking components a generative oracle owns:
equivalence_relation_contract— the declared properties are the contract made executable: they state, as checkable predicates, exactly what "equivalent" must mean for this rewrite (old equals new; the round-trip holds).invariant_preservation_oracle— running both forms across a generated input space and checking those predicates is the oracle; a single failing case is proof the rewrite changed behaviour.
It does not compare against a frozen recorded corpus with masked incidental fields (Golden-Output Regression Test), does not assert metamorphic relations or a side-effect register when no reference form exists (Metamorphic Test Suite), and does not measure whether the rewrite is faster (Benchmark Harness).
Related¶
- Instantiates: Equivalence-Preserving Rewrite Optimization — it is the generative oracle that hunts for a behaviour difference between the two forms.
- Sibling mechanisms: Golden-Output Regression Test · Metamorphic Test Suite · Benchmark Harness · Compiler Optimization Pass · Peephole Optimization
Editorial Notes¶
Form Classification¶
Form family: Experiment, Test & Rehearsal
Rationale: Property-Based Equivalence Test operates as an active test, trial, simulation, drill, or rehearsal that generates evidence through a deliberate attempt or perturbation because it machine-generates a large input space, runs the original and rewritten forms side by side against declared properties, and shrinks any disagreement to a minimal counterexample.
Independent corroboration: The frozen evidence defines Property-Based Equivalence Test as 'Machine-generates a large input space, runs the original and rewritten forms side by side against declared properties, and shrinks any disagreement to a minimal counterexample', so its operative form is Experiment, Test & Rehearsal.
Review outcome: Independent reviewer agreement; high confidence.
Origin Attribution¶
Primary origin: Computer Science & Software Engineering
Origin pattern: Cross-disciplinary synthesis
Present-day reach: Specialized
Rationale: Property-Based Equivalence Test is most plausibly rooted in the computer_science tradition because its characteristic form depends on algorithms, data structures, formal interfaces, and software-system practice. The assignment tracks that formative lineage, not the many settings in which the mechanism can now be applied.
Related originating lineages:
- Mathematics — The mathematics tradition materially shaped Property-Based Equivalence Test through its own practice of formal definition, proof, mapping, and quantitative structure.
Review resolution: Both blind reviewers agree that computer science is the primary origin. Explicit reconciliation resolves encyclopedia synthesis disagreement. Formative alternate lineages are retained as mathematics; later breadth of use is recorded separately as domain_reach=specialized, while origin_mode=cross_disciplinary_synthesis describes the relationship among origin lineages.
Encyclopedia synthesis: The exact catalogued form synthesizes established practice rather than reproducing a single standard historical label.
Review outcome: Reconciled after independent review; high confidence.
Notes¶
The three equivalence-testing siblings form a ladder by how much oracle you have. Use a Golden-Output Regression Test when you can freeze an exact reference; a Property-Based Equivalence Test when you still have the original form to run as a live oracle; a Metamorphic Test Suite when you have neither and can only assert relations. Reaching for the strongest oracle actually available is the discipline that keeps testing honest.
References¶
[1] Dijkstra, E. W. Notes on Structured Programming. 2nd ed., Technische Hogeschool Eindhoven, EUT Report 70-WSK-03 / EWD249 (1970). Explains that testing can reveal bugs but cannot prove their absence because sampling cannot exhaust the enormous input space. registry ↩