LARA

Frame Conditions (Modifies Clauses)

Motivation

Example procedure with globals x,y,z which increments x.

var x,y,z :: int;

proc inc()
requires y >= 0
ensures y = old(y) + 1
{ y = y + 1; }
   
proc test()
{
   y = 0;
   x = 2;
   inc();
   assert(x==2);
}

By rules so far in verification of test we consider

proc test()
{
   y = 0;
   x = 2;

   var y1 = y;
   assert(y >= 0);
   havoc(x,y,z);
   assume(y = y1 + 1);

   assert(x==2);
}

More precise postcondition:

Problems:

  • long to write
  • specification must change every time we add variables

Frame condition notation

proc inc()
requires y >= 0
modifies y
ensures y = old(y) + 1
{ y = y + 1; }

Note: no mention of x,z.

Meaning is the same as above.

Translation when analyzing procedure call:

Meaning of Frame Conditions as Variable Lists

Specifying Sets of Locations in Frame Conditions