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:54]
vkuncak
@@ Line 61: / Line 61: @@
 \]
-=== Shunting rules ===
+===== Shunting rules =====
-Under certain 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(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)
 \]
+Proofs:
+  * using relations
+  * using weakest preconditions (see [[sav07_homework_4#rules_for_guarded_commands|homework in SAV'07]])