Forward and backward propagation
Let denote the result of propagating backward the error conditions, that is, the negation of postcondition. We define by
for all . Here for any set of states we write for the complement of , that is, the set .
If is the postcondition operator, that is,
1. Then show that
where denotes the inverse of relation . In other words, computing weakest preconditions corresponds to propagating possible errors backwards.
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 and between partial orders on and on , such that
for all and (intuitively, the condition means that is approximated by ).
2. Show that the condition is equivalent to the conjunction of these two conditions:
hold for all and .
3. Let and satisfy the condition of Galois connection. Show that the following three conditions are equivalent:
4. State the condition for to hold for all . When is the set of sets of concrete states and is a domain of static analysis, is it more reasonable to expect that or to be satisfied, and why?