OXFORD UNIVERSITY COMPUTING LABORATORY

Programming Research Group Technical Monograph PRG-26

The Consistency of the Calculus of Total Correctness for Communicating Processes

Zhou Chao Chen

February 1982, 38 pages, ISBN 0-902928-16-3

In [1], Hoare suggests a notation of assertions to describe the total correctness of communicating processes, and a calculus for proving it. However the question of the consistency of the calculus is left open in that paper. In this paper we give an operational model of communicating processes and present two variants of the calculus, which are consistent with this model. One of them cannot deal with livelock, while the other one does.


  1. C A R Hoare, "A Calculus for Total Correctness of Communicating Processes"
    Science of Computer Programming, 1, (1981), pp. 49-72


[Oxford Spires]



Oxford University Computing Laboratory Courses Research People About us News