Skip to main content
SpringerLink
Log in

A compositional reformulation of Owicki-Gries's partial correctness logic for a concurrent while language

  • Conference paper
  • First Online:
Automata, Languages and Programming (ICALP 1986)

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

Included in the following conference series:

Abstract

A straightforward compositional reformulation of Owicki-Gries's Hoare logic for a parallel while language is presented. The reformulation involves a Hoare quintuple (Γ,Δ) ⊢ {A} p {B} where Γ,Δ are sets of first-order formulas. It is shown that the quintuple has an interesting semantics which suggests a generalization of the proof system.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. K. Abrahamson "Modal logic of concurrent programs" LNCS 70 pp. 21–33 (1979).

    Google Scholar 

  2. K. Apt "Recursive assertions and parallel programs" Acta Informatica pp. 219–32 (1981).

    Google Scholar 

  3. H. Barringer, R. Kuiper and A. Pnueli "Now you may compare temporal logic specifications" Proc. STOC (1984).

    Google Scholar 

  4. S. Brookes "An axiomatic treatment of a parallel programming language" LNCS 193 (1985).

    Google Scholar 

  5. N. Francez, A. Pnueli "A proof method for cyclic programs" Acta Informatica pp. 133–157 (1978).

    Google Scholar 

  6. R. Gerth "Transition logic" Proc. STOC (1983).

    Google Scholar 

  7. M. Hennessy, G. Plotkin "Full abstraction for a simple parallel programming language" LNCS 74 pp. 108–120 (1979).

    Google Scholar 

  8. C. Jones "Specification and design of (parallel) programs" IFIP pp. 321–32 (1983).

    Google Scholar 

  9. L. Lamport "The Hoare logic of concurrent programs" Acta Informatica pp. 21–37 (1980).

    Google Scholar 

  10. J. Misra and K. Chandy "Proofs of networks of processes" IEEE Transactions on Software Engineering pp. 417–26 (1981).

    Google Scholar 

  11. S. Owicki "Axiomatic Proof Techniques for Parallel Programs" Ph.D. thesis, Cornell (1975).

    Google Scholar 

  12. S. Owicki, D. Gries "An axiomatic proof technique for parallel programs I" Acta Informatica pp. 319–40 (1976).

    Google Scholar 

  13. J. Reynolds "The Craft of Programming" Prentice-Hall (1981).

    Google Scholar 

  14. N. Soundararajan "A proof technique for parallel programs" Theoretical Computer Science pp. 13–29 (1984).

    Google Scholar 

  15. J. Zwiers, W. de Roever, P. van Emde Boas "Compositionality and concurrent networks: soundness and completeness of a proof system" LNCS 194 (1985).

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Dept. of Computer Science, University of Edinburgh, UK

    Colin Stirling

Authors
  1. Colin Stirling
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Laurent Kott

Rights and permissions

Reprints and permissions

Copyright information

© 1986 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Stirling, C. (1986). A compositional reformulation of Owicki-Gries's partial correctness logic for a concurrent while language. In: Kott, L. (eds) Automata, Languages and Programming. ICALP 1986. Lecture Notes in Computer Science, vol 226. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-16761-7_90

Download citation

  • DOI: https://doi.org/10.1007/3-540-16761-7_90

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-16761-7

  • Online ISBN: 978-3-540-39859-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation