|
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.
- C A R Hoare, "A Calculus for Total Correctness of Communicating
Processes"
Science of Computer Programming, 1, (1981), pp. 49-72
|