Design by Contract

Design by Contract (DbC) is a software design approach introduced by Bertrand Meyer in the Eiffel programming language. It formalizes the relationship between a software component and its callers using three types of assertions: preconditions (what the caller must guarantee before calling), postconditions (what the component guarantees upon successful return), and invariants (properties that hold for the lifetime of an object). The metaphor is a legal contract — both parties have obligations, and violation by either party constitutes a bug in that party’s code.

The practical payoff is precise ownership of defects. When a precondition fails, the caller is broken — the component was invoked incorrectly. When a postcondition fails, the component is broken — it failed to deliver what it promised. Without explicit contracts, these ownership questions are resolved by convention and argument; with contracts, they are architectural facts.

The Three Contract Elements

Preconditions

Conditions that must be true when a function is called. The caller is responsible for satisfying them. The component is permitted to behave arbitrarily if a precondition is violated — this is the “garbage in, garbage out” principle made explicit.

def withdraw(account: Account, amount: float) -> None:
    assert amount > 0, "Precondition: withdrawal amount must be positive"
    assert account.balance >= amount, "Precondition: sufficient funds required"
    account.balance -= amount

Postconditions

Conditions that must be true when a function returns. The component is responsible for ensuring them. If a postcondition fails, there is a bug in the component itself.

def withdraw(account: Account, amount: float) -> None:
    initial_balance = account.balance
    # ... withdrawal logic ...
    assert account.balance == initial_balance - amount, "Postcondition: balance decreased by exactly amount"

Invariants

Properties that must hold for an object at all observable points — before and after every public method call. Invariants define what it means for an object to be in a valid state.

class BankAccount:
    def __check_invariants(self):
        assert self.balance >= 0, "Invariant: balance must never be negative"
        assert self.owner is not None, "Invariant: account must always have an owner"

Contracts in Languages Without Native Support

Most languages lack native DbC. Common approaches:

  • Assertions — assert statements disabled in production (fast, zero-overhead)
  • Guard clauses — explicit early returns with exceptions (always active)
  • Type systems — encode preconditions as types (e.g., NonNegativeFloat as a newtype)
  • Libraries — J契約 (Java), deal (Python), ts-design-by-contract (TypeScript)

DbC vs Defensive Programming

Defensive programming validates inputs at every boundary. DbC assigns responsibility: the caller validates before calling, the component trusts its preconditions. These are complementary at system boundaries (always validate external input) but DbC is cleaner for internal APIs where caller identity is known and trusted.

Key Concepts

  • Preconditions: caller’s obligation; postconditions: component’s obligation; invariants: object’s ongoing obligation
  • Contract violations are bugs in the violating party, not runtime errors to be handled gracefully
  • Assertions express contracts cheaply but are often disabled in production — consider which contracts need to be active always
  • DbC makes implicit assumptions explicit and machine-checkable
  • Single Responsibility — well-contracted components have clear, bounded responsibilities
  • Small Functions — smaller functions have simpler, more expressible contracts
  • Meaningful Names — contract violations are more diagnosable when components have clear names

References

  • Meyer, B. (1997). Object-Oriented Software Construction (2nd ed.). Prentice Hall.
  • Hunt, A., & Thomas, D. (1999). The Pragmatic Programmer. “Design by Contract.”
  • Meyer, B. (1992). Applying Design by Contract. IEEE Computer.