• English only

# 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] (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. ​