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; |