• English only

# Differences

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

 sav08:galois_connection_on_lattices [2008/05/07 23:45]giuliano sav08:galois_connection_on_lattices [2015/04/21 17:30] (current) Both sides previous revision Previous revision 2008/05/08 12:33 vkuncak 2008/05/07 23:45 giuliano 2008/05/07 10:22 vkuncak 2008/05/07 10:18 vkuncak 2008/05/07 10:14 vkuncak 2008/05/07 10:12 vkuncak 2008/05/07 10:03 vkuncak 2008/05/07 10:03 vkuncak 2008/05/07 08:52 vkuncak created Next revision Previous revision 2008/05/08 12:33 vkuncak 2008/05/07 23:45 giuliano 2008/05/07 10:22 vkuncak 2008/05/07 10:18 vkuncak 2008/05/07 10:14 vkuncak 2008/05/07 10:12 vkuncak 2008/05/07 10:03 vkuncak 2008/05/07 10:03 vkuncak 2008/05/07 08:52 vkuncak created Line 34: Line 34: Define $sp^\#$ using $\alpha$ and $\gamma$: Define $sp^\#$ using $\alpha$ and $\gamma$: ++++| ++++| - $+ \begin{equation*} sp^\#(a,r) = \alpha(sp(\gamma(a),​r) sp^\#(a,r) = \alpha(sp(\gamma(a),​r) -$ + \end{equation*} ++++ ++++ Line 46: Line 46: The most precise $sp^{\#}$ is called "best abstract transformer"​. The most precise $sp^{\#}$ is called "best abstract transformer"​. + + If $\alpha(\gamma(a)) = a$, then $sp^{\#}$ defined using $\alpha$ and $\gamma$ is the most precise one (given the abstract domain and particular blocks in the control-flow graph).