Preconditions and Postconditions as the Function Contract

A function signature states which values a caller may pass and which value comes back. It says nothing about the relationship between the two. The sentence “returns the index of the first occurrence” is the actual specification, and it lives in a comment, a docstring, or nowhere at all. A contract moves that sentence into a form the machine can check: a precondition that constrains the caller, a postcondition that constrains the result, and an invariant that constrains every observable state in between.

The formalism comes from Hoare logic, where the triple ${P}\ S\ {Q}$ asserts that if assertion $P$ holds before statement $S$ executes, then $Q$ holds afterwards provided $S$ terminates. The important clause is the conditional. A Hoare triple says nothing about what happens when $P$ is false, and nothing about whether $S$ terminates. Those two omissions are where most arguments about specification go wrong.

What the triple does and does not promise

Take a binary search over a sorted slice. The precondition is that the slice is sorted in non-decreasing order and that the element type has a total order. The postcondition is that the returned index, if any, satisfies a[i] == key, and that no earlier index satisfies it. Neither condition mentions termination, and neither mentions what the function does when handed an unsorted slice.

That gap is deliberate rather than sloppy. A specification that promises behaviour for every input is a total specification, and total specifications are expensive: the implementer must decide what an unsorted input means, document it, and test it. A partial specification pushes that decision onto the caller, who is the only party that knows whether the input is sorted. Design by contract formalises the division: the precondition is the caller’s obligation, the postcondition is the implementer’s obligation, and the implementer may assume the precondition without proving it.

This is the same structure that appears at a larger scale in state machine specifications, where each transition carries its own guard and effect. A guard is a precondition on an event; the resulting state is a postcondition on the transition. The difference is that a state machine also has to specify what happens to events that arrive in the wrong state, which a function contract typically leaves undefined.

The blame rule and the substitution principle

The practical value of splitting obligations is diagnostic. When a postcondition fails, the implementer is at fault, because the implementer was permitted to assume the precondition. When a precondition fails at a call site, the caller is at fault, because the caller violated a documented requirement. A single combined assertion gives neither answer, which is why “assert something went wrong” is a weaker debugging aid than two separate checks with distinct messages.

The substitution principle constrains how contracts may evolve. A subtype may weaken its precondition and strengthen its postcondition relative to the supertype; the reverse breaks callers. Weakening a precondition means accepting more inputs, which cannot hurt an existing caller. Strengthening a postcondition means promising more about the result, which also cannot hurt a caller who only relied on the weaker promise. Tightening a precondition, or loosening a postcondition, is a breaking change even when the type signature is untouched. This is the same compatibility reasoning that governs any published interface, and it applies to a private method as soon as two modules call it.

Checking a contract at runtime

A contract written only in prose drifts. A contract written as executable code drifts less, because the check runs whenever the code runs. The cost is a branch and, for anything involving collections, a traversal.

import collections

class QueueFull(Exception):
    pass

class BoundedQueue:
    def __init__(self, capacity):
        if capacity <= 0:
            raise ValueError("capacity must be positive")
        self._items = collections.deque()
        self._capacity = capacity

    def put(self, item):
        # Precondition: the queue is not full. Caller's obligation.
        if len(self._items) == self._capacity:
            raise QueueFull("queue at capacity")
        self._items.append(item)
        # Postcondition: size grew by exactly one and the new item is last.
        assert len(self._items) <= self._capacity
        assert self._items[-1] is item

Two details matter more than the syntax. First, the precondition raises rather than asserts, because a violated precondition is a caller error that a caller can handle by waiting for space, whereas a violated postcondition is an internal defect that no caller can repair. Second, the postcondition compares identity rather than equality: is item states that the stored element is the same object, which is a stronger claim than “an equal element is present” and is the claim the caller actually relies on when the item is mutable.

Postconditions that quantify over the whole collection are the expensive ones. “The queue is sorted” costs $O(n)$ per insertion if checked naively, turning an $O(\log n)$ operation into a linear one. The standard compromise is to check the cheap local condition on every call and the expensive global condition only in a test build, or to maintain the global property incrementally. Both choices are defensible; leaving the property unspecified is not, because then the ordering guarantee exists only in the caller’s head.

Frame conditions: what the contract forgot to say

A postcondition normally constrains the return value and, sometimes, the state of the receiver. It rarely says what did not change. That omission is a frame condition, and it is the most common source of specification bugs that pass every test.

Consider a function documented as returning a sorted copy of a list. Nothing in that sentence forbids the function from also sorting the argument in place. A caller that reuses the original list afterwards observes a changed value with no contract violation, and the failure appears far from its cause. A frame condition states the complement explicitly: the argument is unmodified, no global registry is touched, no file is opened. In languages with ownership or linear types, part of the frame condition is enforced by the type system; in most languages it is not, and the specification has to carry it.

Aliasing is the same problem in a harder form. If a postcondition refers to self.items and a caller also holds a reference to that list, then the postcondition is evaluated against state the caller can mutate concurrently. A contract that quantifies over shared mutable state is only meaningful under a discipline: either the state is copied at the boundary, or the caller agrees not to mutate it for the duration of the call, or the check is performed on a snapshot. Each option has a cost in copies or in discipline, and no contract notation removes the need to choose one.

Class invariants and the state between calls

A method contract constrains one call. An object with several methods also needs a claim that holds between calls, and that claim is the class invariant: a predicate on the fields that every public method may assume on entry and must restore on exit. For the bounded queue above, the invariant is that the item count never exceeds the capacity and that the deque is never None. Neither clause appears in any single method’s contract, and both are relied on by every method.

The invariant interacts with the precondition in a way that is easy to get backwards. A method may assume the invariant on entry, but it may not assume that a caller has checked the precondition — the precondition is the caller’s obligation, and a violated one means the method’s behaviour is unspecified, not that the invariant has been repaired. Conversely, a method that temporarily breaks the invariant, for instance by removing an element before validating a replacement, must either restore it before returning or document that the object is unusable after a failure. That second option is what makes an exception thrown mid-method a specification question rather than a coding detail: the caller needs to know whether the object is still usable.

Constructors complicate the picture, because they run before the invariant holds. A constructor’s postcondition is the invariant itself, and any helper called from a constructor cannot assume it. This is a common source of bugs in languages where virtual dispatch during construction is permitted, and the standard response is to keep constructors free of calls into overridable methods.

Where the contract stops paying

Contracts degrade in three predictable ways. They are incomplete when they omit frame conditions. They are wrong when they assert something the implementation does not actually guarantee, which is worse than no contract because callers build on the false claim. And they are unenforceable when the precondition refers to a property the callee cannot observe, such as “the caller holds no other reference to this object” in a language without ownership tracking.

There is also a cost that has nothing to do with runtime: a contract that restates the implementation in assertion form adds maintenance without adding information. The useful contracts are the ones that state something a reader could not infer from the code: an ordering, an immutability guarantee, an error taxonomy, an idempotency claim. Those properties are also the ones that a design must specify before any code exists, which is why contracts sit at the boundary between requirements and design rather than inside either one. The same obligation appears one level up, at the interface between components, in specifying partial failure: there, the missing frame condition is what happens to the rest of the system when the call does not return at all.