Skip to main content
SpringerLink
Log in

Composition: A Way to Make Proofs Harder

  • Conference paper
  • First Online:
Compositionality: The Significant Difference (COMPOS 1997)

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

Included in the following conference series:

Abstract

Compositional reasoning about a system means writing its specification as the parallel composition of components and reasoning separately about each component. When distracting language issues are removed and the underlying mathematics is revealed, compositional reasoning is seen to be of little use.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Martín Abadi and Leslie Lamport. The existence of refinement mappings. Theoretical Computer Science, 82(2):253–284, May 1991.

    Google Scholar 

  2. Martín Abadi and Leslie Lamport. Conjoining specifications. ACM Transactions on Programming Languages and Systems, 17(3):507–534, May 1995.

    Google Scholar 

  3. Yehuda Afek, Geoffrey Brown, and Michael Merritt. Lazy caching. ACM Transactions on Programming Languages and Systems, 15(1):182–205, January 1993.

    Google Scholar 

  4. Bowen Alpern and Fred B. Schneider. Defining liveness. Information Processing Letters, 21(4):181–185, October 1985.

    Google Scholar 

  5. E. A. Ashcroft. Proving assertions about parallel programs. Journal of Computer and System Sciences, 10:110–135, February 1975.

    Google Scholar 

  6. Edsger W. Dijkstra. A personal summary of the Gries-Owicki theory. In Edsger W. Dijkstra, editor, Selected Writings on Computing: A Personal Perspective, chapter EWD554, pages 188–199. Springer-Verlag, New York, Heidelberg, Berlin, 1982.

    Google Scholar 

  7. R. P. Kurshan and Leslie Lamport. Verification of a multiplier: 64 bits and beyond. In Costas Courcoubetis, editor, Computer-Aided Verification, volume 697 of Lecture Notes in Computer Science, pages 166–179, Berlin, June 1993. Springer-Verlag. Proceedings of the Fifth International Conference, CAV’93.

    Google Scholar 

  8. Leslie Lamport. Proving the correctness of multiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125–143, March 1977.

    Google Scholar 

  9. Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872–923, May 1994.

    Google Scholar 

  10. Leslie Lamport. How to write a proof. American Mathematical Monthly, 102(7):600–608, August–September 1995.

    Google Scholar 

  11. S. Owicki and D. Gries. An axiomatic proof technique for parallel programs I. Acta Informatica, 6(4):319–340, 1976.

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Systems Research Center, Digital Equipment Corporation, USA

    Leslie Lamport

Authors
  1. Leslie Lamport
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Informatics and Applied Mathematics, Christian Albrechts University at Kiel, Preußerstr. 1-9, D-24105, Kiel, Germany

    Willem-Paul de Roever  & Hans Langmaack  & 

  2. Department of Applied Mathematics and Computer Science, Weizmann Institute of Science, P.O. Box 26, Rehovot, 76100, Israel

    Amir Pnueli

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Lamport, L. (1998). Composition: A Way to Make Proofs Harder. In: de Roever, WP., Langmaack, H., Pnueli, A. (eds) Compositionality: The Significant Difference. COMPOS 1997. Lecture Notes in Computer Science, vol 1536. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49213-5_15

Download citation

  • DOI: https://doi.org/10.1007/3-540-49213-5_15

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-65493-3

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation