Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Specifications and proofs for abstract data types in concurrent programs

  • II. Program Verification
  • Chapter
  • First Online:
Program Construction

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

Abstract

Shared abstract data types, such as queues and buffers, are useful tools for building well-structured concurrent programs. This paper presents a method for specifying shared types in a way that simplifies concurrent program verification. The specifications describe the operations of the shared type in terms of their effect on variables of the process invoking the operation. This makes it possible to verify the processes independently, reducing the complexity of the proof. The key to defining such specifications is the concept of a private variable: a variable which is part of a shared object but belongs to just one process. Shared types can be implemented using an extended form of monitors; proof rules are given for verifying that a monitor correctly implements its specifications. Finally, it is shown how concurrent programs can be verified using the specifications of their shared types. The specification and proof techniques are illustrated with a number of examples involving a shared bounded buffer.

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 54.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 69.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. P. Brinch Hansen. Operating Systems Principles. Prentice Hall, Englewood Cliffs, New Jersey, (1973).

    MATH  Google Scholar 

  2. P. Brinch Hansen. The programming language concurrent Pascal. IEEE Trans. on Software Eng., SE-1 No. 2, (June, 1975), pp. 199–207.

    Google Scholar 

  3. D.I. Good and A.L. Ambler. Proving systems of concurrent processes synchronized with message buffers. Draft, (1975).

    Google Scholar 

  4. J.V. Guttag. The specification and application to programming of abstract data types. Ph.D. thesis, Computer Science, University of Toronto, (Sept. 1975).

    Google Scholar 

  5. J.V. Guttag, E. Horowitz, D.R. Musser. Abstract data types and software validation. Univ. of Southern California Information Sciences Institute report 76–48, (August, 1976).

    Google Scholar 

  6. C.A.R. Hoare. An axiomatic basis for computer programming. Comm. ACM 12, 10 (Oct. 1969), pp. 576–583.

    Article  Google Scholar 

  7. C.A.R. Hoare. Procedures and parameters—an axiomatic approach. Symp. on the Semantics of Algorithmic Languages, Springer, Berlin-Heidelberg-New York, (1971), pp. 102–116.

    Chapter  Google Scholar 

  8. C.A.R. Hoare. Proof of correctness of data representations. Acta Informatica 1 (1972), pp. 271–281.

    Article  Google Scholar 

  9. C.A.R. Hoare. A structured paging system. Computer J. 16, 3 (1973), pp. 209–215.

    Article  Google Scholar 

  10. C.A.R. Hoare. Monitors: an operating system structuring concept. Comm. ACM 17, 10 (Oct. 1974), pp. 549–556.

    Article  Google Scholar 

  11. J.H. Howard. Proving monitors. Comm. ACM 19, 5 (May 1976), pp. 273–279.

    Article  Google Scholar 

  12. L. Lamport. Formal correctness proofs for multiprocess algorithms. Proc. Second Int. Symp. on Programming, April 1976.

    Google Scholar 

  13. B.H. Liskov and S. Zilles. Specification techniques for data abstractions. IEEE Trans. on Software Eng. SE-1, 1 (March 1975), pp. 7–19.

    Article  Google Scholar 

  14. B.H. Liskov and V. Berzins. An appraisal of program specifications. Computation Structures Group Memo 141, M.I.T. (July 1976).

    Google Scholar 

  15. Z. Manna and A. Pnueli. Axiomatic approach to total correctness of programs. Acta Informatica 3 (1974) pp. 243–263.

    Article  MathSciNet  Google Scholar 

  16. P.G. Neumann, L. Robinson, K.N. Levitt, R.S. Boyer, A.R. Saxena. A provably secure operating system. Stanford Research Institute, Menlo Park, California (June 1975).

    Google Scholar 

  17. S.S. Owicki. A consistent and complete deductive system for the verification of parallel programs. Proc. 8thACM Symp. on Theory of Computing, (May 1976), pp. 73–86.

    Google Scholar 

  18. S.S. Owicki and D. Gries. Verifying properties of parallel programs: an axiomatic approach. Comm. ACM 19, 5 (May 1976), pp. 280–285.

    Article  MathSciNet  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  20. D.L. Parnas. A technique for the specification of software modules, with examples. Comm. ACM 15, 5 (May 1972), pp. 330–336.

    Article  Google Scholar 

  21. V. Schorre. A program verifier with assertions in terms of abstract data. Systems Development Corporation report SP 3841, Santa Monica, California.

    Google Scholar 

  22. M. Shaw. Abstraction and verification in Alphard: design and verification of a tree handler. Computer Science Department, Carnegie-Mellon University, (June 1976).

    Google Scholar 

  23. J. Spitzen and B. Wegbreit. The verification and synthesis of data structures. Acta Informatica 4 (1975), pp. 127–144.

    Article  Google Scholar 

  24. W.A. Wulf, R.L. London, and M. Shaw. An introduction to the construction and verification of Alphard programs. IEEE Trans. on Software Eng., SE-2, 4 (December, 1976), pp. 253–265.

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Digital Systems Laboratory Departments of Electrical Engineering and Computer Science, Stanford University, 94305, Stanford, California, USA

    Susan S. Owicki

Authors
  1. Susan S. Owicki
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Friedrich L. Bauer Manfred Broy E. W. Dijkstra S. L. Gerhart D. Gries M. Griffiths J. V. Guttag J. J. Horning S. S. Owicki C. Pair H. Partsch P. Pepper M. Wirsing H. Wössner

Rights and permissions

Reprints and permissions

Copyright information

© 1979 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Owicki, S.S. (1979). Specifications and proofs for abstract data types in concurrent programs. In: Bauer, F.L., et al. Program Construction. Lecture Notes in Computer Science, vol 69. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014668

Download citation

  • DOI: https://doi.org/10.1007/BFb0014668

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-35312-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation