Correctness Preserving Transformations on a Multipass Occam Compiler

Abstract

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.