Differences
This shows you the differences between two versions of the page.
sav08:homework11 [2008/05/08 18:51] vkuncak |
sav08:homework11 [2015/04/21 17:30] |
||
---|---|---|---|
Line 1: | Line 1: | ||
- | ====== Homework 11, Due May 14 ====== | ||
- | |||
- | ===== Problem 1 ===== | ||
- | |||
- | Galois connection is defined by two monotonic functions $\alpha : C \to A$ and $\gamma : A \to C$ between [[:partial order]]s $\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$). | ||
- | |||
- | **Part a)** 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$. | ||
- | |||
- | **Part b)** Let $\alpha$ and $\gamma$ satisfy the condition of Galois connection. Show that the following three conditions are equivalent: | ||
- | |||
- | * $\alpha(\gamma(a)) = a$ for all $a$ | ||
- | * $\alpha$ is a [[wk>surjective function]] | ||
- | * $\gamma$ is an [[wk>injective function]] | ||
- | |||
- | **Part c)** 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? | ||
- | |||
- | ===== Problem 2 ===== | ||
- | |||
- | Suppose you are given a set of predicates ${\cap P} = \{P_0,P_1,\ldots,P_n\}$ in a decidable theory of first-order logic (for example, combination of uninterpreted function symbols with integer linear arithmetic) where $P_0$ 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 | ||
- | \[ | ||
- | a_1 \leq a_2 \leftrightarrow \gamma(a_1) \subseteq \gamma(a_2) | ||
- | \] | ||
- | |||
- | **Part b)** Describe how to construct from $A$ a new, smaller, lattice $B$, where the above equivalence holds. Is there an algorithm to compute $B$ and the partial order on $B$ using a decision procedure for the logic of predicates? | ||
- | |||
- | **Part c)** Suppose that, for the same set of predicates, we use lattice $A$ and lattice $B$ to compute the fixpoints $g_A$ and $g_B$ of the function $F^{\#}$ from [[Abstract Interpretation Recipe]]. What can you say about | ||
- | * the comparison of numbers of iterations needed to compute the fixpoint $g_A$ and $g_B$ (is one always less than the other, can they be equal, does it depend on set ${\cal P}$ of predicates) | ||
- | * the precision of computed information, that is, comparison of sets $\gamma(g_A(p))$ and $\gamma(g_B(p))$ for an arbitrary program point $p \in V$. | ||