Example 11-2. Example:
add(a: INT):INT post initial(a) > result is ... |
initial_expression ==>
initial ( expression ) |
initial expressions may only appear in the post expressions of methods. The expression must have a return value and must not itself contain initial expressions. When a routine is called or an iterator resumes, it evaluates the expression of each initial expression from left to right. When the postcondition is checked at the end, each initial expression returns its pre-computed value.