The Euclid Language: a progress report

ABSTRACT

Euclid is a programming language for writing verifiable system programs. A compiler for Euclid is being implemented by the authors. Since its definition [1], the language has evolved largely in response to problems discovered in the course of implementation. This paper gives a summary of language changes, the status of the implementation and some observations about use of Euclid as a practical programming language.

REFERENCES

• 1: B. W. Lampson , J. J. Horning , R. L. London , J. G. Mitchell , G. J. Popek, Report on the programming language Euclid, ACM SIGPLAN Notices, v.12 n.2, p.1-79, February 1977 [doi>10.1145/954666.971189]
• 2: B.W. Lampson, J.J. Horning, R.L. London, J.G. Mitchell, and G.J. Popek, "Revised Report on the Programming Language Euclid", Xerox Palo Alto Research Center Technical Report CSL 78-2 (to appear).
• 3: G. J. Popek , J. J. Horning , B. W. Lampson , J. G. Mitchell , R. L. London, Notes on the design of Euclid, Proceedings of an ACM conference on Language design for reliable software, p.11-18, March 28-30, 1977, Raleigh, North Carolina
• 4: W.D. Elliott and D.T. Barnard (eds.), "Notes on Euclid", Computer Systems Research Group, University of Toronto, Technical Report CSRG-82, August 1977 (also in SIGPLAN Notices13, 3 (March 1978)).
• 5: J.V. Guttag, J.J. Horning, and R.L. London, "A Proof Rule for Euclid Procedures", in E. Neuhold (ed.), Working Conference on Formal Description of Programming Concepts, North Holland Publishing Co., pp. 211-220, (to appear) (also USC Information Sciences Institute Technical Report ISI/RR-77-60, (May 1977)).
• 6: R.L. London, 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
• 7: D.B. Wortman, "On Legality Assertions in Euclid", (IEEE Transactions on Software Engineering, to appear).
• 8: Donald E. Knuth, The remaining trouble spots in ALGOL 60, Communications of the ACM, v.10 n.10, p.611-618, Oct. 1967 [doi>10.1145/363717.363743]
• 9: B. L. Clark , J. J. Horning, Reflections on a language designed to write an operating system, ACM SIGPLAN Notices, v.8 n.9, p.52-56, September 1973
• 10: Dennis M. Ritchie , Ken Thompson, The UNIX time-sharing system, Communications of the ACM, v.17 n.7, p.365-375, July 1974 [doi>10.1145/361011.361061]
• 11: N. Wirth, "Modula: A language for modular multiprogramming", Software - Practice and Experience7,1 (January-February 1977), pp. 3-35.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications

          Nouns: EUCLID

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.4 Processors
          Subjects: Compilers

General Terms:
Languages

Keywords:
Aliasing, Data encapsulation, Euclid, Language, Legality assertions, Machine dependencies, Parameterized types, Pascal, Reliability, Storage allocation, Systems programming, Verification, Visibility of names