next up previous
Next: Proof of Theorem 1. Up: CORRECTNESS OF A COMPILER Previous: The object language.

The compiler

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( tex2html_wrap_inline405 , map) gives this location and we shall assume

displaymath409

as a relation between the state vector tex2html_wrap_inline381 before the compiled program starts to act and the state vector tex2html_wrap_inline347 of the source program.

Now we can write the compiler. It is

displaymath112

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

displaymath419

where tex2html_wrap_inline421 and tex2html_wrap_inline423 are state vectors and A is a set of variables means that corresponding components of tex2html_wrap_inline421 and tex2html_wrap_inline423 are equal except possibly for values, of variables in A. Symbolically, tex2html_wrap_inline429 . Partial equality satisfies the following relations:

displaymath431

displaymath433

displaymath435

displaymath437

displaymath439

In our case we need a specialization of this notation and will use

displaymath441

and

displaymath443

and

displaymath445

The correctness of the compiler is stated in

THEOREM 1. If tex2html_wrap_inline381 and tex2html_wrap_inline347 are machine and source language state vectors respectively such that

displaymath155

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 tex2html_wrap_inline451 are affected.



John McCarthy
Wed Sep 29 13:40:01 PDT 1999