Galois connection is 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 ).
Part a) Show that the condition is equivalent to the conjunction of these two conditions:
hold for all and .
Part b) Let and satisfy the condition of Galois connection. Show that the following three conditions are equivalent:
Part c) 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?
Suppose you are given a set of predicates in a decidable theory of first-order logic (for example, quantifier-free formulas in the combination of uninterpreted function symbols with integer linear arithmetic) where is the predicate 'false'.
Part a) Consider Conjunctions of Predicates as abstract interpretation domain. Give example showing that it need not be the case that
Part b) Describe how to construct from a new, smaller, lattice , where the above equivalence holds. Is there an algorithm to compute and the partial order on using a decision procedure for the logic of predicates?
Part c) Suppose that, for the same set of predicates, we use lattice and lattice to compute the fixpoints and of the function from Abstract Interpretation Recipe. What can you say about
- the comparison of numbers of iterations needed to compute the fixpoint and (is one always less than the other, can they be equal, does it depend on set of predicates)
- the precision of computed information, that is, comparison of sets and for an arbitrary program point .