Using Galois Connection
- - concrete domain
- - abstract domain
- - concretization function
- - abstraction function
- - (the usual) strongest postcondition (or just “strongest post”)
- - 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 imprecise 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).