Predicate transformers for reasoning about concurrent computation

In this paper we propose a calculus for reasoning about concurrent programs inspired by the wp calculus for reasoning about sequential programs. The calculus uses a small set of familiar rules for dealing with safety, progress and parallel composition. A contribution of this paper is to demonstrate how predicate calculus in general, and predicate transformers in particular, can be used to reason about concurrent programs in which fairness plays a critical role.