LARA

Forthcoming SAV07 Homework 4 Solution.

THE PARTS BELOW ARE DUE ON APRIL 19

Weakest preconditions and relations

Consider a guarded command language with one variable, denoted x, and constructs 

assume F
assert F
havoc(x)
c1 [] c2
c1 ; c2

Assume that F can only mention x as the only variable, which takes values from some set $D$. Program states in our language will be pairs $(x,ok)$ where $x \in D$ and $ok$ is a boolean value that is false if and only if an error has occurred. Therefore, a state is an element of $\mbox{PS} = D \times \{\mbox{true},\mbox{false}\}$.

Your task is to define, for each command $c$, the meaning $R(c) \subseteq \mbox{PS}^2$ such that the expected conditions, stated below, hold.

As usual, define the weakest preconditions of commands by

\begin{equation*} wp(Q,c) = \{ s \mid \forall s'. (s,s') \in R(c) \rightarrow s' \in Q \} \end{equation*}

Define the set $G$ of good states for which $\mbox{ok}=\mbox{true}$, formally $G = \{(x,\mbox{true}) \mid x \in D\}$.

Your goal is to define $R( c )$ recursively for all commands c, such that, for all Q ⊆ G and all commands c, c1, c2 the following expected conditions hold: 

wp(Q,c) ⊆ G
wp(Q, c1 [] c2) = wp(Q,c1) ∩ wp(Q,c2)
wp(Q, c1 ; c2) = wp(wp(Q,c2),c1)
wp(Q, havoc(x)) = {(x,true)|∀x'.(x',true) ∈ Q}
wp(Q, assume F) = {(x,true)|F(x) -> (x,true)∈Q}
wp(Q, assert F) = {(x,true)|F(x) & (x,true)∈Q}

and then verify with an inductive proof that they indeed hold.

These conditions correspond to our rules for propagating formulas using wp.

As a hint, you should be able to define 

R(c1 [] c2) = R(c1) ∪ R(c2)
R(c1 ; c2) = R(c1) o R(c2)

1. Your remaining task is to define the relation R( c ) corresponding to assert, assume, and havoc such that the expected conditions above hold.

Verify your solution by computing 

R(assert(false); assume(false))

and 

R(assume(false); assert(false)).

sp and wp form Galois connection

Let PS be the set of program states and $r \subseteq PS^2$. Define Define wp as in the first part of this homework, and define

\begin{equation*} sp(P,c) = \{ s_2 \mid \exists s_1. s_1 \in P \land (s_1,s_2) \in R(c) \} \end{equation*}

Consider a fixed command c and define

\begin{eqnarray*} \alpha(P) &=& sp(P,c) \\ \gamma(Q) &=& wp(Q,c) \end{eqnarray*}

2. Show that such $\alpha, \gamma : 2^{PS} \to 2^{PS}$ form a Galois connection with ordering on $2^{PS}$ given by $\subseteq$ and definition of Galois connection in SAV07 Homework 3.

Rules for guarded commands

Using the previously defined wp and $G$ as the set of good states, define the relation $\sqsubseteq$ on commands by

\begin{equation*} c_1 \sqsubseteq c_2 \iff \forall Q \subseteq G.\ wp(Q,c_2)\ \subseteq\ wp(Q,c_1) \end{equation*}

Note that this means that if we prove $c_2$ correct, then $c_1$ is correct as well.

3. Is $\sqsubseteq$ a partial order? Prove or give a counterexample.

Define $c_1 \equiv c_2$ as $c_1 \sqsubseteq c_2\ \land\ c_2 \sqsubseteq c_1$.

4. Show

\begin{equation*} c_1 \sqsubseteq c_2\ \iff\ \forall s_1 \in \mbox{PS}.\ sp(\{s_1\},R(c_1)) \subseteq sp(\{s_1\},R(c_2))\ \lor\ sp(\{s_1\},R(c_2)) \not\subseteq G \end{equation*}

In other words, $\sqsubseteq$ holds iff for every execution of $c_1$ from a state $s_1$ there is either the same execution in $c_2$, or $c_2$ can produce an error.

5. Define command skip as assert(True). Prove

$c_1 \sqsubseteq c_2\ \rightarrow\ c_1;c_3 \sqsubseteq c_2;c_3$
$c_1 \sqsubseteq c_2\ \rightarrow\ c_3;c_1 \sqsubseteq c_3;c_2$
$c_1 \sqsubseteq c_2\ \rightarrow\ c_1 [] c_3 \sqsubseteq c_2 [] c_3$
assume(F) $\sqsubseteq$ skip $\sqsubseteq$ assert(F)
assert(F); assume(F) $\equiv$ assert(F)
assume(F); assert(F) $\equiv$ assume(F)

