Title :
An automatically generated and provably correct compiler for a subset of Ada
Author_Institution :
Dept. of Comput. Sci., Aarhus Univ., Denmark
Abstract :
The automatic generation of a provably correct compiler for a nontrivial subset of Ada is described. The compiler is generated from an action semantic description; it emits absolute code for an abstract RISC (reduced instruction set computer) 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 P.D. Mosses, L. Paulson, and M. Wand. The use of action semantics makes the processable language specification easy to read and pleasant to work with
Keywords :
Ada; automatic programming; machine oriented languages; program compilers; reduced instruction set computing; HP Precision Architecture; SPARC; absolute code; abstract RISC; action semantic description; automatic generation; machine language; nontrivial subset; processable language specification; provably correct compiler; reduced instruction set computer; Assembly; Computer languages; Computer science; Error correction; Marine vehicles; Process design; Program processors; Programming profession; Reduced instruction set computing; Specification languages;
Conference_Titel :
Computer Languages, 1992., Proceedings of the 1992 International Conference on
Conference_Location :
Oakland, CA
Print_ISBN :
0-8186-2585-6
DOI :
10.1109/ICCL.1992.185474
