Hoare, C. A. R., A model for communicating sequential process, Department of Computing Science, University of Wollongong, Working Paper 80-1, 1980, 43p.
The primary objective of this paper Is to give a simple mathematical model for communicating sequential processes. The model is Illustrated in a wide range of familiar programming exercises, including an operating system and a simulation study. As the exposition unfolds J the examples begin to look 1ike programs, and the notations begin to look like a programming language. Thus the design of a language seems to emerge naturally from its formal definition J in an intel1ectual1y pleasing fashion. The model is not intended to deal with certain problems of nondeterminism. These have been avoided by observance of certain restrictions detailed in the appendix. No attention has been paid to problems of efficient implementation; for this J even further restrictions should be imposed. The long term objective of this study is to provide a basis for the proof of correctness of programs expressed as communicating sequential processes. However, in this paper the formalities have been kept to a minimum and no proofs are given.