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:abstract_interpretation_recipe [2008/05/08 12:39] vkuncak |
sav08:abstract_interpretation_recipe [2008/05/08 12:40] vkuncak |
||
---|---|---|---|
Line 14: | Line 14: | ||
* define lattice ordering $\sqsubseteq$ on $A$ such that $a_1 \le a_2 \rightarrow \gamma(a_1) \subseteq \gamma(a_2)$ | * define lattice ordering $\sqsubseteq$ on $A$ such that $a_1 \le a_2 \rightarrow \gamma(a_1) \subseteq \gamma(a_2)$ | ||
* define $sp^\# : A \times R \to A$ that maps an abstract element and a CFG statement to new abstract element, such that $sp(\gamma(a),r) \subseteq \gamma ( sp^{\#} (a,r))$ | * define $sp^\# : A \times R \to A$ that maps an abstract element and a CFG statement to new abstract element, such that $sp(\gamma(a),r) \subseteq \gamma ( sp^{\#} (a,r))$ | ||
- | (for example, by defining function $\alpha$ so that $(\alpha,\gamma)$ becomes a [[Galois Connection]]) | + | (for example, by defining function $\alpha$ so that $(\alpha,\gamma)$ becomes a [[Galois Connection on Lattices]]) |
* extend $sp^{\#}$ to work on control-flow graphs, by defining $F^\# : (V \to A) \to (V \to A)$ as follows (below, $g^{\#} : V \to A$) | * extend $sp^{\#}$ to work on control-flow graphs, by defining $F^\# : (V \to A) \to (V \to A)$ as follows (below, $g^{\#} : V \to A$) | ||
\[ | \[ |