Postconditions

The Idea

Here is a deposit routine without a postcondition:

deposit(amount: Real)
require
  positive_amount: amount > 0.0
do
  balance := balance + amount
end

The body suggests the intended effect, but the routine does not state its guarantee explicitly. A postcondition adds that missing half:

deposit(amount: Real)
require
  positive_amount: amount > 0.0
do
  balance := balance + amount
ensure
  increased: balance = old balance + amount
end

Read ensure as “after this routine finishes successfully, the following must be true.” The label increased names the guarantee, and the expression that follows compares the new value of balance with the value it held before the routine began.

The old Keyword

Postconditions often need to talk about both the state after execution and the state before execution. That is the role of old.

ensure
  decreased: balance = old balance - amount

old balance means the value of balance at routine entry. Without old, many useful guarantees would be impossible to state cleanly.

old applies to a whole expression, not only to a field. Nex evaluates the expression once, when the routine is entered (just after the precondition is checked), and remembers its value. So old works just as well on a query or on another object:

ensure
  size_increased: items.length = old items.length + 1
  one_more: count() = old count() + 1
  receiver_gained: other.balance = old other.balance + amount

If evaluating an old expression on entry fails, for example old items.get(0) on an empty array, Nex doesn’t fail the call straight away. It remembers the failure and raises it only if the postcondition actually reads that value. So old items.length > 0 implies items.get(0) = old items.get(0) is a safe way to say “the first element is unchanged, if there was one”. (implies, from Chapter 3, never reads its right side when its left side is false.)

old covers the whole chain of calls after it: old other.balance means old (other.balance). It stops at the first operator, so old balance - amount means (old balance) - amount.

Keep in mind what is remembered. old keeps the value of its expression. When that value is an object, it keeps the object, not a copy of it. So old other is just other, and (old other).balance reads the balance now. To talk about an object’s earlier state, put the query under old: old other.balance. Arrays and maps are the one exception: old items remembers which elements the collection held on entry, so (old items).length is the earlier length too.

For example:

nex> class Counter
     create
       make() do
         count := 0
       end
     feature
       count: Integer
       increment()
       do
         count := count + 1
       ensure
         advanced: count = old count + 1
       end
     end

The postcondition does not describe the code line by line. It describes the observable result: after increment, the count is exactly one larger than before.

Routine Responsibility

A precondition is the caller’s responsibility; a postcondition is the routine’s. The consequence is: if a call satisfies its precondition but the postcondition is then violated, the bug lies inside the routine or in the code it calls, and the fault is not with the caller.

Suppose we write:

nex> class Counter
     create
       make() do
         count := 0
       end
     feature
       count: Integer
       increment()
       do
         count := count + 2
       ensure
         advanced: count = old count + 1
       end
     end

Then:

nex> let c := create Counter.make
nex> c.increment
Error: Postcondition violation: advanced

The postcondition catches the bug at the exact routine that introduced it, rather than letting a wrong count propagate silently into whatever code later relied on it.

Weak and Strong Postconditions

Not all postconditions are equally useful. This one, for instance, is almost worthless:

ensure
  changed: balance /= old balance

It says only that the balance changed. It does not say by how much or in which direction. A deposit routine that subtracted the amount instead of adding it could still satisfy this contract.

This one is better:

ensure
  increased: balance = old balance + amount

It is precise: it rules out the wrong implementations and captures the intended effect exactly. As a rule, prefer postconditions that express the specific relation between inputs, old state, and new state, because a weak postcondition documents very little and catches very few bugs.

Return Values and Postconditions

Postconditions apply to query routines as much as to commands. Consider a function that returns the larger of two integers:

nex> function max(a, b: Integer): Integer 
     do
       if a >= b then
         result := a
       else
         result := b
       end
     ensure
       result_is_one_argument: result = a or result = b
       result_is_at_least_a: result >= a
       result_is_at_least_b: result >= b
     end

The postconditions specify the meaning of the result:

• it must equal one of the arguments
• it must not be smaller than either argument

The body could be rewritten in many ways, but any correct implementation must satisfy those rules.

Some results mean different things in different cases, and the postcondition has to say what each case guarantees. A search that returns the position of a value, or -1 when the value is absent, makes one promise when it finds the value and another when it doesn’t. implies states each promise for its own case:

