Invariant
Precondition
Old expression
Postcondition
Invariant
Execution completed