Differences

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

--- sav08:correctness_of_a_g_reasoning [2008/04/10 13:54]
vkuncak
+++ sav08:correctness_of_a_g_reasoning [2015/04/21 17:30]
@@ Line 1: / Line 1: @@
-====== Correctness of A/G Reasoning ======
-===== Correctness as Approximation of Relations =====
-Specification $s$ provides a relation that is intended to approximate relation $r$ defining the meaning of procedure, that is, we would like to prove
-\[
-    r \subseteq s
-\]
-Following [[Relational Semantics of Procedures]], consider one procedure and its associated function
-\[
-    m : {\cal R} \to {\cal 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
-\[
-     m(s) \subseteq s
-\]
-We claim that $r_* \subseteq s$ where $r_* = \bigcup_{k \ge 0} m^k(\emptyset)$.
-**Proof:**
-++++|
-Indeed, $\emptyset = r_0 \subseteq s$, and by monotonicity of $m$ we obtain that $r_n \subseteq s$ implies $r_{n+1} \subseteq m(s) \subseteq s$.  Therefore, $r_n \subseteq s$ for all $n$, so $r_* \subseteq s$.
-Informally, the reason that this reasoning follows by induction is that if we consider any execution of the procedure (which then belongs to $r_n$) we can show by induction starting from innermost call.  The innermost call has no recursive invocation, so it presents the base case of induction.
-++++
-===== Expressing Approximation Using Assume and Assert =====
-Consider a program with only one state variable $x$.
-We express our approximation as
-\[
-   \begin{array}{l}
-     assert\, (P(x));\\
-     havoc(x); \\
-     assume(Q(x))
-   \end{array}
-\]
-So, we would like to show that
-\[
-    r\qquad \subseteq\qquad
-   \begin{array}{l}
-     (assert\, (P(x));\\
-     havoc(x); \\
-     assume\, (Q(x)))
-   \end{array}
-\]
-is implied by the condition we are checking:
-\[
-   \begin{array}{l}
-     (assume\, (P(x));\\
-     r; \\
-     assert\, (Q(x)))
-   \end{array}
-   \qquad\subseteq \qquad
-   havoc(x)
-\]
-===== Shunting rules =====
-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
-\]
-\[
-     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]])