Property tests need a model

More inputs cannot rescue a weak assertion

Suppose a serializer and parser are tested by encoding a value and checking that decoding returns it. That round-trip property is useful, but the two implementations can share the same mistake. They might both swap fields or agree on an encoding that violates the external protocol. Running the property a million times would strengthen evidence for their mutual agreement, not for interoperability. I would state exactly what the assertion establishes and add an independent oracle or known-format examples for claims it cannot support.

A similarly weak test calls a function twice and asserts equal output. That can detect nondeterminism under controlled inputs, but a consistently wrong function passes. The point is not to dismiss simple properties. Each should be tied to a failure mode and a contract. Idempotence, conservation, order preservation and rejection of invalid input can all be powerful when they express actual requirements. A generated test suite becomes convincing when its properties constrain meaning rather than merely restate the operations the implementation already performs.

A simpler representation can be a better oracle

For a bounded stack implemented with a compact array and indices, an ordinary list can serve as a reference model. Push appends when capacity permits; pop removes the last element or reports empty. The production implementation may optimize memory layout, but the model should prioritize clarity. I would compare returned outcomes and logical contents after every action. That catches a wrong result close to the transition that caused it instead of waiting for a final aggregate mismatch after a long generated history.

Independence matters more than sophistication. Copying the production index arithmetic into the model reproduces the same likely mistakes. A model with a different representation can expose wraparound, overflow or stale-slot errors because it does not share those mechanisms. It still needs review: a wrong specification produces a confidently wrong oracle. I would keep a few hand-worked histories, including capacity overflow and empty removal, beside the model. They anchor the interpretation and make it easier for a reviewer to challenge an assumption before generation amplifies it.

References: [2] Hypothesis: Stateful tests

Stateful properties explore histories

A stateless generator explores values; a stateful generator also explores sequences of actions. For a tiny alphabet containing push zero, push one and pop, there are 3^4, or 81, histories of exactly four actions. Including lengths zero through four gives 1 plus 3 plus 9 plus 27 plus 81, or 121 histories. This bounded space can be exhausted directly. Larger state spaces require sampling or other exploration, but the small calculation illustrates how quickly even a simple interface acquires meaningful ordering cases.

Consider a capacity-two stack receiving push zero, push one, rejected push zero, then pop. The final pop must return one, and the rejected push must not mutate contents. A test that only checks the capacity bound can miss an implementation that overwrites the oldest element when full. The model's rejection semantics are therefore as important as its successful operations. I would generate invalid attempts deliberately when the interface defines them, instead of filtering the generator until it produces only histories that make every command succeed.

for action in generated_history:
  expected = reference_model.apply(action)
  actual = implementation.apply(action)
  assert actual.outcome == expected.outcome
  assert implementation.logical_contents() == reference_model.contents
  assert 0 <= implementation.length() <= capacity

# Rejected pushes and empty pops are generated, not filtered away.

Generators encode assumptions about the world

A generator is a distribution over the cases the test will examine. Uniform random integers do not automatically produce realistic inputs or difficult boundaries. If most bugs involve zero length, maximum capacity or repeated identifiers, those cases deserve intentional weight. QuickCheck's original approach makes custom generators central rather than incidental. I would review the generator with the same attention as the assertion: what categories can it produce, how often, and which supposedly possible inputs are unreachable because of a convenient construction rule?

Constraints should be expressed constructively where possible. Repeatedly generating arbitrary values and discarding almost all of them can waste the test budget and leave little effective coverage. Yet constructing only valid values can conceal the parser or API's rejection behaviour. I would separate valid-domain properties from invalid-input properties and label the cases observed. Coverage statistics for categories such as empty, full, duplicate and boundary-sized are more informative than the raw number of generated examples when the distribution is otherwise difficult to see.

References: [1] Claessen and Hughes: QuickCheck

Shrinking is part of the explanation

A failing history with hundreds of operations is evidence, but a short counterexample is much easier to understand and retain. Shrinking attempts to preserve failure while simplifying the input. For stateful tests, simplification must respect enough of the history to keep the failure meaningful. Removing a setup action may make a later operation invalid, which could hide the original bug or reveal a different one. I would inspect the minimized failure as an execution trace, including preconditions and outcomes, rather than accept its final exception message as the whole diagnosis.

Once understood, preserve the minimal example as a regression fixture alongside the broader property. The fixture documents the discovered failure mode, while continued generation explores nearby cases and future changes. Replaying only a random seed can be less durable when generator logic or framework versions change. Store the actual failing values or action sequence when practical. That artifact also helps distinguish a genuine implementation defect from a mistaken property, a flaky external dependency or an assumption that the test environment did not satisfy.

Metamorphic relations help when exact answers are expensive

Some operations lack a cheap exact oracle. A search algorithm, numerical transform or large optimizer may still obey useful relationships between related inputs. Reordering independent records might preserve an aggregate, adding a zero contribution might preserve a sum, or applying a normalization twice might equal applying it once. These are metamorphic properties. I would derive them from the domain and state their preconditions, because numerical rounding, ordering requirements or hidden state can invalidate an apparently obvious algebraic relation.

The counterargument is that a collection of such properties may still admit many incorrect implementations. A function returning a constant can satisfy surprising numbers of symmetry and idempotence checks. I agree; metamorphic relations are complementary constraints, not a universal proof. Combine them with exact small cases, differential implementations or invariants that exclude trivial wrong answers. The desired test suite narrows the space of permitted behaviour from several independent directions. It should not rely on a single elegant property whose blind spots happen to match the implementation's mistakes.

Match the claim to the explored model

Passing generated tests provides evidence over the explored cases and execution environment. It does not prove every input or concurrent interleaving. A sequential reference model can support checking observed concurrent histories for an appropriate correctness condition, but that requires additional machinery; simply running several test threads is not enough. I would state whether the property concerns sequential behaviour, bounded schedules or a particular concurrency model. The test report should preserve that scope rather than turn a large example count into an unrestricted correctness claim.

A strong property suite remains understandable to someone who did not write the implementation. Its model uses simple concepts, its generators expose boundary assumptions and its failures shrink into useful explanations. That structure makes it valuable during optimization, when the implementation may change substantially while the contract stays fixed. Property testing is most effective when it makes the specification executable and independent. The random inputs provide reach; the model provides meaning. Without the latter, generation can spend considerable time verifying that the code behaves like itself.

I would periodically challenge the suite with a few deliberate incorrect variants, such as dropping a full-stack rejection or returning the wrong end. This is a focused check that the chosen properties can detect the failures they claim to cover. It need not become an elaborate mutation-testing project to reveal a weak oracle.