An approach to composition motivated by wp

Abstract

We consider the question of composition in system design, a fundamental issue in engineering. More precisely, we are interested in deducing system properties from components properties and vice-versa. This requires system and component specifications to be “compositional” in some sense. Depending on what systems are and how they are composed, this problem is satisfactorily solved (e.g., sequential composition of terminating programs) or remains a hot research topic (e.g., concurrent composition of reactive systems). In this paper, we aim at providing a logical framework in which composition issues can be reasoned about independently from the kind of systems and the laws of composition under consideration. We show that many composition related statements can be expressed in terms of predicate transformers in a way that presents interesting similarities with program semantics descriptions based on weakest precondition calculus.