Invariant
Precondition
Old expression
In TEST1 make
0
Postcondition
Invariant
Execution completed