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): |