LARA

This is a sketch of the solution of SAV07 Homework 4

Part 1

\begin{eqnarray*} R(\mbox{havoc x}) &=& \{((x,ok),(x',ok') \mid ok \rightarrow ok' \} \\ R(\mbox{assert}\ F}) &=& \{((x,ok),(x',ok') \mid (ok \land F(x)) \rightarrow (x=x' \land ok') \} \\ R(\mbox{assume}\ F}) &=& \{((x,ok),(x',ok) \mid ok\ \rightarrow\ (F(x) \land x=x' \land ok') \} \end{eqnarray*}

Then we have

$R(assert(false))=PS^2$.

$R(assume(false))= \{ ((x,ok),(x',ok')) | \lnot ok \}$

Then we have $R(assert(false)) \circ R(assume(false)) = PS^2 = R(assert(false))$.

Note that we have $R(assume(false)) \circ R(assert(false)) = R(assume(false))$.

Basically, $R(assert(false))$ and $R(assume(false))$ both act as a left zeros of $\circ$ for the relations of the form $R(c)$.

Part 2

It is easiest to use the definition of Galois connection given by $c \leq \gamma(a) \iff \alpha(c) \leq a$. The condition then reduces to

\begin{equation*} P \subseteq wp(Q,c) \ \iff\ sp(P,c) \subseteq Q \end{equation*}

Both sides are equivalent to $\forall s_1, s_2. s_1 \in P \land (s_1,s_2) \in R(c) \implies s_2 \in Q$, that is, to the Hoare triple $\{P\} c \{Q\}$.

Part 3

$\sqsubseteq$ is not a partial order, it is merely a preorder.

Part 4

Let $s.c$ denote $sp({s},R(c))$. We then have $wp(Q,c) = \{ s \mid s.c \subseteq Q \}$ and the statement reduces to proving the equivalence between

\begin{equation*} \forall Q \subseteq G. \{ s \mid s.c_2 \subseteq Q \} \subseteq \{ s \mid s.c_1 \subseteq Q \} \ \ \ (X) \end{equation*}

and

\begin{equation*} \forall s. (s.c_2 \subseteq G \rightarrow s.c_1 \subseteq s.c_2) \ \ \ (Y) \end{equation*}

We prove both directions.

$Y \rightarrow X$: Let $Q \subseteq G$. Take any $s$ such that $s.c_2 \subseteq Q$. Then $s.c_2 \subseteq G$, so $s.c_1 \subseteq s.c_2$. Therefore $s.c_1 \subseteq Q$.

$X \rightarrow Y$: Let $s.c_2 \subseteq G$. Let $Q = s.c_2$. Then $s.c_2 \subseteq Q$, so also $s.c_1 \subseteq Q$. Thus $s.c_1 \subseteq s.c_2$.

Part 5

Lemma: $skip;c \equiv c;skip \equiv c$.

$c_1 \sqsubseteq c_2\ \rightarrow\ c_1;c_3 \sqsubseteq c_2;c_3$: Let $Q \subseteq G$. Then $wp(Q,c_3) \subseteq G$ by construction of $wp$, so by definition of $\sqsubseteq$ we have $wp(wp(Q,c_3),c1) \subseteq wp(wp(Q,c_3),c2)$, i.e. $wp(Q,c_1;c_3) \subseteq wp(Q,c_2;c_3)$.

$c_1 \sqsubseteq c_2\ \rightarrow\ c_3;c_1 \sqsubseteq c_3;c_2$: Let $Q \subseteq G$. Then $wp(Q,c_1) \subseteq wp(Q,c_2)$. By monotonicity of wp, also $wp(wp(Q,c_1),c_3) \subseteq wp(wp(Q,c_2),c_3)$, so $wp(Q,c_1;c_3) \subseteq wp(Q,c_2;c_3)$.

$c_1 \sqsubseteq c_2\ \rightarrow\ c_1 [] c_3 \sqsubseteq c_2 [] c_3$: Let $Q \subseteq G$. Then $wp(Q,c_1) \subseteq wp(Q,c_2)$, so by basic set theory $wp(Q,c_2) \cap wp(Q,c_3) \subseteq wp(Q,c_1) \cap wp(Q,c_1)$.

assume(F) $\sqsubseteq$ skip $\sqsubseteq$ assert(F), assert(F); assume(F) $\equiv$ assert(F), assume(F); assert(F) $\equiv$ assume(F) - follow from rules for computing weakest preconditions.

Part 6

Suppose $assume(F);c_1 \sqsubseteq c_2$. Then by Part 5 we have

\begin{equation*} c_1 \equiv skip; c_1 \sqsubeteq assert(F);c_1 \equiv assert(F);assume(F);c_1 \sqsubseteq assert(F);c_2$ \end{equation*}

Suppose $c_1 \sqsubseteq assert(F);c_2$. Then

\begin{equation*} assume(F);c_1 \sqsubseteq assume(F);assert(F);c_2 \equiv assume(F);c_2 \subseteq skip;c_2 \equiv c_2$ \end{equation*}

Suppose $c_1;assert(F) \sqsubseteq c_2$. Then

\begin{equation*} c_1 \equiv c_1;skip \sqsubseteq c_1;assert(F);assume(F) \sqsubseteq c_2;assume(F) \end{equation*}

Suppose $c_1 \sqsubseteq c_2;assume(F)$. Then

\begin{equation*} c_1;assert(F) \sqsubseteq c_2;assume(F);assert(F) \equiv c_2;assume(F) \sqsubseteq c_2$ \end{equation*}

Part 7

By shunting rules in Part 6 we have $c_1 \sqsubseteq c_2$. By monotonicity properties in Part 5, we then obtain $P \sqsubseteq P[c_1:=c_2]$ by structural induction.