Galois connection is defined by two monotonic functions and between partial orders on and on , such that
for all and (intuitively, the condition means that is approximated by ).
Lemma: The condition holds iff the conjunction of these two conditions:
holds for all and .
Lemma: Let and satisfy the condition of Galois connection. Then the following three conditions are equivalent:
Using Galois Connection
- - concrete domain
- - abstract domain
- - concretization function
- - abstraction function
- - (the usual) strongest postcondition (or just “strongest post”), also called
- - abstract post, abstract transformer (transforms one abstract element into another)
Abstraction function for sign analysis.
Define using and :
Best Abstract Transformer
can in general be arbitrarily precise while preserving correctness.
Given , we would like to be as precise as possible while being correct.
The most precise is called “best abstract transformer”.
If , then defined using and is the most precise one (given the abstract domain and particular blocks in the control-flow graph).