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 [2008/04/30 10:46] vkuncak |
sav08:abstract_interpretation [2008/04/30 10:55] vkuncak |
||
|---|---|---|---|
| Line 56: | Line 56: | ||
| \end{eqnarray*} | \end{eqnarray*} | ||
| because of the way we defined order. | because of the way we defined order. | ||
| + | |||
| + | Consider first only a single loop. | ||
| Then we rewrite our computation of sp for the loop by replacing $sp$ with $sp\#$ and replacing $\cup$ with $\sqcup$. We obtain fixpoint equation for computing the effect of a transitive closur eof a relation (i.e. a loop): | Then we rewrite our computation of sp for the loop by replacing $sp$ with $sp\#$ and replacing $\cup$ with $\sqcup$. We obtain fixpoint equation for computing the effect of a transitive closur eof a relation (i.e. a loop): | ||