LARA

Differences

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

Link to this comparison view

Both sides previous revision Previous revision
sav08:frame_conditions [2008/04/10 12:54]
vkuncak
sav08:frame_conditions [2008/04/10 13:18] (current)
vkuncak
Line 39: Line 39:
 </​code>​ </​code>​
  
-Strongest ​postcondition:​+More precise ​postcondition:​
 ++++| ++++|
 <​code>​ <​code>​
Line 64: Line 64:
  
 Note: no mention of x,z. 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 =====