Compositional Characterization of Observable Program Properties

Abstract

Abstract interpretation is a method for analyzing program behaviours, i.e. the relationship between programs and their observable properties. It abstracts from standard (denotational) semantics to non-standard semantics for programming languages, which are intended to retain correct information about given properties of interest. This intention is hard to specify without a precise notion of behaviour, which, despite its primacy, was missing in the framework of abstract interpretation. In this paper, behaviour is defined as a simple generalization of abstract interpretation which can then be used to specify the properties of programs which must be respected, both by abstract interpretations, and the abstractions between them.