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

$\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 \} \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):

$\begin{equation*} \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} \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)$ . 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)) \end{equation*}$

by formula

$\begin{equation*} \forall x_1,\ldots,x_n,x'_1,\ldots,x'_n.\ (P \land F_c(c_1) \rightarrow Q) \end{equation*}$

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 semantics of our language.

Assignment

$\begin{equation*} F_c(x=e) = (x'=e \land \bigwedge_{v \in V \setminus \{x\}} v=v') \end{equation*}$

Assume

$\begin{equation*} F_c({\it assume}(e)) = (e \land \bigwedge_{v \in V} v=v') \end{equation*}$

Havoc

$\begin{equation*} 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.

Union

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 \} \end{equation*}$

Therefore,

$\begin{equation*} F_c(c_1 [] c_2) = F_c(c_1) \lor F_c(c_2) \end{equation*}$

Sequential composition

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] \} \end{equation*}$

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]) \end{equation*}$

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

Note: the result will be disjunctions of such existential quantifications. We can always move them to top level.

Resulting formula:

$\begin{equation*} \forall x,x'.\ (P \land (\exists z_1,\ldots,z_n. F_c(c_1))\ \rightarrow Q) \end{equation*}$

which is equivalent to

$\begin{equation*} \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)$ .

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) \end{equation*}$

Example

Take the program in the example below:

(if (x < 0) x=x+1 else x=x);
(if (y < 0) y=y+x else y=y);

It translate into the following relation:

$\begin{equation*} \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} \end{equation*}$

By distribution of composition over union the relation above becomes:

$\begin{equation*} \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} \end{equation*}$

It can be easily proven that $\{P\}\ \cup_i p_i\ \{Q\} \Leftrightarrow \wedge_i \{P\}\ p_i\ \{Q\}$ :

$\begin{equation*} \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} \end{equation*}$

We can take all the terms of the union one by one as in the following small example:

$\begin{equation*} \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} \end{equation*}$

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

LARA