This is an old revision of the document!
Assume Guarantee Reasoning with Procedures
Procedures without parameters or results
Given
var x;
proc P() requires Pre(x) ensures Post(x) { c }
Suppose we verify
proc Q() { c1; P(); c2; }
We will reduce it to:
Postconditions that refer to pre state
proc dec(x) requires x > 0 ensures x <= (old x) { x = x - 2; }
proc Q() { c1; dec(); c2; }