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.