A weakest precondition semantics for communicating processes

  • Tzilla Elrad
  • Nissim Francez
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 137)


A weakest precondition semantics for communicating processes is presented, based on a centralized approach. Semantic equations are given for the CSP constructs. The representation of delay is discussed. Several examples of applying the rules are given.

Key Words and Concepts

Weakest precondition semantics communicating processes distributed programming nondeterminism termination deadlock 

CR Categories

5.24 4.32 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [ADA]
    Preliminary ADA reference manual. SIGPLAN notices 14, 6 (June 1979).Google Scholar
  2. [AFRI]
    K.R. Apt, N. Francez, W.P. de Roever: A proof system for communicating sequential processes, ACM-TOPLAS, 2, 1, (July 1980).Google Scholar
  3. [BH]
    P. Brinch Hansen: Distributed processes — a concurrent programming concept. CACM 21, 11 (November 1978).Google Scholar
  4. [CC]
    P. Cousot, R. Cousot: Semantic analysis of communicating sequential processes. Proceedings of the 7-th Colloquium, Automata, Languages and Programming, Nordwijkerhout, July 1980.Google Scholar
  5. [CH]
    Z.C. Chen, A.A.R. Hoare: Partial correctness of communicating sequential processes. Proc. 2nd Int. Symp. on Distributed Systems, Paris (April 1981).Google Scholar
  6. [CM]
    K.M. Chandy, J. Misra: Proofs of networks of processes. IEEE-TSE, SE-7, No. 4 (July 1981).Google Scholar
  7. [D]
    E.W. Dijkstra: A Discipline of Programming. Prentice Hall, Englewood Cliffs, New Jersey, (1976).Google Scholar
  8. [E]
    Tz. Elrad: Ph.D. thesis, in preparation.Google Scholar
  9. [FE]
    J.A. Feldman: High level programming for distributed computing. CACM 22, 6 (June 1979).Google Scholar
  10. [FHLR]
    N. Francez, C.A.R. Hoare, D.J. Lehmann, W.P. de Roever: Semantics of nondeterminism, concurrency and communication, JCSS 19, 3 (December 1979).Google Scholar
  11. [FLP]
    N. Francez, D.J. Lehmann, A. Pnueli: A linear history semantics for distributed leanguages. Proc. FOCS Conf. (October 1980).Google Scholar
  12. [FS]
    L. Flon, N. Suzuki: Nondeterminism and the correctness of parallel programs. IFIP working conf. on Formal Description of Programming Concepts, Saint Andrews, 1977.Google Scholar
  13. [H]
    C.A.R. Hoare: Communicating sequential processes. CACM 21, 8 (August 1978).Google Scholar
  14. [LG]
    G. Levin, D. Gries: A proof technique for communicating sequential processes. Acta Informatica 15 (1981).Google Scholar
  15. [LS]
    A. Van Lamsweerde, M. Sintzoff: Formal derivation of strongly correct concurrent programs. Acta Informatica, Vol. 12, Fasc. 1, (1979).Google Scholar
  16. [MM]
    G. Milne, R. Milner: Concurrent processes and their syntax. JACM 26, 2 (April 1979).Google Scholar
  17. [OG]
    S.S. Owicki, D. Gries: An axiomatic proof technique for parallel programs I. Acta Informatica, 6 (1976).Google Scholar
  18. [MI]
    R. Milner: A Calculus of Communicating Processes. Lecture Notes in Computer Science, No. 92, Springer-Verlag (1980).Google Scholar
  19. [P]
    G.D. Plotkin: An operational semantics for CSP. Technical Report, Dept. of Computer Science, University of Edinburgh, October 1981.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1982

Authors and Affiliations

  • Tzilla Elrad
    • 1
  • Nissim Francez
    • 1
  1. 1.Dept. of Computer Science Technion — IITHaifaIsrael

Personalised recommendations