Parts I through VI gave us the tools to build software that is correct by design: clear problem statements, explicit models, well-chosen algorithms, organized data structures, and components with stable interfaces. Part VII asks a harder question. Given software that was built with care, how do we keep its behavior dependable as requirements evolve and the code passes through other hands? The answer is to make the software’s assumptions explicit and verifiable at every boundary where those assumptions matter.
Every routine in a system makes two kinds of implicit commitments. It assumes certain things about the world when it is called — that its inputs satisfy certain constraints, that the system is in a certain state. And it promises certain things about the world when it returns — that its output has a certain format, that the system has been left in a certain state. When these assumptions and promises are implicit, they are discovered only through failure. When they are explicit, they can be checked, and a violation becomes diagnostic: the failure occurs at the violated boundary, not at some distant point where the corrupted state finally produces a visible symptom.
A precondition is the formal statement of an assumption: what must be true of the inputs and the current state before this routine may be called. A postcondition is the formal statement of a promise: what will be true of the outputs and the resulting state when this routine returns, given that the precondition was satisfied.
A precondition is a statement about the caller’s responsibility. It says: I, this routine, am only obligated to deliver my postcondition if you, the caller, have satisfied this condition before calling me. If the caller violates a precondition, the routine’s behavior is unspecified — it may signal an error, or it may quietly produce a wrong result. The caller has not held up their end of the contract.
This has a practical consequence: preconditions should not be written to handle the caller’s mistakes gracefully. A precondition is not a validation layer that converts bad inputs into error results. It is a boundary that says: inputs satisfying these conditions are valid inputs for this routine; inputs that do not satisfy them are not. A routine that promises ASSIGNED on valid inputs and BAD_INPUT on invalid ones has not written a precondition — it has written a conditional that handles both cases and made both cases part of the postcondition. That is a legitimate design, but it is different from a contract that rejects invalid inputs with a contract violation.
What belongs in a precondition? Three categories cover most cases.
Input presence and validity. Empty identifiers, null references, and values outside a defined range are inputs that no routine can process meaningfully. Stating the required form explicitly — task_id /= "", priority >= 0 — tells the caller what they must guarantee before the call.
Required state. Many operations are only legal from certain states. A task can only be assigned if its status is PENDING or FAILED. A robot can only be dispatched if it is marked ready. These conditions belong in the precondition, not in a conditional inside the routine body, because they are the caller’s responsibility to ensure before calling.
Relationship constraints. Some operations require that two or more inputs stand in a certain relationship — that a start location and a destination both exist in the same graph, that an update refers to an entity that has been previously registered. When these relationships are required, stating them as preconditions makes the requirement visible and checkable.
A postcondition is a statement about the routine’s responsibility. It says: if you, the caller, have satisfied the precondition, then I, this routine, guarantee the following when I return. The postcondition is an unconditional promise, relative to the precondition — no matter what path through the routine body execution takes, if the precondition was satisfied on entry, the postcondition will be satisfied on exit.
This unconditional quality is what makes postconditions valuable for reasoning. A caller that knows the precondition and postcondition of a routine can reason about what comes after the call without reading the routine’s implementation. The postcondition is the contract the implementation must fulfill, and the implementation can be changed freely as long as it continues to fulfill it.
Three categories cover most postconditions.
Result constraints. What the returned value is allowed to be. A route operation’s result is always one of three declared status values; a score is never negative. Stating these constraints ensures that callers can depend on them rather than defensively checking them.
State transition outcomes. When a routine modifies state, the postcondition records what changed and what the new state satisfies. An assignment operation leaves the task in IN_TRANSIT with the specified robot identifier. A blocking operation leaves the path with status BLOCKED. These assertions close the loop between the operation’s intent and its result.
Derivable consequences. Some postconditions follow from the combination of the precondition and the routine’s action. If a precondition requires non-negative edge costs and the routine computes a sum of edge costs, the postcondition can assert that the result is non-negative — not because the routine checks it explicitly, but because it follows from the combination of the precondition and the computation. Stating derivable consequences explicitly makes them checkable and makes the chain of reasoning visible.
Consider the requirement:
“Assign a task to a robot and return the assignment status.”
Step 1: Define caller obligations. Both identifiers must be present and non-empty — an assignment needs a real task and a real robot to assign to it. And the task’s current status must be PENDING or FAILED — assigning a task that is already IN_TRANSIT or DELIVERED is an illegal transition. These three conditions are the precondition.
Step 2: Define routine guarantees. If the precondition is satisfied, the routine will: set assigned_robot_id to the provided robot identifier, set status to IN_TRANSIT, and return "ASSIGNED". The postcondition asserts all three: assigned_robot_id = robot_id, status = "IN_TRANSIT", and result = "ASSIGNED".
Step 3: Define fail-fast behavior. A call that violates the precondition should fail immediately with a clear signal — a contract violation — rather than silently producing a wrong result that propagates through the system. The earlier a violation is detected, the closer it is to the code that caused it, and the easier it is to diagnose.
Step 4: Verify the contract is complete. A contract is complete when the precondition and postcondition together fully specify the routine’s behavior for all valid inputs. A contract with a precondition that permits inputs the postcondition cannot deliver is incomplete. A contract with a postcondition that leaves the new state underspecified is incomplete. Completeness is the test.
class Delivery_Task
feature
task_id: String
status: String
assigned_robot_id: String
assign(robot_id: String): String
require
task_id_present: task_id /= ""
robot_id_present: robot_id /= ""
can_assign: status = "PENDING" or status = "FAILED"
do
assigned_robot_id := robot_id
status := "IN_TRANSIT"
result := "ASSIGNED"
ensure
assigned: assigned_robot_id = robot_id
now_in_transit: status = "IN_TRANSIT"
known_result: result = "ASSIGNED"
end
invariant
valid_status:
status = "PENDING" or
status = "IN_TRANSIT" or
status = "DELIVERED" or
status = "FAILED"
endRead the structure in layers. The invariant asserts a property that must hold at all times, from construction onward. The precondition on assign adds requirements specific to this operation: the task identifier and robot identifier must be non-empty, and the status must be one that permits assignment. The postcondition asserts what the operation has accomplished.
The three preconditions address different responsibilities. task_id_present is an integrity check on the task itself — a task without an identifier is malformed and should never have been constructed, which is why the invariant also requires task_id /= "". Its presence in the precondition is a belt-and-suspenders assertion that guards against callers operating on malformed instances. The other two are ordinary caller obligations: robot_id_present requires the caller to supply a real robot, and can_assign requires it to check, before calling, that the task is in a state that permits assignment.
The postcondition closes the loop: every commitment made in the do block has a corresponding assertion in the ensure block. A future refactor that modifies the do block must still satisfy every one of those assertions, which means the postcondition is both documentation and test specification.
In the delivery system, the contract in the worked example is one of four. Every state transition on Delivery_Task — assign, start, complete, fail — carries one, and together their preconditions encode the legal transition graph from Modeling Change: which states permit which operations. A developer modifying the transition logic can see at once what each contract requires and whether a change still satisfies it.
Contracts do the same work elsewhere on a smaller scale. The knowledge engine’s scoring operation requires non-empty document and query strings and guarantees a non-negative score, which makes each stage of the pipeline from Breaking Problems Apart independently verifiable. The virtual world’s per-tick state update requires the entity to exist in the current frame and guarantees that its state satisfies the world’s invariants afterward, so a violation is caught at the update boundary before corrupted state reaches collision detection.
Contracts turn the informal expectations that developers carry in their heads — “this must be non-empty,” “this transition is only legal from PENDING” — into executable statements that are checked automatically and fail close to their source.
Missing preconditions for state transitions. A transition operation without a precondition on the current state permits callers to invoke it from any state. A delivered task can be reassigned. A robot can be dispatched before it is ready. The illegal transition is not detected at the call site — it is detected later, when downstream code encounters a state it was not designed to handle. The remedy is to encode transition legality as a precondition on every transition operation. The precondition fires at the call, not at the downstream consequence.
Weak postconditions. A postcondition that asserts only that the result is non-empty, or that the return value is a string, is a postcondition that provides almost no guarantee. A caller that depends only on these weak properties cannot reason about what the operation actually accomplished. The postcondition should assert the specific state changes that matter, such as the new status and the recorded assignment, so that any implementation that fails to accomplish them will violate the postcondition and fail immediately.
Contract drift between similar operations. A codebase with many similar operations — several transition operations, say, or several searches — will accumulate contracts that began as consistent and gradually diverged through independent modifications. One transition requires non-empty task id; another was written later and omits it. One search guarantees NOT_FOUND on miss; another returns an empty string. The inconsistency is invisible until a caller that works correctly with one operation fails with another. The remedy is to review contracts across similar operations periodically and to establish conventions — all transitions require non-empty identifiers, all searches declare an explicit miss status — that future contracts are written to match.
Quick Exercise
Choose one routine in your system — one that is called from multiple places and whose behavior callers depend on — and write its complete contract with four parts: three preconditions that state the caller’s obligations, three postconditions that state the routine’s guarantees, one input that violates a precondition and the behavior that should result, and one valid input with the specific postconditions it should satisfy.
Then verify that the postconditions still hold after one plausible refactor of the routine body. If a refactor that improves the implementation without changing the observable behavior would break a postcondition, the postcondition is specifying implementation rather than guarantees.
Takeaways
The next chapter, Invariants — Rules That Must Never Break, extends the contract discipline from individual routines to entire objects. Where postconditions specify what is true after a single operation, invariants specify what is true at all times — before every call and after every return. Invariants are the class-level counterpart of postconditions, and they are what make it possible to reason about an object’s state without reading every operation that might have modified it.