Preconditions and postconditions are part of routine definitions. They are optional. If present, they are automatically checked at runtime and an error is reported if a condition is not met.
Preconditions are written at the beginning of a routine body and are checked on entry of that routine. It is the responsibility of the caller to ensure that the precondition is met (i.e. that it evaluates to true on routine entry). The code inside the routine body can then safely assume that the condition is true.
Postconditions are written at the end of a routine body and are checked on exit of the routine. It is the responsibility of the routine to ensure that the postcondition is true, and the caller can assume that the condition is met on return from the routine.
BNF:
routine-body ::= routine-comment
[ pre condition ]
...
do
...
[ post condition ]
end identifier
Pre- and postconditions consist of one condition each. If multiple conditions are to be defined, they can be combined with a logical and to form one condition.
Example:
func (n: Integer, m: Integer) -> (res: Integer) is pre
n >= 0 and
m >= 1 do
... post
res <> nil end func
Both pre- and postconditions are part of the interface of a routine. Redefinitions of routines may alter these conditions only in restricted ways: preconditions may be weakened, postconditions may be strengthened. If a redefined routine does not define pre- or postconditions, the conditions of the original (parent) routine apply. If a precondition is redefined, the actual condition tested at runtime is
precondition or parent-precondition
If a postcondition is redefined, the condition tested at runtime is
postcondition and parent-postcondition
This ensures that the redefined routine guarantees at least as much as its parent.
Two special expression are available in conditions: => (implies) and the reserved word old.
Example:
post
found => index > 0
The implies symbol can be read as
if (found) then assert (index > 0)
The old expression is available only in postconditions. It is used on exit of a routine to refer to the value that an expression had on entry to that routine.
The following example ensures that the global variable num has not been altered in the routine:
Example:
doSomething (n: Integer) is pre
n <> nil post
num = old num end doSomething
It is an error to use "=>" outside of a pre- or postcondition or class invariant or to use "old" outside a postcondition.