Differences

This shows you the differences between two versions of the page.

--- sav08:correctness_of_a_g_reasoning [2008/04/10 12:44]
vkuncak
+++ sav08:correctness_of_a_g_reasoning [2008/04/10 13:47]
vkuncak
@@ Line 63: / Line 63: @@
 === Shunting rules ===
-Under certain 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)
 \]