Proceedings of the 2nd BCS-FACS Northern Formal Methods (FM)
Northern Formal Methods
14-15 July 1997
We show how compilation of high-level language programs to assembler code can be formally represented in the refinement calculus. New operators are introduced to widen the modelling language to encompass assembler code. A compilation strategy is then embodied as a set of derived refinement rules.