Lab for Automated Reasoning and Analysis 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

  ep(Q,r) = wp(Q^c,r)^c

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,

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

1. Then show that

  ep(Q,r) = sp(Q,r^{-1})

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

  \alpha(c) \sqsubseteq a\ \iff\ c \leq \gamma(a) \qquad (*)

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:

  c &\leq& \gamma(\alpha(c)) \\
  \alpha(\gamma(a)) &\sqsubseteq& a

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?

sav07_homework_3.txt · Last modified: 2007/04/15 17:07 by vkuncak