nex> function position(xs: Array[Integer], target: Integer): Integer
     do
       result := -1
       from
         let i := 0
       until
         i = xs.length or result /= -1
       do
         if xs.get(i) = target then
           result := i
         end
         i := i + 1
       end
     ensure
       in_range: result >= -1 and result < xs.length
       found_means_here: result >= 0 implies xs.get(result) = target
       missing_means_absent: result = -1 implies not xs.contains(target)
     end

nex> position([4, 8, 15, 16], 15)
2

nex> position([4, 8, 15, 16], 23)
-1

Read each clause as a sentence: if the result is a position, the target is there; if the result is -1, the target is nowhere in the array. Each clause only applies in its own case, so neither gets in the way of the other. found_means_here is also safe on the -1 path: when its left side is false, implies doesn’t evaluate xs.get(result), which would fail for -1.

Without implies, the same promise is written result < 0 or xs.get(result) = target. It means the same thing, but the reader has to turn it around to see the rule.

Postconditions and Helper Routines

Good postconditions also make routines easier to compose. Return to the Account class:

nex> class Account
     create
       make(initial: Real) do
         balance := initial
       end
     feature
       balance: Real
       deposit(amount: Real)
       require
         positive_amount: amount > 0.0
       do
         balance := balance + amount
       ensure
         increased: balance = old balance + amount
       end
       withdraw(amount: Real)
       require
         positive_amount: amount > 0.0
         enough: amount <= balance
       do
         balance := balance - amount
       ensure
         decreased: balance = old 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)
       ensure
         sender_lost_amount: balance = old balance - amount
         receiver_gained_amount: other.balance = old other.balance + amount
       end
     end

The postconditions on withdraw and deposit explain why transfer_to is trustworthy. The postcondition on transfer_to then states the exact effect on both accounts. old other.balance is the destination’s balance when transfer_to was entered, because old evaluates its whole expression on entry, including a query on a parameter. Contracts accumulate in this way, and a system of small, precise routines is far easier to reason about than a system of large, vague ones.

Choosing the Right Level of Detail

A postcondition should describe what the caller can rely on. It should not repeat every assignment from the body.

For example, this is too implementation-specific:

ensure
  x_set: x = px
  y_set: y = py
  local_was_used: true

The last line says nothing useful. A caller of a point constructor cares that the point’s coordinates equal the arguments, not whether the implementation used a temporary local variable along the way.

By contrast, for a sorting routine the right postcondition is not “the routine compared elements many times.” It is something like:

• the result has the same length as the input
• the result is in non-decreasing order
• every original element still appears in the result

That is what the caller needs to know — the properties the result is guaranteed to have, stated independently of how the sorting was actually carried out.

A Worked Example: Removing the Last Stack Element

Here is a stack with both preconditions and postconditions:

nex> class Stack [G]
     create
       make() do
         items := []
       end
     feature
       items: Array[G]
       push(value: G)
       do
         items.add(value)
       ensure
         last_is_value: items.get(items.length - 1) = value
       end
       pop(): G
       require
         not_empty: items.length > 0
       do
         result := items.get(items.length - 1)
         items.remove(items.length - 1)
       ensure
         length_decreased_by_one: items.length = old items.length - 1
       end
     end

The postcondition on pop is particularly good because it specifies both effects:

• the stack becomes shorter by one
• the returned value is exactly the element that used to be last

That is the behavior the caller cares about. The internal array representation is almost irrelevant.

Summary

• A postcondition states what a routine guarantees after successful completion
• ensure clauses define the routine’s responsibility
• old refers to values from routine entry and is essential for expressing state change
• Strong postconditions describe precise effects, not vague change
• Query routines can and should have postconditions too
• implies states a guarantee that applies only in some cases: result >= 0 implies xs.get(result) = target
• Good postconditions make routines easier to compose and reason about
• A postcondition should describe the externally meaningful result, not internal implementation trivia

Exercises

1. Add a postcondition to the average(items: Array[Real]): Real routine from Chapter 16. The postcondition should state at least one useful fact about the result relative to the input.

2. Define a class Lamp with a Boolean field is_on, a constructor that starts it in the false state, and methods switch_on and switch_off. Add postconditions showing the effect of each routine.

3. Write a function absolute_value(x: Integer): Integer and give it a postcondition strong enough to rule out both result := x and result := -x as universally correct implementations.

4. Extend the Queue[G] class so that enqueue(value: G) has a postcondition describing the new size and the value at the back of the queue.

5.* A routine sort(items: Array[Integer]): Array[Integer] returns a new sorted array. Write three postconditions for it: one about length, one about order, and one about preservation of elements. You do not need to implement the routine; focus on the specification.