Differences

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

--- sav08:compositional_vcg [2009/03/04 23:49]
vkuncak
+++ sav08:compositional_vcg [2015/04/21 17:30]
@@ Line 1: / Line 1: @@
-====== Compositional VCG ======
-Let $P, Q$ be formulas and $c$ a command of our language using variables $V = \{x_1,\ldots,x_n\}$.  To check $\{P\}c_1\{Q\}$  we compute formula $F$ containing
-$x_1,\ldots,x_n,x'_1,\ldots,x'_n$ specifying the semantics of //c_1//, that is, formula $F$ such that
-\[
-    r_c(c_1) = \{ (\{("x_1",x_1),\ldots,("x_n",x_n)\},\{("x_1",x'_1),\ldots,("x_n",x'_n)\}) \mid F_1 \}
-\]
-Denote the truth value of formula in two states by $P_F(F_1)(s,s')$ (predicate for the formula) using an auxiliary definition of $f_T(s,s')$ (function for the term):
-\[
-\begin{array}{l}
-  P_F(F_1 \land F_2)(s,s') = P_F(F_1)(s,s') \land P_F(F_2)(s,s') \\
-  P_F(F_1 \lor F_2)(s,s') = P_F(F_1)(s,s') \lor P_F(F_2)(s,s') \\
-  P_F(\lnot F_1)(s,s') = \lnot P_F(F_1)(s,s') \lor P_F(F_2)(s,s') \\
-  P_F(t_1 = t_2)(s,s') = (f_T(t_1)(s,s') = f_T(t_2)(s,s')) \\
-  P_F(t_1 < t_2)(s,s') = (f_T(t_1)(s,s') < f_T(t_2)(s,s')) \\
-  f_T(t_1 + t_2)(s,s') = f_T(t_1)(s,s') + f_T(t_2)(s,s') \\
-  f_T(t_1 - t_2)(s,s') = f_T(t_1)(s,s') - f_T(t_2)(s,s') \\
-  f_T(K * t_1)(s,s') = K \cdot f_T(t_1)(s,s') \\
-  f_T(x)(s,s') = s(x) \\
-  f_T(x')(s,s') = s'(x)
-\end{array}
-\]
-Then we can construct formula $F_1$ such that $r_c(c_1) = \{ (s,s') \mid P_F(F_1)(s,s') \}$.  Denote such formula $F_1$ by $F_c(c_1)$.
-To can then represent the validity of a Hoare triple
-\[
-    \forall s,s'.\ (f_T(P)(s) \land (s,s') \in r_c(r) \rightarrow f_T(Q))
-\]
-by formula
-\[
-    \forall x_1,\ldots,x_n,x'_1,\ldots,x'_n.\ (P \land F_c(c_1) \rightarrow Q)
-\]
-===== Rules for Computing Formulas for Commands =====
-Therefore, to prove Hoare triples, we just need to compute for each command $c_1$ the formula $F_c(c_1)$.  We next show how to do it.  These rules all follow from the [[relational semantics|semantics of our language]].
-=== Assignment ===
-\[
-   F_c(x=e) = (x'=e \land \bigwedge_{v \in V \setminus \{x\}} v=v')
-\]
-=== Assume ===
-\[
-   F_c({\it assume}(e)) = (e \land \bigwedge_{v \in V} v=v')
-\]
-=== Havoc ===
-\[
-   F_c({\it havoc}(x)) = (\bigwedge_{v \in V \setminus\{x\}} v=v')
-\]
-For simplicity of notation, in the sequel we work with state that has only one variable, x.
-=== Union ===
-Note
-\[
-   \{(\vec x,\vec x') \mid F_1 \} \cup \{(\vec x,\vec x') \mid F_2 \} = \{(\vec x,\vec x') \mid F_1 \lor F_2 \}
-\]
-Therefore,
-\[
-   F_c(c_1 [] c_2) = F_c(c_1) \lor F_c(c_2)
-\]
-=== Sequential composition ===
-Note that
-\[
-    \{(\vec x,\vec x') \mid F_1 \} \circ \{(\vec x,\vec x') \mid F_2 \} = \{ (\vec x,\vec z) \mid F_1[\vec x':=\vec z] \} \circ \{ (\vec z,x') \mid F_2[\vec x:=\vec z] \} = \{ (\vec x,\vec z) \mid \exists \vec z. F_1[\vec x':=\vec z] \land F_2[\vec x:=\vec z] \}
-\]
-Therefore,
-\[
-   F_c(c_1\ ;\ c_2)\ =\ (\exists \vec z. F_c(c_1)[\vec x':=\vec z] \land F_c(c_2)[\vec x:=\vec z])
-\]
-To avoid re-using variables, introduce always a fresh variable as //\vec z//, denote it $\vec z_i$.
-===== Using Computed Formulas =====
-Note: the result will be disjunctions of such existential quantifications.  We can always move them to top level.
-Resulting formula:
-\[
-    \forall x,x'.\ (P \land (\exists z_1,\ldots,z_n. F_c(c_1))\  \rightarrow Q)
-\]
-which is equivalent to
-\[
-    \forall x,x',z_1,\ldots,z_n.  (P \land F_c(c_1) \rightarrow Q)
-\]
-Conclusions: we can just generate fresh variables for intermediate points and prove the validity of the resulting quantifier free formula $(P \land F_c(c_1) \rightarrow Q)$.
-Optimizations: assignments and assume statements generate equalities, many of which can be eliminated by one-point rule
-\[
-    (\exists x. x=t \land F(x)) \leftrightarrow F(t)
-\]
-=== Example ===
-Take the program in the example below:
-<code>
-(if (x < 0) x=x+1 else x=x);
-(if (y < 0) y=y+x else y=y);
-</code>
-It translate into the following relation:
-\[
-\begin{array}{l}
-(assume(x<0) \circ (x = x+1)\ \cup\ assume (\lnot (x<0)) \circ skip) \circ \\
-(assume(y<0) \circ (y = y+x)\ \cup\ assume(\lnot(y<0)) \circ skip)
-\end{array}
-\]
-By distribution of composition over union the relation above becomes:
-\[
-\begin{array}{l}
-(assume(x<0) \circ (x = x+1) \circ  assume(y<0) \circ (y = y+x)) \cup \\
-(assume (\lnot (x<0)) \circ assume(y<0) \circ (y = y+x)) \cup \\
-(assume(x<0) \circ (x = x+1) \circ  assume(\lnot(y<0))) \cup \\
-(assume (\lnot (x<0)) \circ assume(\lnot(y<0)))
-\end{array}
-\]
-It can be easily proven that $\{P\}\ \cup_i p_i\ \{Q\} \Leftrightarrow \wedge_i \{P\}\ p_i\ \{Q\}$:
-\[
-\begin{array}{1}
-\{P\}\ \cup_i p_i\ \{Q\} \Leftrightarrow \\
-sp(P, \cup_i p_i) \subseteq Q \Leftrightarrow \\
-\cup_i sp(P, p_i) \subseteq Q \Leftrightarrow \\
-\wedge_i sp(P,p_i) \subseteq Q \Leftrightarrow \\
-\wedge_i \{P\}\ p_i\ \{Q\}
-\end{array}
-\]
-We can take all the terms of the union one by one as in the following small example:
-\[
-\begin{array}{1}
-(assume(x<0) \circ (x = x+1) \circ  assume(y<0) \circ (y = y+x)) \cup \\
-assume(\lnot (x<0)) \Leftrightarrow \\
-\exists x_1,y_1.(x<0 \wedge y_1 = y \wedge x_1 = x) \wedge (x'=x_1 + 1 \wedge y'=y_1)) \vee \\
-(\lnot (x<0) \wedge x'=x \wedge y'=y)
-\end{array}
-\]
-Using valid formulas we can move the existential quantifiers outside the formula.
-However, we can avoid expanding all paths and instead compute relations by following program structure.
-===== Size of Generated Formulas =====
-The compositional approach generates a formula polynomial in the size of the program.  Indeed, fix the set of variables $V$.  Then:
-  * the size of formula for each basic command is constant
-  * non-deterministic choice is disjunction
-  * sequential composition is conjunction (along with renaming that does not affect size--or affects at most $\log n$)
-Moreover, formula generated in such a way looks very much like the program itself, converted to //static single assignment form//, see
-  * [[Compiler Textbooks]]
-  * [[http://doi.acm.org/10.1145/115372.115320|Efficiently computing static single assignment form and the control dependence graph]]
-===== Further reading =====
-  * [[http://sdg.csail.mit.edu/forge/|FORGE project at MIT]]