Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | |||
sav08:frame_conditions [2008/04/10 12:54] vkuncak |
sav08:frame_conditions [2008/04/10 13:18] 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 ===== |