• People
• Events
• Research

Compositional Characterization of Observable Program Properties

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.

ECS-LFCS-89-99