6. Prove the following shunting rules:

\begin{eqnarray*} \mbox{assume}(F)\ ;\ c_1\ \sqsubseteq\ c_2 \ &\iff& \ c_1\ \sqsubseteq\ \mbox{assert}(F)\ ;\ c_2 \\ c_1\ ;\ \mbox{assert}(F)\ \sqsubseteq\ c_2 \ &\iff& \ c_1\ \sqsubseteq\ c_2\ ;\ \mbox{assume}(F) \end{eqnarray*}

7. Let P be a guarded language program containing a statement c1. Suppose that

assume(pre); c1; assert(post) $\sqsubseteq$ havoc(x)

Then show that if c2 is given by

assert(pre); havoc(x); assume(post)

then

P $\sqsubseteq$ P[c1:=c2]

where P[c1:=c2] denotes the result of substuting c2 instead of c1.

THE PARTS BELOW ARE DUE ON APRIL 26

Using formDecider

Download Jahob system, generate some simple true verification conditions using SAV07 Homework 2, save them into a file foo.txt, and make sure that you can prove them using 

bin/decide foo.txt

To make sure that formulas are understood by the prover, you will need to add some type annotations. If a variable is integer, instead of just 

ALL x. F

you should output 

ALL (x::int). F

Similarly, instead of emitting constants such as 3, you should pretty print them as (3::int).

When emitting multiple quantifiers, do not write e.g. “ALL x,y. F” but instead write “ALL (x::t). (ALL (y::t). F)”.

You can find some example formulas in jahob/examples/nasty_formulas directory of Jahob.

Language features

Extend the language from SAV07 Homework 2 so that it can manipulate global arrays (represented as functions from integers to objects) and so that it handles dynamically allocated objects. Extend the verification condition generator accordingly, using the desugaring in SAV07 Lecture 4.

Your new formula language will need to contain not only integer terms but also terms containing function symbols that represent arrays. Also, assignments will generate function update expressions. Therefore, terms can be generated not only by function symbols, such as $a(i)$, but also by updated function symbols. For example, $a[i_1:=o_1][i_2:=o_2](i)$ denotes a term that contains an updated function symbol $a[i_1:=o_1][i_2:=o_2]$ with integer expressions $i_1,i_2$ and object expressions $o_1,o_2$, and $i$ denotes an integer expression. You can assume that the formulas in specifications are well typed, for example, there are no terms that attempt to add integers and objects. Note that you will be able to eliminate update expressions such as $a[i_1:=o_1][i_2:=o_2](i)$ by flattening them and using propositional operators, as in SAV07 Lecture 4.

Note: to generate verification conditions that talk about dynamically allocated objects, you would need to model the set of allocated objects. For the purpose of this homework you can simplify your task and replace a command of the form 

x = new Object();

with 

havoc x;
assume "not (x = null)"

and avoid maintaining the set of allocated objects.

Here is an example of how you can transform a program into a verification condition.

Consider a program: 

j = i + k;
a[i] = o1;
a[j] = o2;
assert (a[i]=a[j]);

After reducing array assignments to ordinary assignments with update expressions, you obtain: 

j = i + k;
a = a[i:=o1];
a = a[j:= o2];
assert (a[i]=a[j]);

Computing weakest precondition with respect to True we get, going backwards, the following formulas: 

a(i)=a(j)
a[j:=o2](i) = a[j:=o2](j)
a[i:=o1][j:=o2](i) = a[i:=o1][j:=o2](j)
a[i:=o1][i+k:=o2](i) = a[i:=o1][i+k:=o2](i+k)

This is the formula whose validity we would like to prove.

To do this, we eliminate array update expressions. A useful intermediate step is to represent array updates using conditional IF expressions. After replacing top-level updates the last expression becomes 

(if i+k=i then o2 else a[i:=o1](i)) = (if i+k=i+k then o2 else a[i:=o1](i+k))

and then repeating the process we obtain 

(if i=i+k then o2 else (if i=i then o1 else a(i))) = 
(if i+k=i+k then o2 else (if i+k=i then o1 else a(i+k)))

We can in fact simplify *some* of these 'if' expressions, but this is not necessary, and it is not possible in general. For example we cannot eliminate if i=i+k … because we do now know the value of k.

