Compositional Characterization of Observable Program Properties

Bernhard Steffen, C. Barry Jay, Michael Mendler

Abstract: 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 and completeness of abstract interpretations naturally arise from the 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.


Previous | Index | Next