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