The solution is therefore to first flatten expressions by introducing fresh variables for all IF expressions and then transform IF expressions into disjunctions and conjunctions. When proving validity of formulas, we can obtain, for example: 

(v1 = (if i=i then o1 else a(i))) &
 v2 = (if i=i+k then o2 else v2) &
 v3 = (if i+k=i then o1 else a(i+k)) &
 v4 = (if i+k=i+k then o2 else v3)) --> v2 = v4

You can generate such formulas by repeatedly extracting the innermost IF expressions and naming them using fresh variables. If you have such a set of definitions of the form v1=t1, …, vn=tn then if you are proving validity of formula F you use 

(v1=t1 & ... & vn=tn) --> F

As a result, all 'if' expressions occur in formulas of form 

v = (if c then t else e)

which you can represent as 

(c & v=t) | ((not c) & (v = e))

You can then pretty print such formulas and test their value using formDecider.

NOTE: To test your translation, you can use the fact that formDecider and Isabelle do, in fact, support 'if' expressions. For example, if you give to formDecider the formula 

((if i=i+k then o2 else (if i=i then o1 else a(i))) = 
(if i+k=i+k then o2 else (if i+k=i then o1 else a(i+k))))

it will say that the formula is not valid, which is a correct answer. On the other hand, if you give it the formula 

(o1=o2 | k=0) --> 
((if i=i+k then o2 else (if i=i then o1 else a(i))) = 
(if i+k=i+k then o2 else (if i+k=i then o1 else a(i+k))))

it will correctly conclude that the formula is valid.

Verifying programs with procedures

Extend the abstract syntax trees for guarded commands from SAV07 Homework 2 to represent programs. A program is a collection of procedures, which manipulate objects, arrays of objects, and integers. Each procedure has:

  • a list of integer parameters
  • precondition, which is a formula that must be true before procedure execution
  • postcondition, which is a formula that must be true after procedure execution
  • modifies clause, which is a list of variables and arrays that the procedure may modify

Assume that all arrays are global, and can be represented as functions from integers to objects. Function application f(x) in Isabelle formulas is written simply (f x).

For simplicity you may assume that procedures do not return results.

To verify a procedure whose precondition is pre, body c, and postcondition post, prove the validity of the weakest precondition of

assume(pre); c; assert(post)

and check syntactically that only variables mentioned in modifies clause are modified.

When you encounter a procedure call to a procedure with precondition pre1, modifies clause M, and postcondition post1, then replace in pre1 and post1 formal procedure parameters with actual arguments of the procedure call. Call the resulting pre and postcondition pre2 and post2. Then you can replace procedure call with

assert(pre2); havoc M; assume(post2)

This allows you to verify procedure calls. Its soundness can be proven starting from the shunting rules shown in the previous part. (In a proof one would also need to use inductive reasoning to justify that such reasoning can be done for recursive procedures as well, but you do not to do this proof in this homework.)

Using the described technique, given a program, your implementation should check that all procedures satisfy their specification by computing weakest precondition of the desugared guarded command and then invoking formDecider.

Test your implementation on the representation of the following example in your language. 

class Max {
    private static final length = 100;
    private static Object a[] = new Object[length];
    private static void initializeFrom(int from)
    /*: requires "0 <= from & from < length"
        modifies a
        ensures "ALL (i::int). from <= i & i < length --> a i ~= null"
    */
    {
	if (from + 1 < a.length) {
	    initializeFrom(from+1);
	}
	a[from] = new Object();
    }
 
    private static void initializeFromFails(int from)
    /*: requires "0 <= from & from < length"
        modifies a
        ensures "ALL (i::int). from <= i & i < length --> a[i] ~= null"
    */
    {
	a[from] = new Object();
	if (from + 1 < a.length) {
	    initializeFromFails(from+1);
	}
    }
}

Note that 'modifies a' means that the entire content of the array 'a', viewed as a function, can be modified. The first procedure should verify, and the second procedure should not verify. Explain why this is the case and suggest possible solutions.

To debug your implementation, it is useful to first do the transformation into guarded command language, then apply the verification condition generator as a second pass. You can write a pretty-printer for guarded commands to help you understand whether you are transforming the program correctly.

Feel free to simplify your language by, for example, disallowing expressions such as 

a[from] = new Object()

and instead requiring them to be written as 

n = new Object();
a[from] = n;

to keep the set of statements in your language simple.