Contracts as a Design Tool

2.1 The Four Forms

Nex builds contracts into the ordinary routine and class forms, not into a separate assertion library. There are four:

• require — a precondition: what must be true for the caller to invoke this routine at all.
• ensure — a postcondition: what the routine guarantees on exit, provided its precondition held.
• invariant — a standing property of an object that holds before and after every one of its operations, or a property preserved across every turn of a loop.
• variant — a quantity that strictly decreases toward a bound, used to prove that a loop or recursion terminates.

Here is an account that uses the first three. Read the contracts first and the body second — that is the order in which they were designed.

class Account
  create
    open(initial: Money)
      require
        non_negative_open: initial >= Money.zero
      do
        balance := initial
      end

  feature
    balance: Money

    withdraw(amount: Money)
      require
        positive: amount > Money.zero
        sufficient_funds: amount <= balance
      do
        balance := balance - amount
      ensure
        balance_reduced: balance = old balance - amount
        never_negative: balance >= Money.zero
      end

    deposit(amount: Money)
      require
        positive: amount > Money.zero
      do
        balance := balance + amount
      ensure
        balance_grew: balance = old balance + amount
      end

  invariant
    solvent: balance >= Money.zero
end

Every clause has a name — sufficient_funds, never_negative, solvent — and the names are not decoration. They are the vocabulary of the design. When a contract is violated at runtime, the failure reports which named claim broke, so a bug announces itself in domain language rather than as an anonymous stack trace. Writing the name forces you to say, in words, what you believe — and half the value of a contract is extracted at the moment you are forced to name it, long before it ever runs.

2.2 The Precondition Is a Specification

Look again at withdraw. Its precondition says amount <= balance. A defensive programmer would instead write the check inside the body — if amount > balance then return error — and hand the caller a failure to inspect. The contract makes the opposite choice, and the difference is the whole point.

A precondition is a statement about whose responsibility a condition is. By writing require sufficient_funds: amount <= balance, the routine declares: establishing this is the caller's job, not mine. Inside the body, the routine may then treat sufficiency as a fact. It does not re-check; it does not branch; it does not return an error for the case, because the case is not its to handle. The contract has moved the obligation across the boundary and, in doing so, has made the body simpler and the caller's duty explicit.

This is what it means to say a precondition is a specification rather than an assertion. An assertion asks, "is this true right now?" A specification asks, "who must make this true, and who may assume it?" The first is a runtime event. The second is a design decision — a division of labour written into the interface — and it holds whether or not the check ever executes.

2.3 Postconditions, and the Word old

Where a precondition binds the caller, a postcondition binds the routine. ensure balance_reduced: balance = old balance - amount promises that, if you met the precondition, the balance afterward is exactly the balance before minus the amount — no rounding drift, no fee sneaked in, no forgotten path that leaves the balance untouched.

The keyword old refers to the value an expression had on entry, before the body ran. It is what lets a postcondition talk about change rather than just about the final state: not merely "the balance is non-negative" but "the balance moved by precisely this much." That distinction is where a whole class of quiet arithmetic bugs would otherwise live. A postcondition with old is a promise about the transition, and transitions are exactly what the order core of our running system must never get wrong.

Notice how the two halves cooperate. The precondition lets the body assume; the postcondition obliges the body to deliver. Together they form a complete specification of the routine that a reader can trust without reading the body at all — which is precisely what you want at the seams of a large system, where you compose routines you did not write and will not re-read.

2.4 Invariants: The Object's Standing Promise

A precondition and postcondition describe a single routine. An invariant describes the whole object, across its entire lifetime. The Account's invariant, solvent: balance >= Money.zero, is a promise that holds after construction and after every method — that there is no sequence of legal operations, however long, that can leave an account with a negative balance.

This is a stronger and more useful claim than any single postcondition, because it is closed under composition. Each method must both assume the invariant on entry and re-establish it on exit; in exchange, no method ever has to worry about receiving an object in a broken state. The invariant is the object's contract with itself, and it is the constraint tradition of Chapter 1 in its most local form: a standing narrowing of what states the object may occupy, enforced at every step rather than hoped for.

When we model the order core in Part II, its invariants will carry most of the correctness argument — a placed order's total equals the sum of its lines, a shipped order has a tracking id, and so on. The invariant is where "make illegal states unrepresentable" lands for a mutable object: the states are still reachable in memory, but the invariant forbids the object from ever resting in one.

2.5 Variants: Promising an End

The fourth form addresses a hardness the other three do not touch: not correctness but termination. A loop can preserve every invariant and satisfy every postcondition and still never stop. A variant is an integer quantity, bounded below, that must strictly decrease on every iteration — and a quantity that only ever goes down and cannot go below its bound cannot decrease forever, so the loop must end.

-- Sum a list of line totals. The variant proves the loop terminates.
function sum_totals(items: Array[Money]): Money
  do
    from
      let i: Integer := 0
      result := Money.zero
    invariant
      in_range: 0 <= i and i <= items.length
    variant
      items.length - i
    until
      i >= items.length
    do
      result := result + items.get(i)
      i := i + 1
    end
  end

The variant here is items.length - i. It starts at the list's length, drops by one each turn as i rises, and cannot fall below zero because the loop stops when i reaches the length. Stating it forces you to name why the loop ends — and, as with preconditions, most of the value arrives at the moment of naming. A loop whose variant you cannot write is a loop whose termination you do not actually understand.

2.6 Contracts as the Membrane

Everything so far has shown contracts guarding a single object. Their deeper role in this book is guarding a boundary — the seam where an open edge hands a value to a constrained core.

Recall the arrangement from Chapter 1: the pricing engine is deliberately open, so that new rules can be added without the core knowing they exist. But that openness has a cost. When some rule the core has never heard of produces a price, the compiler cannot vouch for it — the rule was designed to live outside the compiler's knowledge. The type system, which guards the doors we can name in advance, has nothing to say about a value arriving from a door left open on purpose. This is exactly the moment types fall silent.

A contract speaks where the type is silent. The core exposes a boundary routine whose precondition states precisely what any price must satisfy to be admitted — regardless of which rule produced it:

-- The core accepts a quote from the open pricing edge — but only on its terms.
apply_quote(order: Placed, quote: Money)
  require
    priced_in_order_currency: quote.currency = order.total.currency
    non_negative: quote >= Money.zero
    not_below_floor: quote >= order.floor_price
  do
    order.set_total(quote)
  ensure
    total_is_quote: order.total = quote
    still_valid: order.is_consistent
  end

Any pricing rule at all may compute quote — a promotion, a loyalty tier, something invented next year. The core does not know and does not care. What it insists on is the contract at the doorway: the quote is in the right currency, not negative, not below the order's floor. The rule's author, on the other side of the membrane, reads the same precondition and knows exactly what they must deliver for their price to be accepted. Neither side has to see inside the other. The precondition is the interface between a discipline of openness and a discipline of constraint.

This is the pattern the whole book turns on. In Part IV, when we step outside the type system into generic dispatch, and in Part V, when computation runs on partial information, the type checker will fall silent again and again — and each time, a contract will take over the guarding. That recurrence is what makes constraint and flexibility one story rather than two. With the tool in hand, we can now go and constrain the core. The next part begins where correctness begins: making illegal states impossible to write down.