Program Transformations in a Denotational Setting

Abstract

Program transformations are frequently performed by optimizing compilers and the correctness of applying them usually depends on data flow information. For source-to-source transformations it is shown how a denotational setting can be useful for validating such program transformations.

Strong equivalence is obtained for transformations that exploit forward data flow information, whereas weak equivalence is obtained for transformations that exploit backward data flow information. To obtain strong equivalence both the original and the transformed program must be data flow analysed, but consideration of a transformation exploiting liveness of variables indicates that a more satisfactory approach may be possible.