Differences

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

--- sav08:forward_vcg [2010/03/09 17:23]
vkuncak
+++ sav08:forward_vcg [2015/04/21 17:30]
@@ Line 1: / Line 1: @@
-====== Forward VCG: Using Strongest Postcondition ======
-If $P$ is a formula on state and $c$ a command, let $sp_F(P,c)$ the formula version of strongest postcondition operator.  $sp_F(P,c)$ is therefore formula $Q$ that describes the set of states that can result from executing $c$ in a state satisfying $P$.
-Thus, we have
-\[
-   sp(\{s.\ f_T(P)(s)\}, r_c(c_1)) = \{ s.\ f_T(sp_F(P,c_1))(s) \}
-\]
-or, less formally,
-\[
-   sp(\{s.\ P\}, r_c(c_1)) = \{ s.\ sp_F(P,c_1) \}
-\]
-For a predicate $P$, let $P_s$ be the set of states that satisfies it,
-\[
-P_s = \{s.\ f_T(P)(s) \}
-\]
-===== Rules for Computing Strongest Postcondition =====
-=== Assume Statement ===
-Define:
-\[
-   sp_F(P, assume(F)) = P \wedge F
-\]
-Then
-\[
-\begin{array}{l}
-   sp(P_s, assume(F)) \\
-   = sp(P_s, \Delta_{F_s}) \\
-   = \{s' | \exists s \in P_s.((s,s') \in \Delta_{F_s})\} \\
-   = \{s' | \exists s \in P_s.(s=s' \wedge s \in F_s)\} \\
-   = \{s' | s' \in P_s, s' \in F_s\} = P_s \cap F_s.
-\end{array}
-\]
-=== Havoc Statement ===
-Define:
-\[
-   sp_F(P,\mbox{havoc}(x)) = \exists x_0. P[x:=x_0]
-\]
-=== Assignment Statement ===
-Define:
-\[
-   sp_F(P, x = e) = \exists x_0.(P[x:=x_0] \land x=e[x:=x_0])
-\]
-Indeed:
-\[
-\begin{array}{l}
-   sp(P_s, r_c(x = e)) \\
-   = \{s'| \exists s.(s \in P_s \wedge (s, s') \in r_c(x=e))\} \\
-   = \{s'| \exists s.(s \in P_s \wedge s' = s[x \rightarrow f_T(e)(s)]) \}
-\end{array}
-\]
-=== Sequential Composition ===
-For relations we proved
-\[
-   sp(P_s,r_1 \circ r_2) = sp(sp(P_s,r_1),r_2)
-\]
-Therefore, define
-\[
-   sp_F(P,c_1;c_2) = sp_F(sp_F(P,c_1),c_2)
-\]
-=== Nondeterministic Choice (Branches) ===
-We had $sp(P, r_1 \cup r_2) = sp(P,r_1) \cup sp(P,r_2)$. Therefore define:
-\[
-   sp_F(P,c_1 [] c_2) = sp_F(P,c_1) \lor sp_F(P,c_2)
-\]
-===== Correctness =====
-We show by induction on $c_1$ that for all $P$:
-\[
-   sp(\{s.\ P\}, r_c(c_1)) = \{ s.\ sp_F(P,c_1) \}
-\]
-===== Examples =====
-**Example 1.**
-Precondition: $\{x \ge 5 \wedge y \ge 3\}$. Code:
-<code>
-x = x + y + 10
-</code>
-\[
-\begin{array}{l}
-sp(x \ge 5 \land y \ge 3, x=x+y+10) = \\
-                   \exists x_0.\ x_0 \ge 5 \wedge y \ge 3\ \land\ x = x_0 + y + 10 \\
-\leftrightarrow \ y \ge 3 \land x \ge y + 15
-\end{array}
-\]
-**Example 2** Precondition: $\{x \ge 2 \land y \le 5 \land x \le y \}$. Code:
-<code>
-havoc(x)
-</code>
-\[
-  \exists x_0.\ x_0 \ge 2 \land y \le 5 \land x_0 \le y
-\]
-i.e.
-\[
-   \exists x_0.\ 2 \le x_0 \le y \land y \le 5
-\]
-i.e.
-\[
-\le y \land y \le 5
-\]
-If we simply removed conjuncts containing $x$, we would get just $y \le 5$.
-===== Size of Generated Formulas =====
-The size of the formula can be exponential because each time we have a nondeterministic choice, we double formula size:
-\[
-\begin{array}{l}
-sp_F(P, (c_1 [] c_2);(c_3 [] c_4)) =  \\
-sp_F(sp_F(P,c_1 [] c_2), c_3 [] c_4) =  \\
-sp_F(sp_F(P,c_1) \vee sp_F(P,c_2), c_3  [] c_4) = \\
-sp_F(sp_F(P,c_1) \vee sp_F(P,c_2), c_3) \vee
-sp_F(sp_F(P,c_1) \vee sp_F(P,c_2), c_4)
-\end{array}
-\]
-===== Reducing sp to Relation Composition =====
-The following identity holds for relations (see [[:sav08:Sets and Relations]]):
-\[
-   sp(P,r) = ran(\Delta_P \circ r)
-\]
-Based on this, we can compute $sp(P,c_1)$ in two steps:
-  - compute formula $F_c(assume(P);c_1)$, using [[Compositional VCG]]
-  - existentially quantify over initial (non-primed) variables
-Indeed, if $F_1$ is a formula denoting relation $r_1$, that is,
-\[
-    r_1 = \{(\vec x, \vec x\,').\ F_1(\vec x,\vec x\,')
-\]
-then $\ \exists \vec x. F_1(\vec x, \vec x\,')$ is formula denoting the range of $r_1$:
-\[
-   ran(r_1) = \{ \vec x\,'.\ \exists \vec x. F_1(\vec x, \vec x\,') \}
-\]
-Moreover, the resulting approach does not have exponentially large formulas.