This is an old revision of the document!
Galois Connection
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:
for all
is a surjective function
is an injective function
Using Galois Connection
Terminology:
- 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)
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”.