THE CONSISTENCY OF THE CALCULUS OF TOTAL CORRECTNESS FOR COMMUNICATING PROCESSES

Abstract

In [1] Hoare suggests a notation of assertions to describe the total correctness of communicating processes, and a calculus for proving it. But 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.