Abstract Interpretation From a Denotational-semantics Perspective

AbstractThe basic principles of abstract interpretation are explained in terms of Scott-Strachey-style denotational semantics: abstract-domain creation is defined as the selection of a finite approximant in the inverse-limit construction of a Scott-domain. Abstracted computation functions are defined in terms of an embedding-projection pair extracted from the inverse-limit construction. The key notions of abstract-interpretation backwards and forwards completeness are explained in terms of topologically closed and continuous maps in a coarsened version of the Scott-topology. Finally, the inductive-definition format of a language's denotational semantics is used as the framework into which the abstracted domain and abstracted computation functions are inserted, thus defining the language's abstract interpretation