Compositional Characterization of Observable Program Properties

In this paper we model both program behaviours and abstractions between them as lax functors, which generalize abstract interpretations by exploiting the natural ordering of program properties. This generalization provides a framework in which correctness (safety) and completeness of abstract interpretations naturally arise from this order. Furthermore, it supports modular and stepwise refinement: given a program behaviour, its characterization, which is a "best" correct and complete denotational semantics for it, can be determined in a compositional way. University of Aarhus, Denmark y LFCS, University of Edinburgh, Scotland z Universitat Erlangen, Germany 1 Introduction Abstract interpretation is a method for analyzing program behaviours, i.e. the relationship between programs and their observable properties [CC77a, CC77b, Nie86, AH87, JN90]. It abstracts from standard (denotational) semantics for programming languages to nonstandard semantics, which are intended to retain c..