Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
sav07_lecture_6_skeleton [2007/03/30 19:57] vkuncak |
sav07_lecture_6_skeleton [2007/03/30 20:18] vkuncak |
||
---|---|---|---|
Line 187: | Line 187: | ||
S is infinite, instead of S, we use a representation of some approximation of S. Because we want to be sure to account for all possibilities (and not miss errors), we use overapproximation of S. | S is infinite, instead of S, we use a representation of some approximation of S. Because we want to be sure to account for all possibilities (and not miss errors), we use overapproximation of S. | ||
+ | |||
Line 220: | Line 221: | ||
This is the most important condition for abstract interpretation. | This is the most important condition for abstract interpretation. | ||
- | |||
- | When equality holds, we have the "best abstract transformer" (the most precise one) for a given $\gamma$. | ||
One way to find $sp\#$ it is to have $\alpha$ that goes the other way | One way to find $sp\#$ it is to have $\alpha$ that goes the other way | ||
Line 241: | Line 240: | ||
sp\#(a,r) = \alpha(sp(\gamma(a),r)) | sp\#(a,r) = \alpha(sp(\gamma(a),r)) | ||
\end{equation*} | \end{equation*} | ||
+ | and we call this "the best transformer". | ||
- | All else being same, the best transformer is better, because it gives as precise results as we can get with a given analysis domain. But sometimes it can be more expensive so we use a weaker one. | ||
==== Lattices ==== | ==== Lattices ==== | ||
+ | |||
+ | Recall notions of [[preorder]], [[partial order]], [[equivalence relation]]. | ||
Partial order where each two element set has | Partial order where each two element set has |