A demonstrably correct compiler
- 1 January 1991
- journal article
- research article
- Published by Association for Computing Machinery (ACM) in Formal Aspects of Computing
- Vol. 3 (1) , 58-101
- https://doi.org/10.1007/bf01211435
Abstract
As critical applications grow in size and complexity, high level languages, rather than better-trusted assembly languages, will be used in their development. This adds potential for extra errors to creep in, especially in the now necessary compiler. To avoid these new errors, it is necessary to have a formal specification of the high level language, and a formal development of its compiler. We outline what we believe is a practical route for achieving a demonstrably correct compiler, and describe a prototype compiler we have built by this route for a small, but non-trivial, language.Keywords
This publication has 15 references indexed in Scilit:
- Reliable programming in standard languagesPublished by Springer Nature ,1989
- A Proof of Correctness of the Viper Microprocessor: The First LevelPublished by Springer Nature ,1988
- Formal specification of an access control systemSoftware: Practice and Experience, 1987
- Information-flow and data-flow analysis of while-programsACM Transactions on Programming Languages and Systems, 1985
- A semantics-directed compiler generatorPublished by Association for Computing Machinery (ACM) ,1982
- Logic programming and compiler writingSoftware: Practice and Experience, 1980
- Abstract interpretation: a unified lattice model for static analysis of programs by construction or approximation of fixpointsPublished by Association for Computing Machinery (ACM) ,1977
- Advice on structuring compilers and proving them correctPublished by Association for Computing Machinery (ACM) ,1973
- Semantics of context-free languagesTheory of Computing Systems, 1968
- Correctness of a compiler for arithmetic expressionsProceedings of Symposia in Applied Mathematics, 1967