Preconditions

The Idea

Consider a small Wallet class:

nex> class Wallet
     create
       make(initial: Real) do
         money := initial
       end
     feature
       money: Real
       spend(amount: Real) do
         money := money - amount
       end
     end

This class works mechanically, but the routine spend is underspecified. What if amount is negative? What if amount is larger than money? The body says what the routine does, but not when it is valid to call it.

A precondition makes that explicit:

nex> class Wallet
     create
       make(initial: Real) do
         money := initial
       end
     feature
       money: Real
       spend(amount: Real)
       require
         non_negative_amount: amount >= 0.0
         enough: amount <= money
       do
         money := money - amount
       end
     end

Now the routine says two things:

• what it requires of the caller
• what computation it performs once those requirements are met

That separation — between the conditions a routine demands and the work it performs once they hold — is the beginning of disciplined software design. The contract and the computation are no longer tangled together, and each can be read on its own terms.

Reading a Precondition

Read require as “this routine may be called only if…”:

spend(amount: Real)
require
  non_negative_amount: amount >= 0.0
  enough: amount <= money
do
  money := money - amount
end

The labels non_negative_amount and enough are names for the individual assertions. Choosing these names carefully is important because when a contract fails, Nex reports the assertion by name.

Bad names:

• check1
• test
• condition

Good names:

• amount_positive
• customer_exists
• index_in_bounds
• source_has_funds

The expression after the colon is the actual rule. The name is documentation; the expression is enforcement.

Caller Responsibility

When a routine has a precondition, satisfying it is the caller’s job — a point that is easy to state and easy to forget. Many beginners write routines that both require something and then, inside the body, also try to defend themselves against the caller violating that same requirement:

withdraw(amount: Real): Boolean
require
  enough: amount <= balance
do
  if amount <= balance then
    balance := balance - amount
      result := true
    else
      result := false
  end
end

The if duplicates the contract. If amount > balance, the call is already invalid. The body does not need to ask again. Duplicating the check weakens the design because it blurs the boundary between correct use and incorrect use.

The cleaner version:

withdraw(amount: Real)
require
  non_negative_amount: amount >= 0.0
  enough: amount <= balance
do
  balance := balance - amount
end

Now the routine is simpler and its interface is sharper. Either the caller meets the contract, or the call is rejected.

A First Useful Example

Here is a routine that returns the largest element of an integer array:

nex> function max_of(items: Array[Integer]): Integer
     require
       not_empty: items.length > 0
     do
       result := items.get(0)
       across items as item do
         if item > result then
           result := item
         end
       end
     end

Without the precondition, the call items.get(0) is suspicious. With the precondition, the suspicion is removed. The routine states exactly why that access is safe.

nex> max_of([4, 8, 2, 9, 1])
9

If the caller violates the contract:

nex> max_of([])
Error: Precondition violation: not_empty

The failure occurs at the boundary where the mistake was made. That is the practical value of contracts: errors are reported where they originate, not later after damage has spread.

Preconditions Are Not Input Validation

It is important to distinguish two different situations. In the first, the caller has made a programming error: it invoked a routine without meeting the rules that routine plainly depends on. In the second, the outside world has handed the program uncertain data — a value read from a file, say, or a message arriving over the network. Preconditions are for the first case. They describe the obligations between one routine and another inside a program, where both sides are code under the author’s control.

Suppose a routine computes the square root of a number:

nex> function positive_root(x: Real): Real
     require
       non_negative: x >= 0.0
     do
       result := x ^ 0.5
     end

This is appropriate if positive_root is an internal routine in a program whose callers are expected to know the rule. But if the number came from a file or a user typing at a prompt, that is not a contract problem yet. The program must first inspect the external data and decide what to do with it, because the uncertainty belongs at the program boundary. Only once the data has been accepted and checked can the internal routines downstream rely on contracts.

In short:

• use require for programmer obligations
• use ordinary control flow for uncertain real-world input

Strengthening a Design with Preconditions

Consider a bounded stack:

