• 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)
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).