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 [2007/04/16 01:13] mirco.dotta |
sav07_lecture_6 [2007/05/28 19:40] vasu.singh |
||
|---|---|---|---|
| Line 83: | Line 83: | ||
| x == h(u) | x == h(u) | ||
| f(g(y)) == f(v) | f(g(y)) == f(v) | ||
| + | |||
| Line 125: | Line 126: | ||
| \end{equation*} | \end{equation*} | ||
| where $\theta$ is the most general unifier of $A_1$ and $A_2$. | where $\theta$ is the most general unifier of $A_1$ and $A_2$. | ||
| + | |||
| Line 186: | Line 188: | ||
| [R]e<sub>T</sub> = {(a,s1(a)), (s1(a),s1(s1(a))), (s2(a), s2(s2(a))), ...} \\ | [R]e<sub>T</sub> = {(a,s1(a)), (s1(a),s1(s1(a))), (s2(a), s2(s2(a))), ...} \\ | ||
| \\ | \\ | ||
| - | Then we should find a pair (tx,ty) s.t. (tx,ty) ∉ [R]. A possible counter-example is (tx,a) ∉ [R], ∀tx | + | Then we should find a pair (tx,ty) s.t. (tx,ty) ∉ [R]. A possible counter-example is (tx,a) ∉ [R], ∀tx. |
| + | The fact that we have found a counter-example imply that the initial formula is invalid.\\ | ||
| \\ | \\ | ||
| Consider case where R denotes less than relation on integers and Ev denotes that integer is even | Consider case where R denotes less than relation on integers and Ev denotes that integer is even | ||
| Line 343: | Line 346: | ||
| Simple example with small ascending chains but large size: constant propagation. | Simple example with small ascending chains but large size: constant propagation. | ||
| + | |||
| ==== Example analyses ==== | ==== Example analyses ==== | ||
| Line 350: | Line 354: | ||
| + | ==== References ==== | ||
| + | * A wonderful tutorial by Prof. Cousot, explaining in fairly simple language what abstract interpretation is all about. [[http://www.di.ens.fr/~cousot/COUSOTtalks/VMCAI05_TOOLS.shtml|Tutorial Abstract Interpretation]] | ||