LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
sav08:abstract_interpretation_recipe [2008/05/08 12:41]
vkuncak
sav08:abstract_interpretation_recipe [2008/05/20 12:14]
vkuncak
Line 18: Line 18:
   * 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$)
 \[ \[
-   ​F^{\#​}(g^{\#​})(p_2) = g^{\#}(p_2) \sqcup \bigsqcup_{(p_1,p_2) \in E} sp^{\#​}(g^{\#​}(p_1),r(p_1,p_2))+   ​F^{\#​}(g^{\#​})(p') = g^{\#}(p') \sqcup \bigsqcup_{(p,p') \in E} sp^{\#​}(g^{\#​}(p),r(p,p'))
 \] \]
 which is analogous to [[Collecting Semantics]] which is analogous to [[Collecting Semantics]]