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 19:59] vkuncak |
||
|---|---|---|---|
| Line 25: | Line 25: | ||
| We typically do not write universal quantifiers either, because we know that all variables in a clause are universally quantified. | We typically do not write universal quantifiers either, because we know that all variables in a clause are universally quantified. | ||
| + | |||
| Line 54: | Line 55: | ||
| **Herbrand's theorem**: If a set of clauses in language L is true in some interpretation with domain D, then it is true in an interpretation with domain Term(L). | **Herbrand's theorem**: If a set of clauses in language L is true in some interpretation with domain D, then it is true in an interpretation with domain Term(L). | ||
| + | |||
| **Proof sketch**: If set $S$ of clauses is true in interpretation $e$, then define interpretation $e_T$ with domain Term(L) by evaluating functions as in the term model $[[f]](t_1,t_2) = f(t_1,t_2)$, and defining the value of relations by $[[R]]e_T = \{(t_1,t_2)\mid [[R(t_1,t_2)]]e = \mbox{true} \}$ (end of sketch). | **Proof sketch**: If set $S$ of clauses is true in interpretation $e$, then define interpretation $e_T$ with domain Term(L) by evaluating functions as in the term model $[[f]](t_1,t_2) = f(t_1,t_2)$, and defining the value of relations by $[[R]]e_T = \{(t_1,t_2)\mid [[R(t_1,t_2)]]e = \mbox{true} \}$ (end of sketch). | ||
| Line 185: | 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 218: | 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 239: | 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 ==== | ||