Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
sav08:correctness_of_a_g_reasoning [2008/04/10 13:47] vkuncak |
sav08:correctness_of_a_g_reasoning [2015/04/21 17:30] (current) |
||
|---|---|---|---|
| Line 4: | Line 4: | ||
| Specification $s$ provides a relation that is intended to approximate relation $r$ defining the meaning of procedure, that is, we would like to prove | Specification $s$ provides a relation that is intended to approximate relation $r$ defining the meaning of procedure, that is, we would like to prove | ||
| - | \[ | + | \begin{equation*} |
| r \subseteq s | r \subseteq s | ||
| - | \] | + | \end{equation*} |
| Following [[Relational Semantics of Procedures]], consider one procedure and its associated function | Following [[Relational Semantics of Procedures]], consider one procedure and its associated function | ||
| - | \[ | + | \begin{equation*} |
| m : {\cal R} \to {\cal R} | m : {\cal R} \to {\cal R} | ||
| - | \] | + | \end{equation*} |
| and its fixed point $r_*$. | and its fixed point $r_*$. | ||
| The idea of approach based on specifications is to prove that, if we assume that procedure calls satisfy the specification, then we can prove the specification for the procedure we are verifying. In other words, specifications provide a relation $s$ such that | The idea of approach based on specifications is to prove that, if we assume that procedure calls satisfy the specification, then we can prove the specification for the procedure we are verifying. In other words, specifications provide a relation $s$ such that | ||
| - | \[ | + | \begin{equation*} |
| m(s) \subseteq s | m(s) \subseteq s | ||
| - | \] | + | \end{equation*} |
| We claim that $r_* \subseteq s$ where $r_* = \bigcup_{k \ge 0} m^k(\emptyset)$. | We claim that $r_* \subseteq s$ where $r_* = \bigcup_{k \ge 0} m^k(\emptyset)$. | ||
| Line 33: | Line 33: | ||
| We express our approximation as | We express our approximation as | ||
| - | \[ | + | \begin{equation*} |
| \begin{array}{l} | \begin{array}{l} | ||
| assert\, (P(x));\\ | assert\, (P(x));\\ | ||
| Line 39: | Line 39: | ||
| assume(Q(x)) | assume(Q(x)) | ||
| \end{array} | \end{array} | ||
| - | \] | + | \end{equation*} |
| So, we would like to show that | So, we would like to show that | ||
| - | \[ | + | \begin{equation*} |
| r\qquad \subseteq\qquad | r\qquad \subseteq\qquad | ||
| \begin{array}{l} | \begin{array}{l} | ||
| Line 49: | Line 49: | ||
| assume\, (Q(x))) | assume\, (Q(x))) | ||
| \end{array} | \end{array} | ||
| - | \] | + | \end{equation*} |
| is implied by the condition we are checking: | is implied by the condition we are checking: | ||
| - | \[ | + | \begin{equation*} |
| \begin{array}{l} | \begin{array}{l} | ||
| (assume\, (P(x));\\ | (assume\, (P(x));\\ | ||
| Line 59: | Line 59: | ||
| \qquad\subseteq \qquad | \qquad\subseteq \qquad | ||
| havoc(x) | havoc(x) | ||
| - | \] | + | \end{equation*} |
| - | === 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 | ||
| + | \begin{equation*} | ||
| 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 | ||
| - | \] | + | \end{equation*} |
| - | \[ | + | \begin{equation*} |
| 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) | ||
| - | \] | + | \end{equation*} |
| + | |||
| + | Proofs: | ||
| + | * using relations | ||
| + | * using weakest preconditions (see [[:sav07_homework_4#rules_for_guarded_commands|homework in SAV'07]]) | ||