This paper contains a proof of the correctness of a simple compiling algorithm for compiling arithmetic expressions into machine language.
The definition of correctness, the formalism used to express the description of source language, object language and compiler, and the methods of proof are all intended to serve as prototypes for the more complicated task of proving the correctness of usable compilers. The ultimate goal, as outlined in references [1], [2], [3] and [4] is to make it possible to use a computer to check proofs that compilers are correct.
The concepts of abstract syntax, state vector, the use of an interpreter for defining the semantics of a programming language, and the definition of correctness of a compiler are all the same as in [3]. The present paper, however, is the first in which the correctness of a compiler is proved.
The expressions dealt with in this paper are formed from constants and variables. The only operation allowed is a binary + although no change in method would be required to include any other binary operations. An example of an expression that can be compiled is
although, because we use abstract syntax, no commitment to a particular notation is made.
The computer language into which these expressions are compiled is a single address computer with an accumulator, called ac, and four instructions: li (load immediate), load, sto (store) and add. Note that there are no jump instructions. Needless to say, this is a severe restriction on the generality of our results which we shall overcome in future work.
The compiler produces code that computes the value of the expression being compiled and leaves this value in the accumulator. The above expression is compiled into code which in assembly language might look as follows:
Again because we are using abstract syntax there is no commitment to a precise form for the object code.