LARA

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision 		Previous revision
sav07_lecture_6 [2007/04/16 00:05]
mirco.dotta 		sav07_lecture_6 [2007/05/28 19:40] (current)
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 168: Line 173:
   by: Adding a constant '​a'​   by: Adding a constant '​a'​
 R.{s1,s2,a} = L \\ R.{s1,s2,a} = L \\
 +\\
 +Term(L) = {a, s1(a), s2(a), s1(s1(a)), ...} \\
 \\ \\
 [R]e<​sub>​T</​sub>​ = {(t,s1(t)) | t ∈ Term(L)} where e<​sub>​T</​sub>:​ F => {true, false} ​ and  T => Term(L)\\ [R]e<​sub>​T</​sub>​ = {(t,s1(t)) | t ∈ Term(L)} where e<​sub>​T</​sub>:​ F => {true, false} ​ and  T => Term(L)\\
Line 179: Line 186:
 ∀t ∈ Term(L) ¬[R(s2(y),​y) ] R(s2(y),​y)]e<​sub>​T[y:​=t]</​sub>​ \\ ∀t ∈ Term(L) ¬[R(s2(y),​y) ] R(s2(y),​y)]e<​sub>​T[y:​=t]</​sub>​ \\
 \\ \\
 +[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.
 +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 336: 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 343: 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]]