We present a proof of correctness in Matita for an optimising assembler for the MCS-51 microcontroller. The efficient expansion of pseudoinstructions, namely jumps, into machine instructions is complex. We isolate the decision making over how jumps should be expanded from the expansion process itself as much as possible using 'policies', making the proof of correctness for the assembler more straightforward. Our proof strategy contains a tracking facility for 'good addresses' and only programs that use good addresses have their semantics preserved under assembly, as we observe that it is impossible for an assembler to preserve the semantics of every assembly program. Our strategy offers increased flexibility over the traditional approach to proving the correctness of assemblers, wherein addresses in assembly are kept opaque and immutable. In particular, we may experiment with allowing the benign manipulation of addresses. © 2012 Springer-Verlag Berlin Heidelberg.
CITATION STYLE
Mulligan, D. P., & Sacerdoti Coen, C. (2012). On the correctness of an optimising assembler for the Intel MCS-51 microprocessor. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7679 LNCS, pp. 43–59). https://doi.org/10.1007/978-3-642-35308-6_7
Mendeley helps you to discover research relevant for your work.