Open AccessModelling Program Compilation in the Refinement Calculus
Author(s) -
Colin Fidge
Publication year - 1997
Publication title -
electronic workshops in computing
Language(s) - English
Resource type - Conference proceedings
ISSN - 1477-9358
DOI - 10.14236/ewic/fa1997.8
Subject(s) - programming language , computer science , refinement calculus , code (set theory) , set (abstract data type) , code generation , assembly language , theoretical computer science , calculus (dental) , algorithm , software , key (lock) , medicine , computer security , dentistry
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.
Accelerating Research
Robert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom
Address
John Eccles HouseRobert Robinson Avenue,
Oxford Science Park, Oxford
OX4 4GP, United Kingdom