Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav07_lecture_3_skeleton [2007/03/21 11:01] vkuncak |
sav07_lecture_3_skeleton [2007/03/21 11:02] vkuncak |
||
|---|---|---|---|
| Line 25: | Line 25: | ||
| R( c ) -> error=false | R( c ) -> error=false | ||
| + | |||
| Line 38: | Line 39: | ||
| R(havoc x) = frame(x) | R(havoc x) = frame(x) | ||
| - | R(assume F) = F[x:=x_0, y:=y_0, error:=error_0] | + | R(assume F) = F[x:=x_0, y:=y_0, error:=error_0] & frame() |
| R(assert F) = (F -> frame) | R(assert F) = (F -> frame) | ||