Skip to main content
SpringerLink
Log in

Proof rules for the programming language Euclid

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

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

  • 238 Accesses

Abstract

In the spirit of the previous axiomatization of the programming language Pascal, this paper describes Hoare-style proof rules for Euclid, a programming language intended for the expression of system programs which are to be verified. All constructs of Euclid are covered except for storage allocation and machine dependencies.

April 7, 1978 Accepted for Publication in ACTA INFORMATICA

Supported by the Defense Advanced Research Projects Agency under contract DAHC-15-72-C-0308.

Supported in part by the National Science Foundation under grant MCS-76-06089 and the Joint Services Electronics Program monitored by the Air Force Office of Scientific Research under contract F44620-76-C-0061.

Supported in part by a Research Leave Grant from the University of Toronto and a grant from the National Research Council of Canada. Current address

Supported in part by the Defense Advanced Research Projects Agency under contract DAHC-73-C-0368.

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. Clarke, E. M. Jr.: Programming language constructs for which it is impossible to obtain good Hoare-like axiom systems. Conference Record of the Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, pp. 10–20. New York: ACM 1977

    Google Scholar 

  2. Donahue, J. E.: Complementary Definitions of Programming Language Semantics. Lecture Notes in Computer Science, Vol. 42. Berlin-Heidelberg-New York: Springer 1976

    MATH  Google Scholar 

  3. Ernst, G. W.: Rules of inference for procedure calls. Acta Informatica 8, 145–152 (1977)

    Article  MathSciNet  Google Scholar 

  4. Guttag, J. V., Horning, J. J., and London, R. L.: A proof rule for Euclid procedures. Working Conference on Formal Description of Programming Concepts, Preprints of Technical Papers, (E. Neuhold, ed.), St. Andrews, New Brunswick, pp. 10.1–10.8. Publication by North Holland forthcoming. Also USC Information Sciences Institute, Technical Report ISI/RR-77-60, May 1977

    Google Scholar 

  5. Guttag, J. V., Horowitz, E., and Musser, D. R.: Abstract data types and software validation. USC Information Sciences Institute, Technical Report ISI/RR-76-48, August 1976

    Google Scholar 

  6. Hoare, C. A. R.: An axiomatic basis for computer programming. Comm. ACM 12, 576–580 and 583 (1969)

    Article  Google Scholar 

  7. Hoare, C. A. R.: Procedures and parameters: An axiomatic approach. In: Symposium on Semantics of Algorithmic Languages (E. Engeler, ed.), Lecture Notes in Mathematics, Vol. 188, pp. 102–116. Berlin-Heidelberg-New York: Springer 1971

    Chapter  Google Scholar 

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

    Article  Google Scholar 

  9. Hoare, C. A. R. and Wirth, N.: An axiomatic definition of the programming language PASCAL. Acta Informatica 2, 335–355 (1973)

    Article  Google Scholar 

  10. Jensen, K. and Wirth, N.: PASCAL User Manual and Report. Lecture Notes in Computer Science, Vol. 18, 2nd ed. Berlin-Heidelberg-New York: Springer 1975

    Book  Google Scholar 

  11. Lampson, B. W., Horning, J. J., London, R. L., Mitchell, J. G., and Popek, G. J.: Revised report on the programming language Euclid (to appear). An earlier version appeared in SIGPLAN Notices, 12, No. 2, February 1977

    Google Scholar 

  12. Musser, D. R.: A proof rule for functions. USC Information Sciences Institute, Technical Report ISI/RR-77-62, October 1977

    Google Scholar 

  13. Popek, G. J., Horning, J. J., Lampson, B. W., Mitchell, J. G., and London, R. L.: Notes on the design of Euclid. Proceedings of an ACM Conference on Language Design for Reliable Software, Raleigh, North Carolina, SIGPLAN Notices, 12, No. 3, 11–18 (1977)

    Article  Google Scholar 

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

    Article  Google Scholar 

  15. Wirth, N.: The programming language PASCAL. Acta Informatica 1, 35–63 (1971)

    Article  Google Scholar 

Download references

Author information

Author notes

  1. J. J. Horning

    Present address: Xerox Research Center, 3333 Coyote Hill Road, 94304, Palo Alto, CA

Authors and Affiliations

  1. USC Information Sciences Institute, 4676 Admiralty Way, 90291, Marina del Rey, CA, USA

    R. L. London

  2. Computer Science Department, University of Southern California, 90007, Los Angeles, CA

    J. V. Guttag

  3. Computer Systems Research Group, University of Toronto, M5S 1A4, Toronto, Canada

    J. J. Horning

  4. Xerox Research Center, 3333 Coyote Hill Road, 94304, Palo Alto, CA

    B. W. Lampson & J. G. Mitchell

  5. Computer Science Department, University of California, 3532 Boelter Hall, 90024, Los Angeles, CA

    G. J. Popek

Authors
  1. R. L. London
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. J. V. Guttag
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. J. J. Horning
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. B. W. Lampson
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. J. G. Mitchell
    View author publications

    You can also search for this author in PubMed Google Scholar

  6. G. J. Popek
    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

London, R.L., Guttag, J.V., Horning, J.J., Lampson, B.W., Mitchell, J.G., Popek, G.J. (1979). Proof rules for the programming language Euclid. In: Bauer, F.L., et al. Program Construction. Lecture Notes in Computer Science, vol 69. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014666

Download citation

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

  • 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