Abstract
This paper presents a method for specifying and proving compilers. This method is based on the algebraic data types ideas. The main points are :
-
to each language is associated an algebraic abstract data type.
-
the semantic value of a program is given as a term of this data type.
-
the translation of the semantic values of source programs into semantic values of target programs is specified and proved as the representation of an algebraic data type by another one.
A compiler generator, PERLUETTE, which accepts such specifications as input is described. The proof technic is discussed.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
P. BOULLIER. Le système SYNTAX, Manuel d'utilisation, Groupe Langages et Traducteur, IRIA, 1977.
P. BOULLIER. Automatic Syntatic Error Recovery for LR-Parsers, 5th Annual III Conference — Guidel, Mai 1977.
P.D. MOSSES. Mathematical Semantics and Compiler Generation. Ph.D. Thesis, Université d'Oxford, 1975.
P.D. MOSSES. SIS, a Compiler-Generator System using Denotational Semantics Dept. of Computer Science, Université d'Aarhus, June 1978.
M.C. GAUDEL. A formal Approach to Translator Specification, IFIP Congress, Toronto, 1977.
M.C. GAUDEL, Ph. DESCAMP, M. MAZAUD. Semantics of Procedures as an Algebraic Abstract Data Type, Rapport Laboria no 334–1978.
M.C. GAUDEL, C. PAIR. Construction de Compilateurs basée sur une Sémantique Formelle. Acte des journées francophones sur la certification du logiciel, Genève, 1979.
M.C GAUDEL, C. PAIR. The Use of a Formal Semantics to Produce and Prove Compilers. International Workshop on the Semantics of Programming Language. Bad Honnef. March 1979.
F. Lockwood MORRIS. Advice on Structuring Compilers and Proving them Correct. P.O.P.L. 1973.
J.V. GUTTAG, E. HOROWITZ, D.R. MUSSER. Abstract Data Types and Software Validation. CACM. December 1978.
J.W. THATCHER, E. WAGNER, J.B. WRIGHT. An Initial Algebra approach to the Specification, Correctness, and Implementation of Abstract Data Type. In Current Trends in Programming Methodology IV (R. Yeh. Ed). Prentice Hall 1979.
M.C. GAUDEL. An introduction to Algebraic Abstract Data Type. Lecture notes of the 2nd advanced course on Computing System Reliability. IRIA, Sept 1979.
M. GORDON, R. MILNER, C. WADSWORTH — Edinburgh LCF. Internal Report CSR-11-77 University of Edinburgh, Sept 1977.
D.R. MUSSER. A Data Type Verification System based on Rewrite Rules. 6th Texas Conference on Computing System, Austin, Nov. 1977.
D.R. MUSSER. Abstract Data Type Specification in the AFFIRM System. IEEE Transactions on Software Engineering (to appear).
D.E. KNUTH. Semantics of Context-free Languages, Math. Systems Theory, Vol. no5, no1, 1971.
B. LORHO. De la Définition à la Traduction des Langages de Programmation: la méthode des attributs sémantiques. Thèse d'Etat — Toulouse, 1974.
B. LORHO. DELTA: manuel d'utilisation, Groupe Langages et Traducteurs, IRIA, Nov. 1977.
M.C. DENDIEN-GAUDEL. Applications des Structures de Données à la description et à la preuve de Traducteurs. Congrès AFCET Informatique, Gif-sur-Yvette, Nov. 1976.
M.C. GAUDEL. Thesis, University of Nancy (France), March 1980.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1980 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Gaudel, M.C. (1980). Specification of compilers as abstract data type representations. In: Jones, N.D. (eds) Semantics-Directed Compiler Generation. SDCG 1980. Lecture Notes in Computer Science, vol 94. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-10250-7_21
Download citation
DOI: https://doi.org/10.1007/3-540-10250-7_21
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-10250-2
Online ISBN: 978-3-540-38339-0
eBook Packages: Springer Book Archive