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;
}

var x : int;

proc dec()
requires x > 0
ensures x <= (old x)
{ x = x - 2; }

proc Q()
{
   c1;
   dec();
   c2;
}