Verification of Euclid programs
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.
KeywordsProof Theory Proof Obligation Verification Condition Axiom Schema Proof Rule
Unable to display preview. Download preview PDF.
- Ashcroft, E. A., M. Clint, and C. A. R. Hoare . “Remarks on ‘Program proving: Jumps and functions' by M. Clint and C. A. R. Hoare.” Acta Informatica 6, pp. 317–318.Google Scholar
- Clarke, E. M. Jr. . “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
- Clint, M., and C. A. R. Hoare . “Program proving: Jumps and functions.” Acta Informatica 1, pp. 214–224.Google Scholar
- Guttag, John V., James J. Horning, and Ralph L. London . “A proof rule for Euclid Procedures.” In Formal Description of Programming Concepts, ed. E. J. Neuhold, pp. 211–220, North-Holland, Amsterdam.Google Scholar
- Hoare, C. A. R. and N. Wirth . “An axiomatic definition of the programming language Pascal.” Acta Informatica 2, pp. 335–355.Google Scholar
- Ichbiah, J. D., J. P. Rissen, and J. C. Heliard . “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
- —,—, and — . “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
- Lampson, B. W., J. J. Horning, R. L. London, J. G. Mitchell, and G. J. Popek . “Report on the programming language Euclid.” SIGPLAN Notices 12, no. 2.Google Scholar
- London, R. L., J. V. Guttag, J. J. Horning, B. W. Lampson, J. G. Mitchell, and G. J. Popek . “Proof rules for the programming language Euclid.” Acta Informatica 10, pp. 1–26.Google Scholar
- Musser, David R. . “A proof rule for functions.” University of Southern California Information Sciences Institute Technical Report ISI/RR-77-62.Google Scholar
- Parnas, D. L. . “Information distribution aspects of design methodology.” In Proc. IFIP Congress 71. pp. 339–344, North-Holland, Amsterdam.Google Scholar
- SIGPLAN . Special issue on data: abstraction, definition, and structure. SIGPLAN Notices 11.Google Scholar
- Wirth, N. . “The programming language Pascal.” Acta Informatica 1, pp. 35–63.Google Scholar
- — . “Modula: A language for modular multiprogramming.” Software—Practice and Experience 7, pp. 3–35.Google Scholar
- —, and K. Jensen . Pascal—User Manual and Report, Springer-Verlag, New York.Google Scholar