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.

Wed Sep 29 13:40:01 PDT 1999