This is an old revision of the document!
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.
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 and between partial orders on and on , such that
for all and .
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:
- for all
- is a surjective function
- is an injective function
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?