LARA

This is an old revision of the document!

(Draft only!)

Forward and backward propagation

Let $ep(Q,r)$ denote the result of propagating backward the error conditions, that is, the negation of postcondition. We define $ep$ by

\begin{equation*} ep(Q,r) = wp(Q^c,r)^c \end{equation*}

for all $Q \subseteq \mbox{PS}$. Here for any set of states $S \subseteq \mbox{PS}$ we write $S^c$ for the complement of $S$, that is, the set $\mbox{PS} \setminus S = \{ x \in \mbox{PS} \mid x \notin S \}$.

If $sp$ is the postcondition operator, that is,

\begin{equation*} sp(P,r) = \{ y \mid \exists x. x \in P \land (x,y) \in r \} \end{equation*}

1. Then show that

\begin{equation*} ep(Q,r) = sp(Q,r^{-1}) \end{equation*}

where $r^{-1}$ denotes the inverse of relation $r$. In other words, computing weakest preconditions corresponds to propagating possible errors backwards.

Galois Connection

In the lecture we talked about a special case of Galois connection, called Galois insertion. Galois connection is in general defined by two monotonic functions $\alpha : C \to A$ and $\gamma : A \to C$ between partial orders $\leq$ on $C$ and $\sqsubseteq$ on $A$, such that

\begin{equation*} \alpha(c) \sqsubseteq a\ \iff\ c \leq \gamma(a) \qquad (*) \end{equation*}

for all $c$ and $a$.

2. Show that the condition $(*)$ is equivalent to the conjunction of these two conditions:

\begin{eqnarray*} c &\leq& \gamma(\alpha(c)) \\ \alpha(\gamma(a)) &\sqsubseteq& a \end{eqnarray*}

hold for all $c$ and $a$.

3. Let $\alpha$ and $\gamma$ satisfy the condition of Galois connection. Show that the following three conditions are equivalent:

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 $S$. Program states in our language will be pairs $(x,ok)$ where $x \in S$ and $ok$ is a boolean value that indicates whether an error has occurred. Therefore, a state is an element of $\mbox{PS} = S \times \{\mbox{true},\mbox{false}\}$.

Your task is to define, for each command $c$, the meaning $R(c) \subseteq \mbox{PS}^2$.

Using the standard definition of $wp$,

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

Your goal is to come up with the definition of $R(c)$ such that wp satisfies the following expected conditions: 

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

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)

Your remaining task is to define the meaning of assert, assume, and havoc such that all the expected conditions above hold.

Verify your solution by computing 

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

and 

wp(PS, assert(false);assume(false)).

where PS is the set of all program states.

Resolution Example