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) |
\] | \] | ||