Differences
This shows you the differences between two versions of the page.
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 ===== |