Design by contract

Precondition, postcondition, invariant — and the main thing that follows from them: who is at fault. A violated precondition is the caller's bug: it can occur in a correct program, is always checked, and is answered with an exception. A violated invariant is your own bug and a sign of already-corrupted state: you cannot carry on, hence assert or panic rather than a tidy error return (25).

The term and the discipline are Bertrand Meyer’s: Eiffel builds require, ensure and invariant into the language, and his “Applying ‘Design by Contract’” (IEEE Computer, 1992) and Object-Oriented Software Construction set out the method. The logic underneath is Hoare’s 1969 “An Axiomatic Basis for Computer Programming”: a triple {P} S {Q} says that if P holds before S, Q holds after. Meyer added the part that matters for teams — a contract is a division of responsibility. The caller guarantees the precondition, so the callee need not defend against it twice; the callee guarantees the postcondition, so the caller need not recheck it. His rule for subclasses — a precondition may only be weakened, a postcondition only strengthened — is the precise form of Liskov substitution (1).

// Objects.requireNonNull + explicit invariants in the constructor; assert for internal ones
public record Transfer(Account from, Account to, Cents amount) {
    public Transfer {
        Objects.requireNonNull(from); Objects.requireNonNull(to);
        if (amount.value() <= 0) throw new IllegalArgumentException("amount must be > 0");
        if (from.equals(to)) throw new IllegalArgumentException("self-transfer");
    }
}

// debug_assert! on internal invariants — free in release
fn apply(&mut self, entry: LedgerEntry) {
    debug_assert!(self.is_balanced(), "ledger invariant broken before apply");
    // ...
    debug_assert!(self.is_balanced(), "apply broke double-entry invariant");
}

// TigerBeetle style — cheap invariant checks stay on in production
func (l *Ledger) Apply(e Entry) error {
    if l.debits != l.credits { // double-entry invariant, always on
        panic("ledger corrupted: unbalanced before apply") // corrupted state = crash-only
    }
    ...
}

# assert for invariants (stripped by -O), exceptions for preconditions
def apply(self, entry: LedgerEntry) -> None:
    if entry.amount <= 0:
        raise ValueError("precondition: amount > 0")   # caller's bug
    assert self._is_balanced(), "invariant broken"     # my bug

The ledger example, and its costs. “Debits equal credits” is the invariant of a double-entry ledger; checking it before and after every apply turns silent corruption into a crash at the line that caused it, which is the whole point. TigerBeetle’s style guide keeps dense assertions on in production for that reason. Whether you can afford that is a measurement: an O(1) balance check is free, an O(n) scan of the ledger on every write is not. Know what your platform does by default — Java assert is off unless the JVM runs with -ea, Python strips assert under -O, Rust’s debug_assert! disappears in release — so a check that must always run is written as an ordinary if with a panic.

Where contracts end. Across a process or network boundary the caller is not a cooperating part of your program, so a precondition there is not “the caller’s bug” but input to parse (2, 32) and an error to return (4). A precondition the type system can carry should move into the type (3): a PositiveCents needs no runtime check at each call.