Design by Contract: Make Assumptions Explicit

A function often depends on rules that its type signature doesn’t fully express. A withdrawal amount must be positive. A completed operation must leave the balance consistent. An object may require its reserved quantity to stay between zero and the quantity on hand.

When those rules live only in developers’ heads, failures appear far from their cause. Design by Contract gives the rules names and assigns responsibility for them. The useful mental model is simple: the caller promises to meet the operation’s entry conditions, and the operation promises a valid result while preserving the object’s valid state.

This article explains how to use preconditions, postconditions, and invariants as practical design tools, even when your language has no special contract syntax.

Think of a contract as a boundary agreement

Suppose an account exposes this operation:

withdraw(amount)

The name tells us the action, but several questions remain. Is zero allowed? Can the account become negative? What must be true after a successful withdrawal?

A contract separates those questions into three kinds of rules:

  • A precondition must be true before an operation starts.
  • A postcondition must be true when the operation completes successfully.
  • An invariant must remain true for every externally observable valid state of an object or component.

For a simple account, we might state the contract like this:

precondition:  amount > 0
precondition:  amount <= balance

postcondition: balance == old(balance) - amount

invariant:     balance >= 0

old(balance) means the balance as it was when the operation began. This is specification notation, not a claim about syntax in a particular programming language.

The value of these statements is not formality for its own sake. Each one answers a different debugging question. If amount is negative, the caller supplied an invalid request. If a valid withdrawal subtracts the wrong amount, the operation failed its promise. If some operation leaves the account with a negative balance, the object’s valid-state rule has been broken.

Preconditions define what an operation accepts

A precondition describes the inputs or state an operation is entitled to rely on. It narrows the set of situations the implementation must handle as normal execution.

Consider a reservation operation:

reserve(item, quantity)

If the intended rule is that quantity must be positive and no greater than the currently available stock, those conditions belong at the operation boundary:

precondition: quantity > 0
precondition: quantity <= item.availableQuantity

That is more precise than saying “reserve validates its arguments.” It tells callers what a valid call means.

The important design question is who can reasonably satisfy the condition? A caller can usually choose not to pass -3, so quantity > 0 is a sensible precondition. By contrast, a caller may not be able to guarantee that a remote payment service is reachable. Network availability is an environmental failure, not a useful precondition on chargeCustomer.

This distinction prevents contracts from becoming a way to dismiss real failure modes. Preconditions should describe obligations a caller can know and meet at the boundary where the call is made.

External input still needs validation. A public API may receive quantity = -3 from an untrusted client and return a structured validation error. Inside the application, a lower-level operation may treat the same condition as a broken programming assumption because an earlier boundary was supposed to reject it.

The rule can be the same while the response differs by boundary.

For example:

HTTP boundary:
    if quantity <= 0:
        return validation_error("quantity must be positive")

application operation:
    require(quantity > 0)
    reserve(item, quantity)

The first check handles expected invalid input. The second protects an internal assumption and helps expose a bug if some other caller bypasses the validated path.

Postconditions describe what success guarantees

A postcondition describes the observable result after an operation succeeds. It should say what changed, not merely restate that the function ran.

For the reservation example, a useful postcondition might be:

postcondition:
    item.availableQuantity == old(item.availableQuantity) - quantity

If the operation also returns a reservation, another condition could be:

postcondition:
    reservation.quantity == quantity

These guarantees help both callers and implementers. Callers know what they can safely rely on next. Implementers know which behavior must survive refactoring.

A weak statement such as reservation != null may be insufficient if callers actually depend on the reservation representing the requested quantity. A contract should capture the property that matters to the collaboration.

Postconditions don’t need to expose private implementation details. Saying that a reservation was persisted in a particular table would unnecessarily tie a behavioral contract to storage design unless that storage fact is genuinely part of the boundary’s promise.

Invariants protect valid state across operations

An invariant is a rule that should hold whenever an object or component is in a valid, externally observable state. It connects operations that would otherwise be reasoned about separately.

Suppose an inventory item stores these values:

onHand
reserved

A useful invariant could be:

0 <= reserved <= onHand

Now reserve, release, and stock-adjustment operations all share one responsibility: none may leave the item violating that rule.

This changes how you review code. Instead of asking only whether release(5) subtracts five, you also ask whether every path preserves the valid-state rule. An implementation that accidentally makes reserved negative is wrong even if its local arithmetic looks plausible.

Invariants are strongest when the component controls the state they describe. If arbitrary callers can directly assign reserved, the invariant is difficult to enforce because mutation bypasses the operations responsible for preserving it. Encapsulation and invariants therefore reinforce each other: controlled state changes give the invariant a meaningful enforcement boundary.

An invariant also doesn’t mean every intermediate instruction must satisfy the rule. An operation may temporarily rearrange internal state while it runs. What matters is that invalid intermediate state is not exposed as a valid completed state. Concurrency, callbacks, or re-entrant code can make that distinction important because they may expose state earlier than expected.

Put each responsibility on the right side of the contract

Contracts become useful when they clarify responsibility rather than duplicate checks everywhere.

Imagine transfer(source, destination, amount). One possible contract is:

