Programming Research Group Technical Monograph PRG-20

Zhou Chao Chen and C A R Hoare

May 1981, 23 pages, ISBN 0-902928-13-9

We introduce a programming notation to describe the behaviour of groups of parallel processes, communicating with each other over a network of named channels. An assertion is a predicate with free channel names, each of which stands for the sequence of values which have been communicated along that channel up to some moment in time. A process invariantly satisfies an assertion if that assertion is true before and after each communication by that process. We present a system of inference rules for proving that processes satisfy assertions, and illustrate their use on some examples. The validity of the inference rules is established by constructing a model of the programming notation, and by proving each inference rule as a theorem about the model. Limitations of the model and proof system are discussed in the conclusion.