CORRECTNESS OF A COMPILER FOR ARITHMETIC EXPRESSIONS^{∗}

JOHN McCARTHY and JAMES PAINTER

1967

1 Introduction

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

(x + 3) + (x + (y + 2))

∗This is a reprint with minor changes of ”Correctness of a Compiler for Arithmetic Expressions” by John McCarthy and James Painter which was published in MATHEMATICAL ASPECTS OF COMPUTER SCIENCE 1, which was Volume 19 of Proceedings of Symposia in Applied Mathematics and published by the American Mathematical Society in 1967

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:

\begin{matrix}load & x \\ sto & t \\ li & 3 \\ add & t \\ sto & t \\ load & x \\ sto & t + 1 \\ load & y \\ sto & t + 2 \\ li & 2 \\ add & t + 2 \\ add & t + 1 \\ add & t \end{matrix}

Again because we are using abstract syntax there is no commitment to a precise form for the object code.

2 The source language

The abstract analytic syntax of the source expressions is given by the table:

predicate  associated functions

isconst(e) isvar(e)

issum(e)  s1(e) s2(e)

which asserts that the expressions comprise constants, variables and binary sums, that the predicates isconst, isvar, and issum enable one to classify each expression and that each sum e has summands s1(e) and s2(e).

The semantics is given by the formula

(2.1)  value(e, ξ) = if isconst(e) then val(e) else if isvar(e) then c(e, ξ)

else if issum(e) then value(s1(e), ξ) + value(s2(e), ξ)

where val(e) gives the numerical value of an expression e representing a constant, c(e, ξ) gives the value of the variable e in the state vector ξ and + is some binary operation. (It is natural to regard + as an operation that resembles addition of real numbers, but our results do not depend on this).

For our present purposes we do not have to give a synthetic syntax for the source language expressions since both the interpreter and the compiler use only the analytic syntax. However, we shall need the following induction principle for expressions:

Suppose Φ is a predicate applicable to expressions, and suppose that for all expressions e we have

isconst(e) ⊃ Φ(e) and isvar(e) ⊃ Φ(e) and issum(e) ⊃ Φ(s1(e)) ∧ Φ(s2(e)) ⊃ Φ(e).

Then we may conclude that Φ(e) is true for all expressions e.

3 The object language.

We must give both the analytic and synthetic syntaxes for the object language because the interpreter defining its semantics uses the analytic syntax and the compiler uses the synthetic syntax. We may write the analytic and synthetic syntaxes for instructions in the following table.

operation  predicate  analytic operation  synthetic operation
li α  isli(s)  arg(s)  mkli(α)
load x  isload(s)  adr(s)  mkload(x)
sto x  issto(s)  adr(s)  mksto(x)
add x  isadd(s)  adr(s)  mkadd(x)

A program is a list of instructions and null(p) asserts that p is the null list. If the program p is not null then first(p) gives the first instruction and rest(p) gives the list of remaining instructions. We shall use the operation p1 ∗ p2 to denote the program obtained by appending p2 onto the end of p1. Since we have only one level of list we can identify a single instruction with a program that has just one instruction.

The synthetic and analytic syntaxes of instructions are related by the following.

isli(mkli(α)) α = arg(mkli(α))

(3.1) isli(s) ⊃ s = mkli(arg(s))

null(rest(mkli(α))) isli(s) ⊃ first(s) = s

isload(mkload(x)) x = adr(mkload(x))

(3.2) isload(x) ⊃ x = mkload(adr(x))

null(rest(mkload(x))) isload(s) ⊃ first(s) = s

issto(mksto(x)) x = adr(mksto(x))

(3.3) issto(x) ⊃ x = mksto(adr(x))

null(rest(mksto(x))) issto(s) ⊃ first(s) = s

isadd(mkadd(x)) x = adr(mkadd(x))

(3.4) isadd(x) ⊃ x = mkadd(adr(x))

null(rest(mkadd(x))) isadd(x) ⊃ first(s) = s

(3.5) ¬ null(p) ⊃ p = first(p) ∗ rest(p),
(3.6) ¬null(p1) ∧ null(rest(p1)) ⊃ p1 = first(p1 ∗ p2)
(3.7) null(p1 ∗ p2) ≡ null(p1) ∧ null(p2).

The ∗ operation is associative. (The somewhat awkward form of these relations comes from having a general concatenation operation rather than just an operation that prefixes a single instruction onto a program.)

A state vector for a machine gives, for each register in the machine, its contents. We include the accumulator denoted by ac as a register. There are two functions of state vectors as introduced in [3], namely

1. c(x, η) denotes the value of the contents of register x in machine state η.

2. a(x, α, η) denotes the state vector that is obtained from the state vector η by changing the contents of register x to α leaving the other registers unaffected.

