Lab for Automated Reasoning and Analysis LARA

Galois Connection

Galois connection is defined by two monotonic functions $\alpha : C \to A$ and $\gamma : A \to C$ between partial orders $\leq$ on $C$ and $\sqsubseteq$ on $A$, such that

\begin{equation*}
  \alpha(c) \sqsubseteq a\ \iff\ c \leq \gamma(a) \qquad (*)
\end{equation*}

for all $c$ and $a$ (intuitively, the condition means that $c$ is approximated by $a$).

Lemma: The condition $(*)$ holds iff the conjunction of these two conditions:

\begin{eqnarray*}
  c &\leq& \gamma(\alpha(c)) \\
  \alpha(\gamma(a)) &\sqsubseteq& a
\end{eqnarray*}

holds for all $c$ and $a$.

Lemma: Let $\alpha$ and $\gamma$ satisfy the condition of Galois connection. Then the following three conditions are equivalent:

Using Galois Connection

Terminology:

  • $C$ - concrete domain
  • $A$ - abstract domain
  • $\gamma$ - concretization function
  • $\alpha$ - abstraction function
  • $sp$ - (the usual) strongest postcondition (or just “strongest post”), also called
  • $sp^{\#}$ - abstract post, abstract transformer (transforms one abstract element into another)

Abstraction function for sign analysis.

Define $sp^\#$ using $\alpha$ and $\gamma$:

Best Abstract Transformer

$sp^{\#}$ can in general be arbitrarily precise while preserving correctness.

Given $\gamma$, we would like $sp^{\#}$ to be as precise as possible while being correct.

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

 
sav08/galois_connection_on_lattices.txt · Last modified: 2015/04/21 17:30 (external edit)