Differences
This shows you the differences between two versions of the page.
| Next revision Both sides next revision | |||
|
sav08:homework11 [2008/05/08 18:50] vkuncak created |
sav08:homework11 [2008/05/08 18:50] vkuncak |
||
|---|---|---|---|
| Line 35: | Line 35: | ||
| **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 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 | + | **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 equal to the other, strictly less, for various sets of predicates) | * the comparison of numbers of iterations needed to compute the fixpoint $g_A$ and $g_B$ (is one always less than equal to the other, strictly less, for various sets of predicates) | ||
| * the precision of computed information, that is, the sets $\gamma(g_A(p))$ and $\gamma(g_B(p))$ for an arbitrary program point $p \in V$ | * the precision of computed information, that is, the sets $\gamma(g_A(p))$ and $\gamma(g_B(p))$ for an arbitrary program point $p \in V$ | ||