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_2 [2007/03/20 18:42] vkuncak |
sav07_lecture_2 [2007/03/21 20:11] vaibhav.rajan |
||
|---|---|---|---|
| Line 387: | Line 387: | ||
| Accumulation of equalities. | Accumulation of equalities. | ||
| - | |||
| - | |||
| - | |||
| - | |||
| - | |||
| - | |||
| - | |||
| - | |||
| ===== Guarded command language ===== | ===== Guarded command language ===== | ||
| Line 439: | Line 431: | ||
| \begin{array}{ll} | \begin{array}{ll} | ||
| \llbracket havoc(x) \rrbracket = \{(s,s1)| \forall "y"\\ | \llbracket havoc(x) \rrbracket = \{(s,s1)| \forall "y"\\ | ||
| - | "y" \neq "x" , s("y") = s("y")\} & \textrm { Modify a variable randomly.} | + | "y" \neq "x" , s1("y") = s("y")\} & \textrm { Modify a variable randomly.} |
| \end{array} | \end{array} | ||
| </latex> | </latex> | ||