Refinement algebra proves correctness of compilation

Abstract

A compiler is specified by a description of how each construct of the source language is translated into a sequence of object code instructions. The meaning of the object code can be defined by an interpreter written in the source language itself. A proof that the compiler is correct must show that interpretation of the object code is at least as good (for any relevant purpose) as the corresponding source program. The proof is conducted using standard techniques of data refinement. All the-calculations are based on algebraic laws governing the source language. The theorems are expressed in a form close to a logic program, which may be used as a compiler prototype, or as a check on the results of a particular compilation. It is suggested that this formal framework provides appropriate interfaces for compiler implementors, and hardware designers, as well as users of the language.