Skip to main content

A case study in language design: Euclid

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

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

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

eBook
USD 16.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

  • Dijkstra, E. W. [1976]. A Discipline of Programming. Prentice-Hall, Englewood Cliffs.

    MATH  Google Scholar 

  • Fischer, Charles N., and Richard J. LeBlanc [1977]. “Efficient implementation and Optimization of run-time checking in Pascal.” SIGPLAN Notices 12, no. 3, pp. 19–24.

    Article  Google Scholar 

  • Habermann, A. N. [1973]. “Critical comments on the programming language Pascal.” Acta Informatica 3, pp. 47–57.

    Article  Google Scholar 

  • Hoare, C. A. R. [1973]. “Hints on programming language design.” Technical Report STAN-CS-73-403, Stanford University Computer Science Department.

    Google Scholar 

  • — [1975]. “Recursive data structures.” Int. J. Comp. Inf. Sci. 4, p. 105.

    Article  Google Scholar 

  • — and Wirth [1973]. “An axiomatic definition of the programming language Pascal.” Acta Informatica 2, pp. 335–355.

    Article  Google Scholar 

  • 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 

  • 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.

    Article  Google Scholar 

  • Luckham, D., and N. Suzuki [1976]. “Automatic program verification V: Verification-oriented proof rules for arrays, records, and pointers.” Technical Report STAN-CS-76-549, Stanford University Computer Science Department.

    Google Scholar 

  • MOHLL [1975]. Machine Oriented Higher Level Languages. ed. W. L. van der Poel and L. A. Maarssen, North-Holland, Amsterdam.

    Google Scholar 

  • Popek, G. J., J. J. Horning, B. W. Lampson, R. L. London, J. G. Mitchell [1977]. “Notes on the design of Euclid.” SIGPLAN Notices 12, no. 3, pp. 11–18.

    Article  Google Scholar 

  • SIGPLAN [1976]. Special issue on data: abstraction, definition, and structure. SIGPLAN Notices 11.

    Google Scholar 

  • Wegbreit, B., and J. Spitzen [1976]. “Proving properties of complex data structures.” J. ACM 23, no. 2, pp. 389–396.

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

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

Horning, J.J. (1979). A case study in language design: Euclid. In: Bauer, F.L., et al. Program Construction. Lecture Notes in Computer Science, vol 69. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0014665

Download citation

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

  • 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