Foundations of compositional program refinement — safety properties —

Abstract

The aim of this paper is twofold: first is to formulate a foundation for refinement of parallel programs that may synchronously communicate and/or share variables; programs rendered as 1st order transition systems. The second aim is to bring closer and to show the relevance of the algebraic theory of parallel processes to that of the refinement of such 1st order systems. We do this by first developing a notion of refinement and a complete verification criteria for it for algebraic, uninterpreted, transition systems—basing ourselves on already existing theory. Then we show how 1st order transition systems can be translated—while preserving those aspects of their semantics that we are interested in—into uninterpreted transition systems. Since this translation is canonical, it is used to lift the algebraic refinement and verification criteria to the level of 1st order systems. Specifically, we show that they yield assertionai methods for refinement of such systems that resemble the methods used in Z. Manna and A. Pnueli’s temporal logic proof system.