precondition:  amount > 0
precondition:  source.balance >= amount

postcondition: source.balance == old(source.balance) - amount
postcondition: destination.balance == old(destination.balance) + amount

invariant:     source.balance >= 0
invariant:     destination.balance >= 0

If callers must establish the source has sufficient funds, the transfer implementation may rely on that fact. If instead the operation is intended to handle insufficient funds as a normal business outcome, then sufficient funds should not be a precondition. The operation might return declined without changing either balance.

Both designs can be valid. They describe different APIs.

This is why a contract is not simply a collection of assertions added after the code is written. Deciding what belongs in the precondition changes who owns a decision. Deciding what the postcondition guarantees changes what callers may depend on.

A useful review question is: if this condition is false, which side failed to keep a promise? If the answer is unclear, the boundary itself may need a clearer design.

Stronger and weaker contracts affect substitutability

Contracts also matter when one implementation can stand in for another.

Suppose a base abstraction accepts any positive withdrawal up to the current balance:

precondition: 0 < amount <= balance

A replacement implementation that accepts only withdrawals of at least 100 imposes a new requirement:

precondition: 100 <= amount <= balance

A caller that correctly used the original contract with withdraw(50) would now fail. The replacement has strengthened the precondition from the caller’s perspective.

Similarly, if the original operation guarantees that a successful withdrawal reduces the balance by exactly the requested amount, a replacement cannot weaken that guarantee to “the balance probably decreases.” Existing callers are entitled to depend on the original promise.

The practical rule is that a substitutable implementation should not demand more from callers than the abstraction promises, and it should not promise less in return. This is one reason precise contracts make interface design easier to reason about: compatibility becomes a question about obligations and guarantees, not just matching method names.

Assertions can enforce contracts, but choose the failure policy deliberately

Many languages and libraries provide assertions or explicit guard functions that can encode contract conditions. The mechanism matters less than the semantics you choose.

An internal precondition might look like:

function reserve(item, quantity):
    require(quantity > 0)
    require(quantity <= item.availableQuantity)

    item.reserved = item.reserved + quantity

    ensure(item.reserved <= item.onHand)

This is pseudocode. require and ensure represent contract checks rather than APIs from a specific language.

A failed internal contract usually indicates a programming defect or corrupted state, so silently continuing is dangerous. But production behavior still depends on the system. A service may translate the failure at a process boundary, record diagnostics, isolate one request, or terminate a component when continuing would make state less trustworthy.

Don’t use assertions that can disappear in some build mode as the only protection against hostile or ordinary invalid external input. Validation that forms part of an external interface’s behavior must remain active when that behavior is required.

Contract checks also aren’t a substitute for error handling. Disk exhaustion, timeouts, dependency failures, and optimistic-concurrency conflicts can occur even when every caller satisfies its preconditions. Model those as operational outcomes where the system needs to recover or report them.

Avoid contracts that merely move confusion around

Several mistakes make contract-style design noisy without making the software clearer.

The first is checking every obvious type property again. If a type already guarantees a value is non-null or a constructor guarantees a quantity is positive, repeating the same condition at every private helper may add ceremony without new protection. Put checks where trust changes or where a violated assumption would otherwise be difficult to diagnose.

The second is writing conditions in terms of implementation details. A postcondition such as “cache slot 7 contains this object” makes future refactoring harder unless callers genuinely observe that cache. Prefer behavioral guarantees.

The third is making preconditions impossible for callers to establish. Requiring “the database will remain available for the next second” doesn’t create a useful contract. It hides an operational uncertainty behind specification language.

The fourth is treating invariants as global wishes. “The whole system is consistent” is too broad to guide an implementation. A useful invariant belongs to a boundary that can preserve it and is stated precisely enough to test or inspect.

Finally, don’t turn every small function into a page of formal notation. A private helper named percentageOf(total, rate) with strong types and obvious behavior may need no additional contract documentation. Contracts earn their cost when assumptions are consequential, non-obvious, or shared across a boundary.

Use contracts where assumptions are expensive to misunderstand

Design by Contract is especially useful around domain operations, reusable modules, stateful components, and interfaces with several implementations. These are places where one developer’s unstated assumption easily becomes another developer’s bug.

Start with the rules already causing defensive checks or repeated explanations. For one operation, write down:

  1. What must the caller establish before calling?
  2. What can the caller rely on after success?
  3. What state must remain valid across all operations?

Then decide how each rule should be represented. A type may encode it. A constructor may establish it. A runtime check may enforce it. A test may document examples. Public documentation may need to state it explicitly. Often the strongest design uses more than one of these without duplicating the rule blindly.

The goal isn’t to make ordinary code look formal. It is to make responsibility visible. When a failure occurs, a clear contract narrows the question from “something went wrong somewhere” to “which obligation was broken at this boundary?”

Make the next boundary clearer

Choose one operation whose callers currently rely on comments, defensive checks, or tribal knowledge. Write its preconditions, postconditions, and relevant invariants in plain language before changing any code.

If you can’t decide which side owns a condition, that uncertainty is useful information. Clarify the API first. Once responsibility is explicit, the implementation, validation strategy, tests, and failure handling usually become easier to place.