Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav07_lecture_18 [2007/05/28 22:41] vasu.singh |
sav07_lecture_18 [2007/05/28 22:48] vasu.singh |
||
---|---|---|---|
Line 27: | Line 27: | ||
This suggests that the two programs above are not equivalent for the purpose of reasoning | This suggests that the two programs above are not equivalent for the purpose of reasoning | ||
in concurrently executing programs. | in concurrently executing programs. | ||
+ | |||
+ | |||
Line 67: | Line 69: | ||
An example | An example | ||
+ | |||
+ | { b = x + y } | ||
+ | while (*) do | ||
+ | if (*) then | ||
+ | x++; | ||
+ | y--; | ||
+ | else | ||
+ | y++; | ||
+ | x--; | ||
+ | endif | ||
+ | end | ||
+ | || | ||
+ | |||
+ | while (*) do | ||
+ | if (*) then | ||
+ | x++; | ||
+ | y--; | ||
+ | else | ||
+ | y++; | ||
+ | x--; | ||
+ | endif | ||
+ | end | ||
+ | { b = x + y } | ||
==== Global reachability invariants ==== | ==== Global reachability invariants ==== |