nex> class Bounded_Stack [G]
     create
       make(limit: Integer) do
         max_size := limit
         items := []
       end
     feature
       max_size: Integer
       items: Array[G]
       push(value: G)
       require
         not_full: items.length < max_size
       do
         items.add(value)
       end
       pop(): G
       require
         not_empty: items.length > 0
       do
         result := items.get(items.length - 1)
         items.remove(items.length - 1)
       end
       size(): Integer do
         result := items.length
       end
     end

Earlier, Chapter 15 showed a version of push that silently ignored extra insertions. That design is convenient but weak. It hides mistakes. A caller can believe the item was pushed even when it was not.

The version above is stricter and better. If the stack is full, the caller learns immediately that the call was invalid. A routine should not quietly proceed when its fundamental assumptions have been broken.

Writing Good Preconditions

A good precondition has three properties. It is necessary: it requires no more than the routine actually needs, so callers are not burdened with obligations that do not matter to the computation. It is precise: it states a definite, inspectable rule rather than a vague gesture such as valid_input: true. And it is checkable: the caller can actually tell, before making the call, whether the obligation has been met.

For example, this precondition is too weak:

require
  okay: amount /= 0.0

This one is better:

require
  positive_amount: amount > 0.0
  enough: amount <= balance

The second version says exactly what the routine needs and nothing more. A related mistake is to require a consequence instead of a cause. If a routine sorts an array, its precondition should not be array_is_sorted — that describes the result the routine is supposed to produce, not the obligation the caller must satisfy beforehand. Preconditions talk about the state that must hold before execution begins, never about the state the routine itself will go on to establish.

A Worked Example: Transfer Between Accounts

Here is a simple account class:

nex> class Account
     create
       make(name: String, initial: Real) do
         owner := name
         balance := initial
       end
     feature
       owner: String
       balance: Real
       deposit(amount: Real)
       require
         positive_amount: amount > 0.0
       do
         balance := balance + amount
       end
       withdraw(amount: Real)
       require
         positive_amount: amount > 0.0
         enough: amount <= balance
       do
         balance := balance - amount
       end
       transfer_to(other: Account, amount: Real)
       require
         positive_amount: amount > 0.0
         enough: amount <= balance
         different_account: other /= this
       do
         withdraw(amount)
         other.deposit(amount)
       end
     end

transfer_to expresses its rules cleanly:

• the amount must be positive
• the source account must contain enough funds
• the destination must not be the same object

The body is then straightforward.

nex> let checking := create Account.make("Checking", 150.0)
nex> let savings  := create Account.make("Savings", 80.0)

nex> checking.transfer_to(savings, 50.0)
nex> checking.balance
100.0

nex> savings.balance
130.0

The routine is short because the contract does most of the explanatory work. Anyone reading transfer_to learns its rules from the require clause rather than from defensive checks scattered through the body.

Summary

• A precondition states what must be true before a routine may be called
• require clauses define the caller’s obligations, not the routine’s promises
• If a precondition is violated, the caller is wrong; the routine is not required to compensate
• Good precondition names document intent and improve error messages
• A good precondition asks for no more than the routine needs, and the caller can check it before calling
• Use contracts for programming obligations inside the system, not for uncertain external input
• A routine with a clear precondition usually has a simpler body

Exercises

1. Write a function average(items: Array[Real]): Real with an appropriate precondition. The routine should return the arithmetic mean of the array elements. Test it on a non-empty array, then deliberately violate the contract with [].

2. Define a class Temperature_Log with an array field readings: Array[Real], a constructor that starts with an empty array, and a method latest(): Real with a precondition that the log is non-empty. Add a method record(value: Real) that appends a reading.

3. Rewrite the Queue[G] class from Chapter 15 so that dequeue and front each have a precondition not_empty. Remove any duplicated emptiness checks from the method bodies.

4. Consider a function substring(s: String, start, finish: Integer): String. Write a plausible set of preconditions for it. Explain in one or two sentences why each is the caller’s responsibility.

5.* A routine transfer_to(other: Account, amount: Real) already requires amount > 0.0 and amount <= balance. Is other /= this always a necessary precondition? Argue both sides, then decide whether it should be a contract or simply an allowed no-op in your design.