Conjunctive predicate transformers for reasoning about concurrent computation
K. Mani Chandy, Beverly A. Sanders · CaltechAUTHORS (California Institute of Technology) · 1993
In this paper we propose a calculus for reasoning about concurrent programs inspired by the wp calculus for reasoning about sequential programs. We suggest predicate transformers for reasoning about progress properties and for deducing properties obtained by parallel composition. The paper presents theorems about the predicate transformers and suggests how they can be used in program design. Familiarity with the wp calculus is assumed.