Reasoning about Program Composition
K. Mani Chandy, Beverly A. Sanders · 2009
This paper presents a theory for concurrent program composition based on a predicate transformer call the the weakest guarantee and a corresponding binary relation guarantees. The theory stems from a novel view of rely-guarantee techniques for reasoning about program composition and provides a general and uniform framework for handling temporal properties as well as other kinds of program properties such as refinement and encapsulation. 1 Introduction The contribution of this paper is a predicate-transformer based theory for reasoning about the composition of concurrent programs. This section contains the motivation for this contribution and a discussion of the central issues. The predicate transformers wp and wlp provide an elegant basis for reasoning about sequential programs because they focus attention on the most fundamental aspects of these programs: their initial and final states [DS90]. By identifying a program with its predicate transformer, we can reason about programs using...