LARA

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:

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

One way to derive rules: use assignments to reduce parameters to changes to global state.