Correctness Preserving Transformations on a Multipass Occam Compiler
DOI:
https://doi.org/10.7146/dpb.v20i368.6600Abstract
The verification of a compiler may be a substantial task. However, by introducing correctness preserving program transformations some automated assistance becomes available. The idea is to specify an initial multipass compiler, to verify it in the usual way and then, while preserving the overall correctness result, to transform it into a more efficient single pass compiler. This transformation process may be performed using the fold/unfold framework of Burstall and Darlington and automation is provided by the Flagship Programming Environment. We illustrate this transformation process on a compiler for a subset of Occam.Downloads
Published
1991-10-01
How to Cite
Glindtvad, K., & Nielson, H. R. (1991). Correctness Preserving Transformations on a Multipass Occam Compiler. DAIMI Report Series, 20(368). https://doi.org/10.7146/dpb.v20i368.6600
Issue
Section
Articles
License
Articles published in DAIMI PB are licensed under a Creative Commons Attribution-NonCommercial-NoDerivs 3.0 Unported License.