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:40] vkuncak |
sav08:abstract_interpretation_recipe [2008/05/08 12:41] vkuncak |
||
---|---|---|---|
Line 7: | Line 7: | ||
* $E \subseteq V \times V$ are control-flow graph edges | * $E \subseteq V \times V$ are control-flow graph edges | ||
* $r : E \to 2^{PS \times PS}$, so each $r(p_1,p_2) \subseteq PS \times PS$ is relation describing the meaning of command between $p_1$ and $p_2$ | * $r : E \to 2^{PS \times PS}$, so each $r(p_1,p_2) \subseteq PS \times PS$ is relation describing the meaning of command between $p_1$ and $p_2$ | ||
+ | We can define meaning of program in this form using [[Collecting Semantics]]. | ||
===== Summary of key steps ==== | ===== Summary of key steps ==== |