Post conditions state what a method guarantees to the caller. It is the method's end of the contract. Post conditions are also stated as an optional initial construct in a method.

The optional '`post`' construct of method definitions contains a boolean expression which must evaluate to true whenever the method returns; it is a fatal error if it evaluates to `false`. The expression may refer to `self` and to the method's arguments.

class VECTOR is ... norm:FLT; -- norm of the vector normalize post norm = 1.0 is ... -- Normalize the vector. The norm of the result must be 1.0 |

It is frequently useful to refer to the values of the arguments before the call, as well as the result of the method call. A problem arises because the initial argument values are no longer known by the time the method terminates, since they may have been arbitrarily modified. Also, since the post condition is outside the scope of the method body, it cannot easily refer to values which are computed before the method executes. The solution to this problem consists of using `result` expressions which provide the return value of the method and `initial` expressions which are evaluated at the time the method is invoked.

*initial expressions* may only appear in the `post` expressions of methods.

add(a:INT):INT post initial(a)>result is ... |

The argument to the initial expression must be an expression with a return value and must not itself contain `initial` expressions. When a routine is called or an iterator resumes, it evaluates each `initial` expression from left to right. When the postcondition is checked at the end, each `initial` expression returns its pre-computed value.

Result expressions are essentially a way to refer to the return value of a method in a postcondition (the post condition is outside the scope of the routine and hence cannot access variables in the routine).

sum:INT post result > 5 is ... -- Means that the value return must be > 5 |

Result expressions may only appear within the postconditions of methods that have return values and may not appear within `initial` expressions. A `result` expression returns the value returned by the routine or yielded by the iterator. The type of a `result` expression is the return type of the method in which it appears (`INT`, in the above example).

The above routine maintains an (always positive) running sum in 'sum'. Only positive numbers are added to the sum, and the result must always be bigger than the argument.

class CALCULATOR is readonly attr sum:INT; -- Always kept positive add_positive(x:INT):INT pre x > 0 post result >= initial(x) is return sum + x; end; end; |