Proof rules for the programming language Euclid

  • R. L. London
  • J. V. Guttag
  • J. J. Horning
  • B. W. Lampson
  • J. G. Mitchell
  • G. J. Popek
II. Program Verification
Part of the Lecture Notes in Computer Science book series (LNCS, volume 69)


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.


Module Rule Defense Advance Research Project Agency Proof Rule Module Definition Abstraction Function 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 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 1977Google Scholar
  2. 2.
    Donahue, J. E.: Complementary Definitions of Programming Language Semantics. Lecture Notes in Computer Science, Vol. 42. Berlin-Heidelberg-New York: Springer 1976Google Scholar
  3. 3.
    Ernst, G. W.: Rules of inference for procedure calls. Acta Informatica 8, 145–152 (1977)Google Scholar
  4. 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 1977Google Scholar
  5. 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 1976Google Scholar
  6. 6.
    Hoare, C. A. R.: An axiomatic basis for computer programming. Comm. ACM 12, 576–580 and 583 (1969)Google Scholar
  7. 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 1971Google Scholar
  8. 8.
    Hoare, C. A. R.: Proof of correctness of data representations. Acta Informatica 1, 271–281 (1972)Google Scholar
  9. 9.
    Hoare, C. A. R. and Wirth, N.: An axiomatic definition of the programming language PASCAL. Acta Informatica 2, 335–355 (1973)Google Scholar
  10. 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 1975Google Scholar
  11. 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 1977Google Scholar
  12. 12.
    Musser, D. R.: A proof rule for functions. USC Information Sciences Institute, Technical Report ISI/RR-77-62, October 1977Google Scholar
  13. 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)Google Scholar
  14. 14.
    Spitzen, J. and Wegbreit, B.: The verification and synthesis of data structures. Acta Informatica 4, 127–144 (1975)Google Scholar
  15. 15.
    Wirth, N.: The programming language PASCAL. Acta Informatica 1, 35–63 (1971)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1979

Authors and Affiliations

  • R. L. London
    • 1
  • J. V. Guttag
    • 2
  • J. J. Horning
    • 3
  • B. W. Lampson
    • 4
  • J. G. Mitchell
    • 4
  • G. J. Popek
    • 5
  1. 1.USC Information Sciences InstituteMarina del Rey
  2. 2.Computer Science DepartmentUniversity of Southern CaliforniaLos Angeles
  3. 3.Computer Systems Research GroupUniversity of TorontoTorontoCanada
  4. 4.Xerox Research CenterPalo Alto
  5. 5.Computer Science DepartmentUniversity of CaliforniaLos Angeles

Personalised recommendations