Differences

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

--- sav08:correctness_of_a_g_reasoning [2008/04/10 13:47]
vkuncak
+++ sav08:correctness_of_a_g_reasoning [2008/04/10 13:54]
vkuncak
@@ Line 61: / Line 61: @@
 \]
-=== Shunting rules ===
+===== Shunting rules =====
-For relations $r$, $s$ that propagate errors (as in [[Assert and error conditions]]):
+Recall [[Assert and error conditions]].  We say that relation $r$ respects errors if for an error state $e$ we have $(e,x) \in r$ for all states $x$.
+For relations $r$, $s$ that respect errors, we have
 \[
      assume(P) \mathop{;} r \subseteq s\ \ \leftrightarrow\ \ r \subseteq assert(P) \mathop{;} s
@@ Line 70: / Line 72: @@
      r \mathop{;} assert(Q) \subseteq s\ \ \leftrightarrow\ \ r \subseteq s \mathop{;} assume(Q)
 \]
+Proofs:
+  * using relations
+  * using weakest preconditions (see [[sav07_homework_4#rules_for_guarded_commands|homework in SAV'07]])