Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:conjunctions_of_predicates [2008/05/08 12:46] vkuncak |
sav08:conjunctions_of_predicates [2008/05/08 12:46] vkuncak |
||
|---|---|---|---|
| Line 3: | Line 3: | ||
| 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_1,\ldots,P_n$ in program variables. | ||
| - | 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}$ |
| - | Using [[Abstract Interpretation Recipe]] we construct: | + | We design analysis using [[Abstract Interpretation Recipe]]. |
| - | * abstract domain: truth values of predicates | + | |
| - | * concretization function: states given by truth values | + | |
| - | * abstraction function | + | |
| - | * best abstract post for simple programming language | + | |
| Finite lattice. | Finite lattice. | ||
| Two different orders. | Two different orders. | ||
| + | |||