Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
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 | 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) | 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]]) | ||