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. They matter. When a contract fails, Nex reports the assertion by name. A good assertion name tells the reader what rule was intended.

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, a field typed by a user, 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, a network request, 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
• Preconditions should be necessary, precise, and checkable
• 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 14 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.