Exercises 05

We call relation $r \subseteq S \times S$ functional if $\forall s,s_1,s_2 \in S$ , if $(s,s_1) \in r$ and $(s,s_2) \in r$ then $s_1 = s_2$ . For each of the following statements either give a counterexample or prove it:

if $r$ is functional, $wp(r,S \setminus Q) = S \setminus wp(r,Q)$
if $r$ is functional, $wp(r,Q) = sp(Q,r^{-1})$
for any $r$ , $wp(r,Q_1 \cup Q_2) = wp(r,Q_1) \cup wp(r,Q_2)$
if $r$ is functional, $wp(r,Q_1 \cup Q_2) = wp(r,Q_1) \cup wp(r,Q_2)$

Rules for guarded commands

see sav07_homework_4 and its solution

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.

Lattices

Partial order and Lattices