These functions satisfy the following relations:

(3.8)  c(x, a(y, α, η)) = if x = y then α else c(x, η),
(3.9) a(x, α, a(y, β, η)) = if x = y then a(x, α, η) else a(y, β, a(x, α, η)),
(3.10)  a(x, c(x, η), η) = η.

Now we can define the semantics of the object language by

step(s, η) = if isli(s)then a(ac, arg(s), η)
else ifisload(s) then a(ac, c(adr(s), η), η)
(3.11)  else ifissto(s) thena(adr(s), c(ac, η), η)
elseif isadd(s) then a(ac, c(adr(s), η) + c(ac, η), η)

which gives the state vector that results from executing an instruction and (3.12) outcome(p, η) = if null(p) then η else outcome(rest(p), step(first(p), η))

which gives the state vector that results from executing the program p with state vector η.

The following lemma is easily proved.

(3.13)  outcome(p1 ∗ p2, η) = outcome(p2, outcome(p1, η))

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

(4.1)  c(loc(ν, map), η) = c(ν, ξ)

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

compile(e, t) = if isconst(e) then mkli(val(e))

(4.2)  else if isvar(e) then mkload(loc(e,map))

else if issum(e) then compile(s1(e), t) ∗ mksto(t) ∗ compile(s2, t + 1) ∗ mkadd(t)

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

ζ_{1} =_{A} ζ_{2},

where ζ_{1} and ζ_{2} are state vectors and A is a set of variables means that corresponding components of ζ_{1} and ζ_{2} are equal except possibly for values, of variables in A. Symbolically, x ∉ A ⊃ c(x, ζ_{1}) = c(x, ζ_{2}). Partial equality satisfies the following relations:

(4.3) ζ_{1} = ζ_{2} is equivalent to ζ_{1} =_{{}} ζ_{2}, where {} denotes the empty set ,

(4.4)  if A ⊂ B and ζ_{1} =_{A} ζ_{2} then ζ_{1} =_{B} ζ_{2}.

(4.5)  if ζ_{1} =_{A} ζ_{2} then a(x, α, ζ_{1}) =_{A−{x}} a(x, α, ζ_{2}).

(4.6)  if x ∈ A then a(x, α, ζ) =_{A} ζ,

(4.7)  if ζ_{1} =_{A} ζ_{2} and ζ_{2} =_{B} ζ_{3} then ζ_{1} =_{A∪B} ζ_{3}.

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

ζ_{1} =_{t} ζ_{2} to denote ζ_{1} =_{{x|x≥t}} ζ_{2}

and

ζ_{1} =_{ac} ζ_{2} to denote ζ_{1} =_{{ac}} ζ_{2}

and

ζ_{1} =_{t,ac} ζ_{2} to denote ζ_{1} =_{{x|x=ac∨x≥t}} ζ_{2}.

The correctness of the compiler is stated in

THEOREM 1. If η and ξ are machine and source language state vectors respectively such that

