We shall assume that there is a map giving for each variable in the expression a location in the main memory of the machine loc( , map) gives this location and we shall assume
as a relation between the state vector before the compiled program starts to act and the state vector of the source program.
Now we can write the compiler. It is
Here t is the number of a register such that all variables are stored in registers numbered less than t, so that registers t and above are available for temporary storage.
Before we can state our definition of correctness of the compiler, we need a notion of partial equality for state vectors
where and are state vectors and A is a set of variables means that corresponding components of and are equal except possibly for values, of variables in A. Symbolically, . Partial equality satisfies the following relations:
In our case we need a specialization of this notation and will use
and
and
The correctness of the compiler is stated in
THEOREM 1. If and are machine and source language state vectors respectively such that
It states that the result of running the compiled program is to put the value of the expression compiled into the accumulator. No registers except the accumulator and those with addresses are affected.