Design by Contract
Preconditions, postconditions, invariants, and the discipline of stating what correct means
Design by Contract
Design by Contract (DbC), introduced by Bertrand Meyer in the Eiffel language, is a way of thinking about modules as parties to an agreement. Each function or method declares what it expects of its caller (preconditions) and what it guarantees in return (postconditions). Each class declares the invariants its instances always satisfy.
The contract is the boundary between two responsibilities. As long as both sides honor the agreement, the code is correct. When one side breaks it, the failure is the responsibility of that side — not its neighbor.
Why Contracts Matter
Most defects come from disagreement about what each piece of code is responsible for. Two functions written by two developers will agree most of the time and disagree on the edge cases neither articulated. The defect lives in the unsaid corners.
Contracts make the corners explicit:
- The caller knows what to provide and what to expect.
- The implementer knows what to assume and what to guarantee.
- The reader can reason about each piece without needing to know the others.
A function with an explicit contract is a function whose correctness can be argued one piece at a time.
The Three Elements
Preconditions — what the caller must guarantee
A precondition is a statement of what must be true before the function is called for the function to be obliged to deliver its result.
/**
* @precondition amount > 0
* @precondition account.status === 'active'
*/
function withdraw(account: Account, amount: number): void { ... }If the caller breaks a precondition, the function is not obliged to do anything sensible. The bug is the caller's. The function is free to fail loudly — that is the right behavior, not "robust" silent recovery.
Postconditions — what the function guarantees
A postcondition is a statement of what is true after the function returns, assuming the preconditions held.
/**
* @postcondition account.balance === old(account.balance) - amount
* @postcondition return.timestamp >= now
*/
function withdraw(account: Account, amount: number): WithdrawalRecord { ... }If the postcondition is broken, the bug is the function's — it failed to keep its promise.
Invariants — what is true between operations
An invariant is a statement that is true on entry to every method of a class, and true again on exit. Invariants survive across operations; they are properties of the object's identity.
class Account {
// Invariant: balance >= 0
// Invariant: balance === sum(transactions)
}Every method may temporarily break the invariant during its execution; what matters is that the object is consistent again before any other method can observe it.
The Asymmetry With Defensive Programming
Both DbC and defensive programming care about correctness, but they assign responsibility differently.
| Defensive programming | Design by Contract | |
|---|---|---|
| Who validates inputs? | The function | The caller |
| What does the function do on bad input? | Recover, return an error, retry | Fail; the contract was broken |
| Where is validation logic? | Throughout the codebase | At the boundary, then trusted |
| Risk | Defensive code obscures intent and hides bugs | Contract violations can corrupt state if not caught |
Modern systems use both, deliberately:
- At the trust boundary (HTTP request, file input, RPC) — defensive: validate everything, the world is hostile.
- Inside the trusted core — DbC: contracts are documented, enforced by assertions in development, and trusted in production.
The mistake is to apply defensive programming everywhere. Validating internal calls produces noise without improving safety, and it teaches the team that violations are recoverable when they are not.
Stating Contracts Explicitly
In the type system, when possible
The strongest contract is one the compiler enforces. Modern type systems can carry a surprising amount of contract:
- Non-null types make "the input is not null" a precondition the compiler verifies.
- Newtype wrappers (
UserIdvsOrderId) prevent passing one where the other is expected. - Refinement types (
PositiveNumber,NonEmptyString) push input validation into construction. - Sum types (
Result<T, E>, sealed hierarchies) express the postcondition exhaustively.
Each piece of contract moved into the type system is one that cannot be forgotten at the call site.
In assertions, where the type system cannot
What the compiler cannot check, assertions can:
function withdraw(account: Account, amount: number): WithdrawalRecord {
assert(amount > 0, 'precondition: amount must be positive');
assert(account.status === 'active', 'precondition: account must be active');
// ... implementation ...
assert(result.balance === oldBalance - amount, 'postcondition: balance updated');
assert(this.invariant(), 'invariant restored');
return result;
}Assertions document the contract in code that runs in development and tests, and that fails loudly when the contract is broken. In production, they may be compiled out for performance — preserving the documentation value without the runtime cost.
In documentation, when neither suffices
When a contract is not expressible in types or runtime checks — "the caller must hold the global lock," "this method must be called within a transaction," "the result is meaningful only when the input is sorted" — write it in the docstring.
/**
* Returns the median of the input.
*
* @precondition values must be sorted in ascending order
* @precondition values is non-empty
*
* The function does not check sortedness. Passing unsorted
* input is a programming error and produces unspecified output.
*/
function median(values: number[]): number { ... }Documented contracts are weaker than enforced ones, but they are stronger than unstated assumptions.
Inheritance and Contracts
Inheritance complicates contracts. The Liskov Substitution Principle (covered in Design Principles) restated in contract terms:
- A subclass may weaken preconditions: accept more inputs than the parent.
- A subclass may strengthen postconditions: guarantee more than the parent.
- A subclass may strengthen invariants: maintain everything the parent does, and more.
- A subclass may not do the inverse: accept less, guarantee less, or violate parent invariants.
When a subclass tightens what a caller can pass, callers written against the parent break. This is a design defect, not an implementation bug.
Contracts at System Boundaries
The trust boundary is the place where contracts shift from "documented and asserted" to "validated and enforced":
- HTTP APIs. Validate request bodies against a schema. Reject anything that does not satisfy the contract before it reaches the handler.
- Inter-service calls. Use schemas with versioning. Contract tests verify that producer and consumer agree.
- Database boundaries. Constraints (NOT NULL, foreign keys, check constraints) enforce invariants at the storage level — the last line of defense.
- Message queues, file uploads, configuration files. Same principle: validate at the edge, trust the interior.
Each layer crossed without validation propagates uncertainty. A request whose shape was checked at the gateway can be trusted by the handler. A request whose shape was assumed by the handler is a defect waiting for malformed input.
Contracts and Failure
When a contract is broken, the response should be:
- Loud. A broken contract is a bug, and a bug should be visible. Silent recovery hides defects.
- Local. The handler that detects the violation should report it, not propagate corrupted state further.
- Diagnostic. The error message should make the violation easy to debug — which precondition, which value, which caller.
A contract violation that produces "OK, processed: false" with no other signal is the worst outcome: the caller does not realize anything went wrong, and the bug accumulates damage downstream.
The Smaller Lesson
Even when DbC is not adopted as a formal practice, its underlying lesson is portable:
Every function has a contract — written or not. Make it written.
The act of stating preconditions and postconditions clarifies what the function actually does, often revealing that the original intent was vague. Many "bugs" turn out to be cases the original author never considered, and would have considered if asked to write the contract first.
Pre-Commit Checklist
- Are the preconditions of each function expressible in the type system, where possible?
- Are the remaining preconditions stated in documentation or asserted at runtime?
- Does each public method's docstring describe what is guaranteed on return?
- Does each class have stated invariants, with assertions or tests that verify them?
- Do subclasses honor the substitution principle — never tightening preconditions or weakening postconditions?
- Is contract enforcement concentrated at the trust boundary, with the interior trusting the contracts?
- When a contract is violated, does the failure point to the responsible party, with enough information to act on?