Euclid programming language
Encyclopedia
Euclid is an imperative programming language for writing verifiable
programs. It was designed by Butler Lampson
and associates at the Xerox PARC
lab in the mid 1970s. The implementation was led by Ric Holt
at the University of Toronto
and James Cordy
was the principal programmer for the first implementation of the compiler
. It was originally designed for the Motorola 6809
microprocessor. It was considered innovative for the time; the compiler development team had a $2 million budget over 2 years and was commissioned by the Defense Advanced Research Projects Agency
of the U.S. Department of Defense
and the Canadian Department of National Defence
. It was used for a few years at I. P. Sharp Associates
, MITRE Corporation
, SRI International
and various other international institutes for research in systems programming and secure software systems.
Euclid is descended from the Pascal programming language. Functions in Euclid are closed scopes, may not have side effects, and must explicitly declare imports. Euclid also disallows goto
s, floating point numbers, global assignments, nested function
s and aliases, and none of the actual parameters to a function can refer to the same thing. Euclid implements modules as types. Descendants of Euclid include the Mesa programming language
, the Concurrent Euclid programming language and the Turing programming language
.
Formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics .- Usage :Formal verification can be...
programs. It was designed by Butler Lampson
Butler Lampson
Butler W. Lampson is a renowned computer scientist.After graduating from the Lawrenceville School , Lampson received his Bachelor's degree in Physics from Harvard University in 1964, and his Ph.D...
and associates at the Xerox PARC
Xerox PARC
PARC , formerly Xerox PARC, is a research and co-development company in Palo Alto, California, with a distinguished reputation for its contributions to information technology and hardware systems....
lab in the mid 1970s. The implementation was led by Ric Holt
Ric Holt
Richard C. "Ric" Holt is a computer science professor.Ric Holt was one of the original developers of the Turing programming language, , Euclid programming language, SP/k, and of the S/SL programming language...
at the University of Toronto
University of Toronto
The University of Toronto is a public research university in Toronto, Ontario, Canada, situated on the grounds that surround Queen's Park. It was founded by royal charter in 1827 as King's College, the first institution of higher learning in Upper Canada...
and James Cordy
James Cordy
James Reginald Cordy, born , is a Canadian computer scientist and educator who is a Professor in the School of Computing at Queen's University. As a researcher he is currently active in the fields of source code analysis and manipulation, software reverse and re-engineering, and pattern analysis...
was the principal programmer for the first implementation of the compiler
Compiler
A compiler is a computer program that transforms source code written in a programming language into another computer language...
. It was originally designed for the Motorola 6809
Motorola 6809
The Motorola 6809 is an 8-bit microprocessor CPU from Motorola, designed by Terry Ritter and Joel Boney and introduced 1978...
microprocessor. It was considered innovative for the time; the compiler development team had a $2 million budget over 2 years and was commissioned by the Defense Advanced Research Projects Agency
Defense Advanced Research Projects Agency
The Defense Advanced Research Projects Agency is an agency of the United States Department of Defense responsible for the development of new technology for use by the military...
of the U.S. Department of Defense
United States Department of Defense
The United States Department of Defense is the U.S...
and the Canadian Department of National Defence
Department of National Defence (Canada)
The Department of National Defence , frequently referred to by its acronym DND, is the department within the government of Canada with responsibility for all matters concerning the defence of Canada...
. It was used for a few years at I. P. Sharp Associates
I. P. Sharp Associates
I. P. Sharp Associates, IPSA for short, was a major Canadian computer time sharing, consulting and services firm of the 1970s and 80s. IPSA is particularly well known for its work on the APL programming language, an early packet switching computer network known as IPSANET, and a powerful...
, MITRE Corporation
MITRE
The Mitre Corporation is a not-for-profit organization based in Bedford, Massachusetts and McLean, Virginia...
, SRI International
SRI International
SRI International , founded as Stanford Research Institute, is one of the world's largest contract research institutes. Based in Menlo Park, California, the trustees of Stanford University established it in 1946 as a center of innovation to support economic development in the region. It was later...
and various other international institutes for research in systems programming and secure software systems.
Euclid is descended from the Pascal programming language. Functions in Euclid are closed scopes, may not have side effects, and must explicitly declare imports. Euclid also disallows goto
Goto
goto is a statement found in many computer programming languages. It is a combination of the English words go and to. It performs a one-way transfer of control to another line of code; in contrast a function call normally returns control...
s, floating point numbers, global assignments, nested function
Nested function
In computer programming, a nested function is a function which is lexically encapsulated within another function. It can only be called by the enclosing function or by functions directly or indirectly nested within the same enclosing function. In other words, the scope of the nested function is...
s and aliases, and none of the actual parameters to a function can refer to the same thing. Euclid implements modules as types. Descendants of Euclid include the Mesa programming language
Mesa programming language
Mesa was an innovative programming language developed in the late 1970s at the Xerox Palo Alto Research Center in Palo Alto, California, United States. The language was named after the mesas of the American Southwest, referring to its design intent to be a "high-level" programming language.Mesa is...
, the Concurrent Euclid programming language and the Turing programming language
Turing programming language
Turing is a Pascal-like programming language developed in 1982 by Ric Holt and James Cordy, then of University of Toronto, Canada. Turing is a descendant of Euclid, Pascal and SP/k that features a clean syntax and precise machine-independent semantics....
.
External links
- B.W. Lampson, J.J. Horning, R.L. London, J.G. Mitchell and G.J. Popek 1977. Report on the programming language Euclid. SIGPLAN Notices 12, 2 (February 1977), 1-79.
- R.C. Holt, D.B. Wortman, J.R. Cordy and D.R. Crowe 1978. The Euclid Language: a progress report. In Proceedings of the 1978 Annual Conference (Washington, D.C., United States, December 04 - 06, 1978), 111-115.
- D.B. Wortman and J.R. Cordy 1981. Early experiences with Euclid. In Proc. 5th international Conference on Software Engineering (San Diego, California, United States, March 09 - 12, 1981), 27-32.