Differences
This shows you the differences between two versions of the page.
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]] |