LARA – Lab for Automated Reasoning and Analysis -

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:

$\alpha(\gamma(a)) = a$ for all $a$
$\alpha$ is a surjective function
$\gamma$ is an injective function

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