LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Next revision
Previous revision
sav08:frame_conditions [2008/04/09 00:40]
vkuncak created
sav08:frame_conditions [2008/04/10 13:18]
vkuncak
Line 1: Line 1:
 ====== Frame Conditions (Modifies Clauses) ====== ====== Frame Conditions (Modifies Clauses) ======
 +
 +===== Motivation =====
  
 Example procedure with globals x,y,z which increments x. Example procedure with globals x,y,z which increments x.
 +
 +<​code>​
 +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);​
 +}
 +</​code>​
 +
 +By rules so far in verification of //test// we consider
 +
 +<​code>​
 +proc test()
 +{
 +   y = 0;
 +   x = 2;
 +
 +   var y1 = y;
 +   ​assert(y >= 0);
 +   ​havoc(x,​y,​z);​
 +   ​assume(y = y1 + 1);
 +
 +   ​assert(x==2);​
 +}
 +</​code>​
 +
 +More precise postcondition:​
 +++++|
 +<​code>​
 +proc inc()
 +requires y >= 0
 +ensures y = old(y) + 1 & x=old(x) & z=old(z)
 +{ y = y + 1; }
 +</​code>​
 +++++
 +
 +Problems:
 +  * long to write
 +  * specification must change every time we add variables
 +
 +==== Frame condition notation ====
 +
 +<​code>​
 +proc inc()
 +requires y >= 0
 +modifies y
 +ensures y = old(y) + 1
 +{ y = y + 1; }
 +</​code>​
 +
 +Note: no mention of x,z.
 +
 +Meaning is the same as above.
 +
 +Translation when analyzing procedure call:
 +++++|
 +<​code>​
 +assert(y>​=0);​
 +havoc(y);
 +assume(y=old(y)+1)
 +</​code>​
 +++++
  
 ===== Meaning of Frame Conditions as Variable Lists ===== ===== Meaning of Frame Conditions as Variable Lists =====