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] (current) 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 | + | |