11.4. result expressions

Example 11-3. Example:

sum: INT
   post result > 5 is ...
result_expression ==>
        result

result expressions may only appear within the postconditions of methods that have return values and may not appear within initial expressions. They return the value returned by the routine or yielded by the iterator. Their type is the return type of the method in which they appear.