Design by contract
A Socratic walk-through of design by contract — reasoned out one step at a time, not lectured.
The question we started with
THE QUESTION #Why write down what a function refuses to accept rather than making it cope with anything?
A careful programmer's instinct is to make each function bulletproof: check every argument, handle the null, tolerate the empty list, clamp the out-of-range number. Nothing you can pass it will make it misbehave. That looks like the definition of robust code.
Bertrand Meyer's design by contract, built into the Eiffel language in the 1980s, proposes something that sounds like the opposite. A routine should state, formally, the conditions under which it declines to work at all — and then assume they hold, doing no checking beyond them. Why would refusing work be better engineering than coping?
Reasoning it through
REASONING #Start with a question the bulletproof style never asks: when a routine is handed something it cannot sensibly process, whose mistake was it?
Suppose withdraw is called with a negative amount. Either the caller was obliged not to do that, or the routine was obliged to handle it. Somebody's obligation. The trouble with the defensive style is that it never decides, so both parties assume the other is responsible — and the caller checks, and the routine checks again, and a third layer checks once more. The condition is now tested in several places, stated nowhere, and if the rule changes, every check must be found.
Now make the decision explicit and see what falls out. A precondition is what the caller must guarantee before calling; a postcondition is what the routine guarantees on return, provided the precondition held; an invariant is what stays true of the object between calls. Together they form a contract with a benefit-and-obligation structure that Meyer draws as a table: each party's obligation is the other's benefit. The caller's obligation to pass a positive amount is exactly what buys the routine the right not to check.
That word right is the pivot. A precondition is not a validation; it is permission to omit validation. If a routine says amounts must be positive, then inside it the amount is positive, full stop — there is no defensive branch, no error path, no question of what to return for a negative one. Whole categories of code and of nonsense return values simply do not exist. And redundancy disappears: the condition is written once, in the place a reader looks for it.
Then blame becomes computable, which is the practical prize. If a precondition is violated, the caller has a bug. If a postcondition fails while the precondition held, the routine has a bug. If an invariant breaks, the class has one. Contrast the defensive style, where a routine that silently clamps a bad argument produces a wrong answer far away and leaves nobody obviously at fault. This is the same argument as failing fast, made precise: the contract says exactly where to stop and who to tell.
Contracts also do something documentation cannot. A comment saying "amount should be positive" is a hope. An executable assertion is checked, so it cannot drift from the code the way prose does — and it is checked by every test you already run, without your writing a test for it. That is what makes contracts cheap: the specification and the check are the same text.
There is one further consequence worth following, because it explains an otherwise arbitrary-sounding rule about inheritance. If a subclass may be substituted for its parent, then any caller who satisfied the parent's contract must be safe. So an overriding method may weaken a precondition — accept more — but never strengthen it, and may strengthen a postcondition — promise more — but never weaken it. That is Liskov substitution stated in contract terms, and it turns a stylistic guideline into something a compiler or runtime can enforce.
The analogy
THE ANALOGY #Think of a dry cleaner's ticket. It says what they will accept — no leather, nothing with the label removed — and what they promise in return, clean by Thursday. Refusing leather is not poor service; it is what makes the Thursday promise meaningful, because a shop that accepted absolutely anything could only promise to try. The narrower the intake, the stronger the guarantee that can honestly sit on the other side.
a shop inspects each item at the counter, whereas a precondition is deliberately not re-inspected in production builds — so the contract's protection depends on the obligation having been met upstream, not on a check at the point of handover.
Clarifying the model
THE MODEL #Three refinements.
First, contracts are not input validation, and conflating them is a security hazard. Data arriving from a user, a network, or a file is untrusted and must be validated — that validation is ordinary functionality, on the boundary, with a defined error result. Preconditions govern the internal interface between components you control, where a violation means a bug rather than a hostile input. Many teams run with assertions disabled in production for speed, which is defensible for the internal case and catastrophic if a precondition was quietly doing the boundary's job.
Second, contracts do not require a special language. Eiffel has dedicated syntax and Ada 2012 added Pre and Post aspects, but assertions at the top and bottom of a routine, refinement types, or a type system that makes the illegal state unrepresentable all express the same idea. The strongest version is not a runtime check at all: a parameter of type PositiveAmount has a precondition the compiler enforces, and nothing can violate it.
Third, contracts are a specification technique before they are a checking technique. Most of their value arrives at design time, when writing down what a routine refuses forces you to notice that you never decided — which is usually the moment the real interface improves, whether or not a single assertion is ever evaluated.
A picture of it
THE PICTURE #How to readThe three boxes are the clauses of one contract and the two rounded elements are the parties. Read the arrows as assignments of responsibility: the caller, not the routine, satisfies the precondition, which is why the routine contains no check for it — and the routine alone satisfies the postcondition. The invariant is traced by the routine rather than satisfied by either party, because it is a property of the object that must survive every call. If a check fails, the arrow pointing at it names who has the bug.
What became clearer
WHAT CLEARED #Making a function cope with anything sounds generous and quietly costs a great deal: the same condition is tested repeatedly, stated nowhere, and no one is responsible when it is violated, so wrong values travel instead of stopping. A contract does the opposite — it decides the obligation once and writes it where both parties can see it. The refusal is not the point; it is the price of a guarantee, since a routine that accepts everything can promise almost nothing. And because the clauses are executable, the specification cannot drift from the code, and substitutability in a subclass becomes a rule about widening intake and narrowing promise rather than a matter of taste.
Where to go next
ONWARD #- How refinement types and dependent types move preconditions from run time to compile time.
- Where property based testing fits, since a postcondition is very close to the property such a tool would check.
Key terms
TERMS #| Term | What it means |
|---|---|
| Precondition | what a caller must guarantee before invoking a routine; its violation is the caller's bug. |
| Postcondition | what the routine guarantees on return, given that the precondition held. |
| Class invariant | a property of an object that holds before and after every public call, though not necessarily during one. |
| Design by contract | Meyer's method of specifying components as mutual obligations, implemented natively in Eiffel and as aspects in Ada 2012. |
Every term the collection defines is gathered in the glossary.