Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:compositional_vcg [2009/03/04 23:49] vkuncak |
sav08:compositional_vcg [2015/04/21 17:30] (current) |
||
---|---|---|---|
Line 3: | Line 3: | ||
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 | 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 | $x_1,\ldots,x_n,x'_1,\ldots,x'_n$ specifying the semantics of //c_1//, that is, formula $F$ such that | ||
- | \[ | + | \begin{equation*} |
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 \} | 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 \} | ||
- | \] | + | \end{equation*} |
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): | 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{equation*} |
\begin{array}{l} | \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 \land F_2)(s,s') = P_F(F_1)(s,s') \land P_F(F_2)(s,s') \\ | ||
Line 21: | Line 21: | ||
f_T(x')(s,s') = s'(x) | f_T(x')(s,s') = s'(x) | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
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)$. | 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 | To can then represent the validity of a Hoare triple | ||
- | \[ | + | \begin{equation*} |
\forall s,s'.\ (f_T(P)(s) \land (s,s') \in r_c(r) \rightarrow f_T(Q)) | \forall s,s'.\ (f_T(P)(s) \land (s,s') \in r_c(r) \rightarrow f_T(Q)) | ||
- | \] | + | \end{equation*} |
by formula | by formula | ||
- | \[ | + | \begin{equation*} |
\forall x_1,\ldots,x_n,x'_1,\ldots,x'_n.\ (P \land F_c(c_1) \rightarrow Q) | \forall x_1,\ldots,x_n,x'_1,\ldots,x'_n.\ (P \land F_c(c_1) \rightarrow Q) | ||
- | \] | + | \end{equation*} |
Line 40: | Line 41: | ||
=== Assignment === | === Assignment === | ||
- | \[ | + | \begin{equation*} |
F_c(x=e) = (x'=e \land \bigwedge_{v \in V \setminus \{x\}} v=v') | F_c(x=e) = (x'=e \land \bigwedge_{v \in V \setminus \{x\}} v=v') | ||
- | \] | + | \end{equation*} |
=== Assume === | === Assume === | ||
- | \[ | + | \begin{equation*} |
F_c({\it assume}(e)) = (e \land \bigwedge_{v \in V} v=v') | F_c({\it assume}(e)) = (e \land \bigwedge_{v \in V} v=v') | ||
- | \] | + | \end{equation*} |
=== Havoc === | === Havoc === | ||
- | \[ | + | \begin{equation*} |
F_c({\it havoc}(x)) = (\bigwedge_{v \in V \setminus\{x\}} v=v') | F_c({\it havoc}(x)) = (\bigwedge_{v \in V \setminus\{x\}} v=v') | ||
- | \] | + | \end{equation*} |
For simplicity of notation, in the sequel we work with state that has only one variable, x. | For simplicity of notation, in the sequel we work with state that has only one variable, x. | ||
Line 61: | Line 62: | ||
Note | Note | ||
- | \[ | + | \begin{equation*} |
\{(\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 \} | \{(\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 \} | ||
- | \] | + | \end{equation*} |
Therefore, | Therefore, | ||
- | \[ | + | \begin{equation*} |
F_c(c_1 [] c_2) = F_c(c_1) \lor F_c(c_2) | F_c(c_1 [] c_2) = F_c(c_1) \lor F_c(c_2) | ||
- | \] | + | \end{equation*} |
=== Sequential composition === | === Sequential composition === | ||
Note that | Note that | ||
- | \[ | + | \begin{equation*} |
\{(\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] \} | \{(\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] \} | ||
- | \] | + | \end{equation*} |
Therefore, | Therefore, | ||
- | \[ | + | \begin{equation*} |
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]) | 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]) | ||
- | \] | + | \end{equation*} |
- | To avoid re-using variables, introduce always a fresh variable as //\vec z//, denote it $\vec z_i$. | + | Above, $F_c(c_1)[\vec x':=\vec z]$ denotes taking formula $F_c(c_1)$ and replacing in it occurrences of variables $\vec x'$ by variables $\vec z$. |
+ | |||
+ | To avoid re-using variables, introduce always a fresh variable as $\vec z$ and denote it $\vec z_i$. | ||
===== Using Computed Formulas ===== | ===== Using Computed Formulas ===== | ||
Line 86: | Line 89: | ||
Resulting formula: | Resulting formula: | ||
- | \[ | + | \begin{equation*} |
\forall x,x'.\ (P \land (\exists z_1,\ldots,z_n. F_c(c_1))\ \rightarrow Q) | \forall x,x'.\ (P \land (\exists z_1,\ldots,z_n. F_c(c_1))\ \rightarrow Q) | ||
- | \] | + | \end{equation*} |
which is equivalent to | which is equivalent to | ||
- | \[ | + | \begin{equation*} |
\forall x,x',z_1,\ldots,z_n. (P \land F_c(c_1) \rightarrow Q) | \forall x,x',z_1,\ldots,z_n. (P \land F_c(c_1) \rightarrow Q) | ||
- | \] | + | \end{equation*} |
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)$. | 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 | Optimizations: assignments and assume statements generate equalities, many of which can be eliminated by one-point rule | ||
- | \[ | + | \begin{equation*} |
(\exists x. x=t \land F(x)) \leftrightarrow F(t) | (\exists x. x=t \land F(x)) \leftrightarrow F(t) | ||
- | \] | + | \end{equation*} |
=== Example === | === Example === | ||
Line 110: | Line 113: | ||
It translate into the following relation: | It translate into the following relation: | ||
- | \[ | + | \begin{equation*} |
\begin{array}{l} | \begin{array}{l} | ||
(assume(x<0) \circ (x = x+1)\ \cup\ assume (\lnot (x<0)) \circ skip) \circ \\ | (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) | (assume(y<0) \circ (y = y+x)\ \cup\ assume(\lnot(y<0)) \circ skip) | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
By distribution of composition over union the relation above becomes: | By distribution of composition over union the relation above becomes: | ||
- | \[ | + | \begin{equation*} |
\begin{array}{l} | \begin{array}{l} | ||
(assume(x<0) \circ (x = x+1) \circ assume(y<0) \circ (y = y+x)) \cup \\ | (assume(x<0) \circ (x = x+1) \circ assume(y<0) \circ (y = y+x)) \cup \\ | ||
Line 126: | Line 129: | ||
(assume (\lnot (x<0)) \circ assume(\lnot(y<0))) | (assume (\lnot (x<0)) \circ assume(\lnot(y<0))) | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
It can be easily proven that $\{P\}\ \cup_i p_i\ \{Q\} \Leftrightarrow \wedge_i \{P\}\ p_i\ \{Q\}$: | It can be easily proven that $\{P\}\ \cup_i p_i\ \{Q\} \Leftrightarrow \wedge_i \{P\}\ p_i\ \{Q\}$: | ||
- | \[ | + | \begin{equation*} |
\begin{array}{1} | \begin{array}{1} | ||
\{P\}\ \cup_i p_i\ \{Q\} \Leftrightarrow \\ | \{P\}\ \cup_i p_i\ \{Q\} \Leftrightarrow \\ | ||
Line 137: | Line 140: | ||
\wedge_i \{P\}\ p_i\ \{Q\} | \wedge_i \{P\}\ p_i\ \{Q\} | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
We can take all the terms of the union one by one as in the following small example: | We can take all the terms of the union one by one as in the following small example: | ||
- | \[ | + | \begin{equation*} |
\begin{array}{1} | \begin{array}{1} | ||
(assume(x<0) \circ (x = x+1) \circ assume(y<0) \circ (y = y+x)) \cup \\ | (assume(x<0) \circ (x = x+1) \circ assume(y<0) \circ (y = y+x)) \cup \\ | ||
Line 147: | Line 150: | ||
(\lnot (x<0) \wedge x'=x \wedge y'=y) | (\lnot (x<0) \wedge x'=x \wedge y'=y) | ||
\end{array} | \end{array} | ||
- | \] | + | \end{equation*} |
Using valid formulas we can move the existential quantifiers outside the formula. | Using valid formulas we can move the existential quantifiers outside the formula. |