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:

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

Problems:

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

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:

assert(y>=0);
havoc(y);
assume(y=old(y)+1)