Skip to main content
SpringerLink
Log in
Book cover

International Conference on Foundations of Software Technology and Theoretical Computer Science

FSTTCS 1984: Foundations of Software Technology and Theoretical Computer Science pp 443–465Cite as

Proof rules for communication abstractions

  • Session 7 Algorithms And Complexity
  • Conference paper
  • First Online:

  • 113 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 181))

Abstract

A modular proof system is presented for proving partial correctness and freedom from deadlock of concurrent programs using scripts (including recursive scripts). Its applications to augmentations of CSP and a subset of ADA are discussed. The proof rules are a generalization of both the procedure rules and the concurrency rules. Correctness proofs for examples are presented.

This is a preview of subscription content, log in via an institution.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Apt, K.R., Francez, N., and de Roever, W.P. A proof system for communicating sequential processes. ACM Trans. Prog. Lang. Syst. 2,3 (July 1980), 359–385.

    Google Scholar 

  2. Apt, K.R., Ten years of Hoare logic: A survey-part 1. ACM Trans. Prog. Lang. Syst. 3,4 (October 1981), 431–483.

    Google Scholar 

  3. Apt, K.R., Formal justification of proof system for communicating sequential processes. ACM Trans. Prog. Lang. Syst. 30,1 (January 1983), 197–216.

    Google Scholar 

  4. Elrad, T., Francez, N. Decomposition of distributed programs into communication-close layers. Science of Computer Programming 2 (1982) 155–173, North-Holland.

    Google Scholar 

  5. Francez, N., and Hailpern, B. Script: A communication abstraction mechanism. ACM-SIGACT 2 nd annual PODC conf., Montreal, (August 1983).

    Google Scholar 

  6. Gries, D., and Levin, G. Assignment and procedure call proof rules. ACM Trans. Prog. Lang. Syst. 2,4 (October 1980), 564–579.

    Google Scholar 

  7. Gerth, R., and de Roever, W.P. A proof system for concurrent ada programs. to appear in SCP. Tech. Rep. RUU-CS-83-2, U. of Utrecht, October 1983.

    Google Scholar 

  8. Hoare, C.A.R. Procedures and parameters: An axiomatic approach. In Symp. Semantics of Algorithmic Languages, E. Engeler, Ed., Notes in Mathematics 188, Springer-Verlag, New York, 1971, 102–116.

    Google Scholar 

  9. Hoare, C.A.R. Communicating sequential processes. Commun. ACM 21,8 (August 1978), 666–677.

    Google Scholar 

  10. Owicki, S.S., and Gries, D. An axiomatic proof technique for parallel programs. I. Acta Inf. 6, 1976, 319–340.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Computer Science dept., Technion — Israel Institute of Technology, 32000, Haifa, Israel

    Gadi Taubenfeld & Nissim Francez

Authors
  1. Gadi Taubenfeld
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Nissim Francez
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mathai Joseph Rudrapatna Shyamasundar

Rights and permissions

Reprints and permissions

Copyright information

© 1984 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Taubenfeld, G., Francez, N. (1984). Proof rules for communication abstractions. In: Joseph, M., Shyamasundar, R. (eds) Foundations of Software Technology and Theoretical Computer Science. FSTTCS 1984. Lecture Notes in Computer Science, vol 181. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-13883-8_90

Download citation

  • DOI: https://doi.org/10.1007/3-540-13883-8_90

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-13883-9

  • Online ISBN: 978-3-540-39087-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation