Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:correctness_of_a_g_reasoning [2008/04/10 12:46] vkuncak |
sav08:correctness_of_a_g_reasoning [2008/04/10 13:47] vkuncak |
||
|---|---|---|---|
| Line 65: | Line 65: | ||
| For relations $r$, $s$ that propagate errors (as in [[Assert and error conditions]]): | For relations $r$, $s$ that propagate errors (as in [[Assert and error conditions]]): | ||
| \[ | \[ | ||
| - | (assume(P(x)); r \subseteq s)\ \ \leftrightarrow\ \ r \subseteq assert(P(x)); s | + | assume(P) \mathop{;} r \subseteq s\ \ \leftrightarrow\ \ r \subseteq assert(P) \mathop{;} s |
| \] | \] | ||
| \[ | \[ | ||
| - | (r; assert(Q(x)) \subseteq s)\ \ \leftrightarrow\ \ r \subseteq s;assume(Q(x)) | + | r \mathop{;} assert(Q) \subseteq s\ \ \leftrightarrow\ \ r \subseteq s \mathop{;} assume(Q) |
| \] | \] | ||