An Automatically Generated and Provably Correct Compiler for a Subset of Ada
DOI:
https://doi.org/10.7146/dpb.v21i383.6615Abstract
We describe the automatic generation of a provably correct compiler for a non-trivial subset of Ada. The compiler is generated from an action semantic description; it emits absolute code for an abstract RISC machine language that currently is assembled into code for the SPARC and the HP Precision Architecture. The generated code is an order of magnitude better than what is produced by compilers generated by the classical systems of Mosses, Paulson, and Wand. The use of action semantics makes the processable language specification easy to read and pleasant to work with.Downloads
Published
1992-01-01
How to Cite
Palsberg, J. (1992). An Automatically Generated and Provably Correct Compiler for a Subset of Ada. DAIMI Report Series, 21(383). https://doi.org/10.7146/dpb.v21i383.6615
Issue
Section
Articles
License
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.