Summary
Proof rules are presented for an extension of Hoare's Communicating Sequential Processes. The rules deal with total correctness; all programs terminate in the absence of deadlock. The commands send and receive are treated symmetrically, simplifying the rules and allowing send to appear in guards. Also given are sufficient conditions for showing that a program is deadlock-free. An extended example illustrates the use of the technique.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Apt, K., Francez, N., de Roever, W.: A proof system for communicating sequential processes. TOPLAS 2, 359–385 (1980)
Bernstein, A.: Output guards and non-determinism in “Communicating Sequential Processes”. TOPLAS 2, 234–238 (1980)
Chandy, K., Misra, J.: An axiomatic proof technique for networks of communicating processes. TR-98, Dept. of Computer Science, Univ. of Texas at Austin, 1979
Chandy, K., Misra, J.: Proofs of networks of processes. Technical Report, Dept. of Computer Science, Univ. of Texas at Austin, 1980
Cousot, P., Cousot, R.: Semantic analysis of communicating sequential processes. In: Automata, languages and programming (J.W. de Bakker, J. van Leeuwen, eds.). Lecture Notes in Computer Sciences, Vol. 85, pp. 119–133. Berlin-Heidelberg-New York: Springer 1980
Dijkstra, E.W.: A discipline of programming. Englewood Cliffs, N.J.: Prentice-Hall 1976
Francez, N.: Distributed termination. TOPLAS 2, 42–55 (1980)
Gries, D., Levin, G.M.: Multiple assignment and procedure call proof rules. TOPLAS 2, 564–579 (1980)
Hoare, C.A.R.: An axiomatic basis for computer programming. CACM 12, 576–580, 583 (1969)
Hoare, C.A.R.: Communicating sequential processes. CACM 21, 666–677 (1978)
Hoare, C.A.R.: Towards a theory of communicating sequential processes. Programming Methodology Conference at Santa Cruz, August 1979
Levin, G.M.: Proof rules for communicating sequential processes. Ph.D. thesis, Dept. of Computer Science, Cornell University, August 1980
Levin, G.M.: A proof technique for communicating sequential processes (with an example). TR 79-401, Computer Science Dept., Cornell Univ., 1979
Owicki, S., Gries, D.: An axiomatic proof technique for parallel programs. Acta Informat. 6, 319–340 (1976)
Schneider, F.B.: Synchronization in a distributed environment. TR 79-391, Dept. of Computer Science, Cornell Univ. TOPLAS (1981, in press)
Silberschatz, A.: Communication and synchronization in distributed systems. IEEE Trans. Software Engrg. SE-5,6, 542–546 (1979)
Author information
Authors and Affiliations
Additional information
This research was supported in part by the National Science Foundation under grant MCS-7622360.
Rights and permissions
About this article
Cite this article
Levin, G.M., Gries, D. A proof technique for communicating sequential processes. Acta Informatica 15, 281–302 (1981). https://doi.org/10.1007/BF00289266
Received:
Issue Date:
DOI: https://doi.org/10.1007/BF00289266