Open AccessAn Automatically Generated and Provably Correct Compiler for a Subset of Ada
Author(s) -
Jens Palsberg
Publication year - 1992
Publication title -
daimi pb
Language(s) - English
Resource type - Journals
eISSN - 2245-9316
pISSN - 0105-8517
DOI - 10.7146/dpb.v21i383.6615
Subject(s) - compiler , computer science , programming language , code generation , code (set theory) , semantics (computer science) , dead code elimination , compiler correctness , compiler construction , optimizing compiler , parallel computing , object code , operating system , key (lock) , set (abstract data type)
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.