Advertisement

Verification of Euclid programs

  • J. J. Horning
II. Program Verification
Part of the Lecture Notes in Computer Science book series (LNCS, volume 69)

Abstract

The proof rules for the programming language Euclid are closely modelled on the axiomatic definition of Pascal. However, there is intended to be a much closer correspondence between the language as actually implemented and the proof rules. This has been achieved by a combination of language changes, more stringent requirements on the compiler, and modifications of the proof rules. Several novel features of Euclid were introduced specifically in response to problems and limitations of the Pascal definition.

Typical proof rules and proofs for programs using basic language constructs are very similar in Euclid and Pascal. We discuss some of these as a review of Hoare's methodology.

The proof rules for Euclid functions and procedures deviate from those for Pascal, and avoid some of their problems. We discuss the reasons for some of the changes.

Some parts of the Euclid language, such as modules and zones, were motivated by application or implementation considerations. These have been more difficult to axiomatize, and have proved to be some of the most troublesome parts of the language. We mention a few of the problem areas.

These notes should be read in conjunction with the published proof rules.

Keywords

Proof Theory Proof Obligation Verification Condition Axiom Schema Proof Rule 
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.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Ashcroft, E. A., M. Clint, and C. A. R. Hoare [1976]. “Remarks on ‘Program proving: Jumps and functions' by M. Clint and C. A. R. Hoare.” Acta Informatica 6, pp. 317–318.Google Scholar
  2. Clarke, E. M. Jr. [1977]. “Programming language constructs for which it is impossible to obtain good Hoare-like axiom systems.” Conference Record, Fourth ACM Symposium on Principles of Programming Languages, Los Angeles, pp. 10–20.Google Scholar
  3. Clint, M., and C. A. R. Hoare [1972]. “Program proving: Jumps and functions.” Acta Informatica 1, pp. 214–224.Google Scholar
  4. Guttag, John V., James J. Horning, and Ralph L. London [1978]. “A proof rule for Euclid Procedures.” In Formal Description of Programming Concepts, ed. E. J. Neuhold, pp. 211–220, North-Holland, Amsterdam.Google Scholar
  5. Hoare, C. A. R. and N. Wirth [1973]. “An axiomatic definition of the programming language Pascal.” Acta Informatica 2, pp. 335–355.Google Scholar
  6. Ichbiah, J. D., J. P. Rissen, and J. C. Heliard [1973]. “The two-level approach to data definition and space management in the LIS system implementation language.” SIGPLAN Notices 8, no. 9, pp. 79–81.Google Scholar
  7. —,—, and — [1974]. “The two-level approach to data independent programming in the LIS system implementation language.” In Machine Oriented Higher Level Languages, ed. W. L. van der Poel and L. A. Maarssen, pp. 161–174, North-Holland, Amsterdam.Google Scholar
  8. Lampson, B. W., J. J. Horning, R. L. London, J. G. Mitchell, and G. J. Popek [1977]. “Report on the programming language Euclid.” SIGPLAN Notices 12, no. 2.Google Scholar
  9. London, R. L., J. V. Guttag, J. J. Horning, B. W. Lampson, J. G. Mitchell, and G. J. Popek [1978]. “Proof rules for the programming language Euclid.” Acta Informatica 10, pp. 1–26.Google Scholar
  10. Musser, David R. [1977]. “A proof rule for functions.” University of Southern California Information Sciences Institute Technical Report ISI/RR-77-62.Google Scholar
  11. Parnas, D. L. [1971]. “Information distribution aspects of design methodology.” In Proc. IFIP Congress 71. pp. 339–344, North-Holland, Amsterdam.Google Scholar
  12. SIGPLAN [1976]. Special issue on data: abstraction, definition, and structure. SIGPLAN Notices 11.Google Scholar
  13. Wirth, N. [1971]. “The programming language Pascal.” Acta Informatica 1, pp. 35–63.Google Scholar
  14. — [1977]. “Modula: A language for modular multiprogramming.” Software—Practice and Experience 7, pp. 3–35.Google Scholar
  15. —, and K. Jensen [1974]. Pascal—User Manual and Report, Springer-Verlag, New York.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1979

Authors and Affiliations

  • J. J. Horning
    • 1
  1. 1.Xerox Palo Alto Research CenterUSA

Personalised recommendations