(4.8) c(loc(v, η) = c(v, ξ), then
outcome(compile(e, t), η) =_{t} a(ac,value(e, ξ), η).

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 ≥ t are affected.

5 Proof of Theorem 1.

The proof is accomplished by an induction on the expression e being compiled. We prove it first for constants, then for variables, and then for sums on the induction hypothesis that it is true for the summands. Thus there are three cases.

I. isconst(e). We have

Justification

outcome(compile(e, t), η) = outcome(mkli(val(e)), η)  4.2
= step(mkli(val(e)), η)  3.12, 3.1
= a(ac, arg(mkli(val(e))), η)  3.1, 3.11
= a(ac, val(e), η)  3.1
= a(ac, value(e, ξ), η)  2.1
=_{t} a(ac, value(e, ξ), η).  4.3, 4.4

II. isvar(e). We have outcome(compile(e, t), η)

= outcome(mkload(loc(e, map)), η)  4.2
= a(ac, c(adr(mkload(loc(e))), η), η)  3.12, 3.2, 3.11
= a(ac, c(loc(e, map), η, η)  3.2
= a(ac, c(e, ξ), η)  4.1
= a(ac, value(e, ξ), η)  2.1
=_{t} a(ac, value(e, ξ), η).  4.3, 4.4

III. issum(e). In this case, we first write

outcome(compile(e, t), η)

= outcome(compile(s1(e), t) ∗ mksto(t) ∗compile(s2(e), t + 1) ∗ mkadd(t), η) by 4.2

= outcome(mkadd(t), outcome(compile(s2(e), t + 1),

outcome(mksto(t), outcome(compile(s1(e), t), η)))) by 3.13 using the relation between concatenating programs and composing the functions they represent. Now we introduce some notation. Let

ν = value(e, ξ),
ν_{1} = value(s1(e), ξ),
ν_{2} = value(s2(e), ξ),

so that ν = ν_{1} + ν_{2}. Further let

ζ_{1} = outcome(compile(s1(e), t), η),
ζ_{2} = outcome(mksto(t), ζ_{1}),
ζ_{3} = outcome(compile(s2(e), t + 1), ζ_{2}),
ζ_{4} = outcome(mkadd(t), ζ_{3})

so that ζ_{4} = outcome(compile(e, t), η, and we want to prove that ζ_{4} =_{t} a(ac, ν, η).

We have

ζ_{1} = outcome(compile(s1(e), t), η)
=_{t} a(ac, ν_{1}, η)  Induction Hypothesis

and

c(ac, ζ_{1}) = ν_{1}. 3.8

Now

ζ_{2} = outcome(mksto(t), ζ_{1})
= a(t, c(ac, ζ_{1}), ζ_{1})  3.12, 3.3, 3.11
= a(t, ν_{1}), ζ_{1})  Substitution
=_{t+1} a(t, ν_{1}, a(ac, ν_{1}, η))  4.5
=_{t+1,ac} a(t, ν_{1}, η)  4.5, 3.9

and

c(t, ζ_{2}) = ν_{1}  3.8

Next

ζ_{3} = outcome(compile(s2(e), t + 1), ζ_{2})
= _{t+1}a(ac, ν_{2}, ζ_{2}).

Here we again use the induction hypothesis that s2(e) is compiled correctly. In order to apply it, we need c(loc(ν,map),ζ_{2}) = c(ν, ξ) for each variable ν which is proved as follows:

c(loc(ν, map), ζ_{2}) = c(loc(ν), map)a(t, ν_{1}, η)) since loc(ν, map) < t

= c(loc(ν, map), η) for the same reason = c(ν, ξ) by the hypothesis of the theorem.

Now we can continue with

ζ_{3} =_{t+1} a(ac, ν_{2}, a(t, ν_{1}, η)) by 3.9

Finally,

ζ_{4} = outcome(mkadd (t), ζ_{3})
= a(ac, c(t, ζ_{3}) + c(ac, ζ_{3}), ζ_{3})  3.12, 3.4, 3.11
= a(ac, ν, ζ_{3})  Definition of ν, substitution
=_{t+1} a(ac, ν, a(ac, ν_{2}, a(t, ν_{1}, η)))  4.5
=_{t+1} a(ac, ν, a(t, ν_{1}, η))  3.9
=_{t} a(ac, ν, η).  3.9, 4.6, 4.7

This concludes the proof.

6 Remarks

The problem of the relations between source language and object language arithmetic is dealt with here by assuming that the + signs in formulas (2.1) and (3.11) which define the semantics of the source and object languages represent the same operation. Theorem 1 does not depend on any properties of this operation, not even commutativity or associativity.

The proof is entirely straightforward once the necessary machinery has been created. Additional operations such as subtraction, multiplication and division could be added without essential change in the proof.

For example, to put multiplication into the system the following changes would be required. 1. Add isprod(e), and p1(e), and p2(e) to the abstract

syntax of the source language.

2. Add a term

if isprod(e) then value(p1(e), ζ)× value(p2(e), ζ)

to Equation (2.1).

3. Add

isprod(e) ∧ Φ(p1(e)) ∧ Φ(p2(e)) ⊃ Φ(e)

to the hypotheses of the source language induction principle.

4. Add an instruction mul x and the three syntactical functions ismul(s) adr(r), mkmul(x) to the abstract syntax of the object language together with the necessary relations among them.

5. Add to the definition (3.11) of step a term

else if ismul(s) then a(ac, c(adr(s), η) × x(ac, η), η).

6. Add to the compiler a term

if isprod(e)thencompile(p1(e), t) ∗ mksto(t) ∗ compile(p2(e), t + 1) ∗ mkmul(t).

7. Add to the proof a case isprod(e) which parallels the case issum(e) exactly.

The following other extensions are contemplated. 1. Variable length sums.

2. Sequences of assignment statements.

3. Conditional expressions.

4. go to statements in the source language.

In order to make these extensions, a complete revision of the formalism will be required.

7 References

1. J. McCarthy, Computer programs for checking mathematical proofs, Proc. Sympos. Pure Math. Vol. 5, Amer. Math. Soc., Providence, R. I., 1962, pp. 219-227.

2. ———–, ”A basis for a mathematical theory of computation” in Computer programming and formal systems, edited by P. Braffort and D. Hershberg, North-Holland, Amsterdam, 1963.

3. ———–, Towards a mathematical theory of computation, Proc. Internat. Congr. on Information Processing, 1962.

4. ———–, A formal description of a subset of Algol, Proc. Conf. on Formal Language Description Languages, Vienna, 1964.