property-based-testing

Property-Based Testing

An example test asserts one point. A property asserts a rule over the whole input domain and lets the generator hunt for the counterexample. That trade is worth making when the code has an algebraic shape — an inverse, an invariant, an oracle — and not otherwise. Code with no such shape gets example tests; saying so is a valid outcome.

Check first whether the shape is missing or merely buried. A calculation wrapped in I/O, a string built by concatenation, an in-place mutation — each has a property and no seam to assert it through. See references/refactoring.md before concluding there is nothing to assert.

Property catalog

Property	Formula	Where it applies
Roundtrip	decode(encode(x)) == x	Serialization, conversion pairs
Inverse	f(g(x)) == x	encrypt/decrypt, compress/decompress
Oracle	new(x) == reference(x)	Optimization, refactoring, reimplementation
Idempotence	f(f(x)) == f(x)	Normalization, formatting, sorting
Invariant	Holds before and after	Any transformation, contract state
Easy to verify	is_sorted(sort(x))	Complex algorithms with cheap checkers
Commutativity	f(a, b) == f(b, a)	Binary and set operations
Associativity	f(f(a,b), c) == f(a, f(b,c))	Combining operations
Identity	f(x, e) == x	Operations with a neutral element

Strength ordering, weakest to strongest: no crash → type preservation → invariant → idempotence → roundtrip / oracle.

Assert the strongest property the code supports. "No crash" alone rarely justifies the dependency — if that is all you can find, either a small rearrangement exposes something stronger, or the honest report is that this code is a poor PBT candidate. Rule out the first before settling for the second.

The two ways a property test asserts nothing

• Tautology. assert add(a, b) == a + b restates the implementation; no bug they share can fail it. Pick a property that constrains the function without recomputing it. Note the exception: f(x) == f(x) is a genuine determinism property when f is not obviously pure — serializers over dicts or sets, hashing, anything reading the clock.
• Vacuity. assume() that filters out nearly every input passes without exercising anything, and self-contradictory assume() passes having run zero cases. Push constraints into the strategy so the generator produces valid inputs directly.