Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav07_lecture_6_skeleton [2007/03/30 19:57] vkuncak |
sav07_lecture_6_skeleton [2007/04/03 23:27] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
+ | ====== Lecture 6 Skeleton ====== | ||
+ | |||
===== Resolution theorem proving ===== | ===== Resolution theorem proving ===== | ||
Line 189: | Line 191: | ||
+ | ==== Background on Lattices ==== | ||
+ | Recall notions of [[preorder]], [[partial order]], [[equivalence relation]]. | ||
+ | Partial order where each two element set has | ||
+ | * supremum (least upper bound, join, $\sqcup$) | ||
+ | * infimum (greatest lower bound, meet, $\sqcap$) | ||
+ | |||
+ | So, we have | ||
+ | \begin{equation*} | ||
+ | \begin{array}{ll} | ||
+ | x \sqsubseteq x \sqcup y & \mbox{(bound)} \\ | ||
+ | y \sqsubseteq x \sqcup y & \mbox{(bound)} \\ | ||
+ | x \sqsubseteq z \ \land\ y \sqsubseteq z\ \rightarrow\ x \sqcup y \sqsubseteq z & \mbox{(least)} | ||
+ | \end{array} | ||
+ | \end{equation*} | ||
+ | and dually for $\sqcap$. | ||
+ | |||
+ | See also [[wk>Lattice (order)]] | ||
+ | |||
+ | Example [[wk>Hasse diagram]]s for powerset of {1,2} and for constant propagation. | ||
+ | |||
+ | Properties of a lattice | ||
+ | * finite lattice | ||
+ | * finite ascending chain lattice | ||
==== Basic notions of abstract interpretation ==== | ==== Basic notions of abstract interpretation ==== | ||
Line 220: | Line 245: | ||
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 264: | ||
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 ==== | + | |
- | + | ||
- | Partial order where each two element set has | + | |
- | * supremum (least upper bound, join, $\sqcup$) | + | |
- | * infimum (greatest lower bound, meet, $\sqcap$) | + | |
- | + | ||
- | So, we have | + | |
- | \begin{equation*} | + | |
- | \begin{array}{ll} | + | |
- | x \sqsubseteq x \sqcup y & \mbox{(bound)} \\ | + | |
- | y \sqsubseteq x \sqcup y & \mbox{(bound)} \\ | + | |
- | x \sqsubseteq z \ \land\ y \sqsubseteq z\ \rightarrow\ x \sqcup y \sqsubseteq z & \mbox{(least)} | + | |
- | \end{array} | + | |
- | \end{equation*} | + | |
- | and dually for $\sqcap$. | + | |
- | + | ||
- | See also [[wk>Lattice (order)]] | + | |
- | + | ||
- | Example [[wk>Hasse diagram]]s for powerset of {1,2} and for constant propagation. | + | |
- | + | ||
- | Properties of a lattice | + | |
- | * finite lattice | + | |
- | * finite ascending chain lattice | + | |