Design by Contract

When you hire a builder, you sign a contract: you promise to supply the site and pay on time; they promise to deliver a house that meets code. Neither side re-checks the other's promises on every nail — the contract fixes who is responsible for what, so each party can work with confidence. Design by Contract (DbC) applies exactly this idea to software. Every routine is a tiny legal agreement between a caller and the routine itself, written in the code as machine-checkable assertions.

The idea is Bertrand Meyer's, baked into the Eiffel language in the mid-1980s. It takes the raw material of assertions and invariants and organises them into a discipline: a precondition guards the door, a postcondition promises the result, and a class invariant holds steady across an object's whole life. Together they turn a vague "this function sorts a list" into a checkable, documentable, inheritable promise.

Three clauses: require, ensure, invariant

A contracted routine carries three kinds of assertion, and each has an owner who is responsible for making it true:

Formally these are the pre- and postconditions of a Hoare triple \{P\}\,C\,\{Q\} attached to the routine body C — DbC is Hoare logic made into a language feature you can actually run.

A contracted routine

Here is a stack's push, written with its contract explicit. Read the assertions as the specification and the body as the implementation that must live up to it.

class BoundedStack<T> { private items: T[] = []; constructor(private readonly capacity: number) {} // class invariant (should hold before/after every public method): // 0 <= this.count() <= this.capacity count(): number { return this.items.length; } isFull(): boolean { return this.count() === this.capacity; } push(x: T): void { // require (caller's obligation): there is room if (this.isFull()) throw new Error("precondition violated: stack is full"); const oldCount = this.count(); this.items.push(x); // the actual work // ensure (our obligation): the item is on top and the count grew by one console.assert(this.top() === x, "postcondition: pushed item is on top"); console.assert(this.count() === oldCount + 1, "postcondition: count increased by 1"); } top(): T { return this.items[this.items.length - 1]; } }

Notice the asymmetry. The precondition is checked and, if violated, blames the caller loudly and early. The postconditions describe what a correct body achieves; they document intent and catch bugs in the routine itself. And both refer to oldCount — the value before the call — which is why Eiffel gives you a first-class old keyword to name pre-state expressions inside a postcondition.

Obligations and benefits: the client/supplier table

Meyer's favourite framing is a table of obligations and benefits. The precondition is an obligation on the client but a benefit to the supplier (it gets to assume it); the postcondition is an obligation on the supplier but a benefit to the client. Each side's obligation is the other side's gift.

ObligationBenefit
Client (caller) Establish the precondition before calling. Gets the postcondition, for free, on return.
Supplier (routine) Establish the postcondition on return. May assume the precondition — need not check for cases it forbids.

The payoff is that no property is checked twice. If the precondition says the argument is non-null, the caller guarantees it and the routine simply trusts it — no redundant null-check inside. Each obligation is discharged exactly once, by whoever is in the best position to do it.

Defensive programming tells every routine to distrust its inputs and re-validate everything, everywhere. It feels safe but it is wasteful and, worse, it hides bugs: a routine that silently "handles" a nonsensical argument by returning a default lets a caller's mistake propagate far from its origin, where it is agony to debug. Design by Contract instead assigns responsibility. A precondition is checked in exactly one place — and its violation is a symptom of a caller bug, reported immediately at the boundary. The point isn't to check less for its own sake; it's that redundant, ownerless checks blur who is to blame. A clear contract makes every failure point at the party that broke its promise.

Contracts under inheritance: behavioural subtyping

Contracts get subtle — and powerful — when a subclass overrides a method. If code was written against a parent's contract, an object of a subclass must be usable everywhere the parent was without surprises. That is the Liskov Substitution Principle, and it dictates exactly how a subclass may re-negotiate the contract.

Note the direction: preconditions relax going down the hierarchy, postconditions tighten — the mirror image of the rule of consequence in Hoare logic, and for the same reason. A caller who satisfied the parent's precondition automatically satisfies the child's (weaker) one, and receives at least the parent's (now stronger) postcondition. Substitution is safe. Do it backwards — a subclass that demands more of its callers — and you have the classic Liskov violation: code that works with the base class breaks the moment a subclass object arrives.

The instinct to "tighten things up" in a subclass is exactly backwards for preconditions. Suppose Rectangle.setSize(w, h) accepts any positive w, h, and a subclass Square.setSize "improves" it by requiring w === h. Now a function that was written to resize any Rectangle — perfectly correct against the base contract — throws the moment it is handed a Square, because it passed unequal sides the base contract allowed. The subclass strengthened a precondition, and substitutability is destroyed. The rule to memorise: preconditions may only get weaker, postconditions only stronger, as you go down the hierarchy. Getting this backwards is the single most common way inheritance quietly violates a contract.

Contracts in languages you already use

Few mainstream languages have Eiffel's built-in require/ensure/invariant keywords, but the discipline is everywhere once you know its shapes:

LanguageHow contracts appear
EiffelNative require, ensure, invariant, old; checked at runtime, inherited by the subcontracting rules.
JavaHistorically JML annotations (//@ requires, //@ ensures) checked by tools; plainly, assert and guard clauses throwing IllegalArgumentException.
Kotlinrequire(...) and check(...) stdlib functions throw on a false precondition/state check — a direct, idiomatic pre/post-condition idiom.
PythonThe assert statement, or libraries like icontract/deal with real pre/postcondition decorators.
C / C++<cassert>'s assert; C++26 adds a native contracts facility (pre, post).

Even the humble assert is a contract clause in disguise. What DbC adds on top is method: name the three clauses, assign each an owner, and let inheritance re-negotiate them by the subcontracting rules. Contracts also double as documentation that cannot rot — because they run, they can never silently drift out of step with the code the way a comment does.