Modelling Program Compilation in the Refinement Calculus

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.

Content

Author and article information

Contributors

C. J. Fidge

Conference

Publication date: July 1997

Publication date (Print): July 1997

Pages: 1-10

Affiliations

[0001]Software Verification Research Centre

School of Information Technology

The University of Queensland

Queensland 4072, Australia

Article

DOI: 10.14236/ewic/FA1997.8

SO-VID: 937f7f5d-fefb-43fe-9070-3e7c98542edf

Copyright statement: © C. J. Fidge. Published by BCS Learning and Development Ltd. Proceedings of the 2nd BCS-FACS Northern Formal Methods Workshop, Ilkley

License:

This work is licensed under a Creative Commons Attribution 4.0 Unported License. To view a copy of this license, visit http://creativecommons.org/licenses/by/4.0/

Conference name: Proceedings of the 2nd BCS-FACS Northern Formal Methods

Conference acronym: FM

Conference number: 2

Conference location: Ilkley

Conference date: 14-15 July 1997

Conference sponsor: Electronic Workshops in Computing (eWiC)

Conference theme: Northern Formal Methods

Product

Product Information: 1477-9358BCS Learning & Development

Self URI (article page): https://www.scienceopen.com/hosted-document?doi=10.14236/ewic/FA1997.8

Self URI (journal page): https://ewic.bcs.org/

Modelling Program Compilation in the Refinement Calculus

Abstract