Skip to content

Design-by-Contract Clause

Contract rule — instantiates Representation-Independent Interface Contract

Attaches to each operation a precondition, a postcondition, and the policy for a broken precondition — so that when a call goes wrong, the clause names, per call, whether the caller or the component is at fault.

A Design-by-Contract Clause states, for a single operation, a precondition (what the caller must guarantee), a postcondition (what the operation guarantees in return), and the policy for what happens when a precondition is broken. Its distinctive move is the allocation of responsibility: a precondition makes the caller at fault if it is violated; a postcondition makes the component at fault if it is.[1] That asymmetry — who owes what to whom — is what turns "it broke" into the actionable "the caller broke its promise" or "the component broke its promise," which is what decides where the fix belongs. It is a sharp legal line, not a graded tolerance: a call either meets the precondition or it does not. Where the Abstract Data Type Specification models the whole value space and the Interface Definition Language declares signatures, this mechanism states, operation by operation, the promise and the error responsibility.

Example

A flight-booking service exposes reserveSeat(flightId, seatId). The clause reads: precondition — the flight exists and the seat is currently free; postcondition — the seat is marked reserved to this booking and the free-seat count falls by exactly one; error policy — calling for an already-taken seat is a caller fault (precondition violated), so it raises SeatUnavailable and leaves the component's state untouched — no partial reservation.

Now trace two failures. A client that requests a seat someone already holds gets SeatUnavailable; the contract says this is the caller's error, and correctly so — the component did exactly what it promised. But if the seat was free and the component double-books it anyway, the postcondition ("at most one reservation per seat") is breached, which the contract pins squarely on the component. When a race condition surfaces as a double-booking in production, nobody has to argue about ownership: the postcondition guaranteed at-most-one, so it is a component defect, and the fix belongs in the component's concurrency handling — not scattered across every caller as defensive re-checks.

How it works

  • Write the precondition as the caller's obligation and the component's benefit — the smaller and clearer, the better.
  • Write the postcondition as the component's obligation and the caller's benefit — an independent promise, not a restatement of the code.
  • Fix the violation policy — what a broken precondition produces (typically: raise, and leave state unchanged), distinct from a broken postcondition (a component bug to surface loudly).
  • Make the clauses checkable — runtime assertions turn the promise into an enforced guard rather than a hopeful comment.

Tuning parameters

  • Precondition strength — demanding (push validation onto callers, keep the component lean and fast) versus defensive (the component checks everything). Strong preconditions simplify the component but burden every caller.
  • Check enforcement — assertions on always, in tests only, or off in production for speed. Off-in-production means the contract documents but no longer enforces.
  • Failure semantics — fail-fast (raise on a broken precondition) versus a total operation that defines a result for every input and has no precondition to break.
  • Invariant granularity — per-operation clauses only, or also a class-level invariant every operation must preserve.
  • Subtyping discipline — how strictly an overriding implementation may weaken preconditions or strengthen postconditions when standing in for the original.

When it helps, and when it misleads

Its strength is turning vague "handle errors gracefully" into a precise, per-operation allocation of fault that localizes a bug to whichever side broke its promise — and, when checked at runtime, catches that break at the moment it happens. Its failure modes: preconditions set so strong that every caller re-implements the same check, or so weak the component must defend against everything; assertions disabled in production, which yields false confidence because the contract is now only documentation; and clauses that drift from actual behavior over time. The classic misuse is a postcondition that merely restates the implementation ("returns whatever the code returns"), which can never catch a bug because it is true by construction. The discipline that keeps it honest is to state pre- and postconditions independently of the implementation, keep at least test-time checking enabled, and make the precondition a documented, client-visible rule rather than a hidden internal guard.

How it implements the components

This mechanism supplies the per-operation promise and error allocation side of the archetype:

  • behavioral_contract_statement — the precondition/postcondition pair is the operation's behavioral contract, stated apart from the code.
  • edge_case_and_error_policy — the precondition-and-violation rules define what counts as a caller error versus a component error, and what the component does in each case.

It does not model the abstract value space and its invariant (the Abstract Data Type Specification), declare the syntactic operation surface (the Interface Definition Language), or provide the oracle that checks the clauses across implementations (the Black-Box Contract Test Suite).

Notes

A contract clause is a promise, not a proof — something else must check it. Runtime assertions, the Black-Box Contract Test Suite, and property tests are the mechanisms that verify the promise is kept. Left entirely unchecked, a clause degrades into a comment that can be silently false, which is worse than no contract because it is trusted.

References

[1] Design by Contract (Bertrand Meyer, realized in the Eiffel language) frames a routine as a contract between client and supplier: the client must establish the precondition; in exchange the supplier must establish the postcondition. Class invariants extend the idea to conditions that must hold across every operation. The framework's value here is precisely its assignment of obligation, which is what makes fault attributable per call. ↩