Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Last revision Both sides next revision | ||
|
sav08:conjunctions_of_predicates [2008/05/08 12:46] vkuncak |
sav08:conjunctions_of_predicates [2008/05/08 12:55] vkuncak |
||
|---|---|---|---|
| Line 1: | Line 1: | ||
| ====== Abstract Interpretation with Conjunctions of Predicates ====== | ====== Abstract Interpretation with Conjunctions of Predicates ====== | ||
| - | Parameters: a finite set of formulas ${\cal P} = P_1,\ldots,P_n$ in program variables. | + | Parameters: a finite set of formulas ${\cal P} = \{ P_0, P_1,\ldots,P_n\}$ in program variables. Suppose $P_0$ is the predicate 'false'. |
| - | Let $A = 2^{\cal P}$, so for $a \in A$ we have $a \subseteq {\cal P}$ | + | Let $A = 2^{\cal P}$, so for $a \in A$ we have $a \subseteq {\cal P}$. |
| We design analysis using [[Abstract Interpretation Recipe]]. | We design analysis using [[Abstract Interpretation Recipe]]. | ||
| - | Finite lattice. | + | Define a syntactic order on $(A,\le)$ |
| - | Two different orders. | + | Finite lattice. |
| + | |||
| + | Defining $\gamma$. | ||
| + | |||
| + | Defining $\alpha$. | ||
| + | |||
| + | Is it the case that $\alpha(\gamma(a))=a$? | ||