Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Last revision Both sides next revision | ||
sav07_lecture_6_skeleton [2007/03/30 20:18] vkuncak |
sav07_lecture_6_skeleton [2007/03/30 20:53] vkuncak |
||
---|---|---|---|
Line 189: | Line 189: | ||
+ | ==== 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 241: | Line 263: | ||
\end{equation*} | \end{equation*} | ||
and we call this "the best transformer". | and we call this "the best transformer". | ||
- | |||
- | |||
- | ==== 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 | ||