LARA

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$ (intuitively, the condition means that $c$ is approximated by $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:

4. State the condition for $c=\gamma(\alpha(c))$ to hold for all $c$. When $C$ is the set of sets of concrete states and $A$ is a domain of static analysis, is it more reasonable to expect that $c=\gamma(\alpha(c))$ or $\alpha(\gamma(a)) = a$ to be satisfied, and why?