Concrete and abstract domains
type evalt = Notype
| Vvar of string
| Intero
| Mkarrow of evalt * evalt
t1 _ t2 , if t2 is an instance of t1
lub on evalt:
gci (greatest common instance), computed by unification
glb on evalt:
lcg (least common generalization), computed by anti-unification
even if evalt is not the final abstract domain, we relate it to the concrete domain of the collecting semantics
concrete domain: (Ã(ceval), _ , {}, ceval, Ç , È )
abstract domain: (evalt, _, Vvar(_), Notype, lcg, gci)
Previous slide
Next slide
Back to first slide
View graphic version