CORRECTNESS OF A COMPILER FOR

ARITHMETIC EXPRESSIONS∗

JOHN McCARTHY and JAMES PAINTER

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 Ex-
• pressions” 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: load

  sto

  li

  add

  sto

  load

  sto

  load

  sto

  li

  add

  add

  add

  x

  t

  t

  t

  x

  t + 1

  y

  t + 2

  t + 2

  t + 1

  t

• 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: associated functions

  predicate

  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 con-
• stant, 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)

  isvar(e) ⊃ Φ(e)

  issum(e) ⊃ Φ(s1(e)) ∧ Φ(s2(e)) ⊃ Φ(e).

  and

  and

• 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
• li α
• load x
• sto x
• add x predicate

  isli(s)

  isload(s)

  issto(s)

  isadd(s)

  analytic operation

  synthetic operation

  mkli(α)

  mkload(x)

  mksto(x)

  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) arg(s)

  adr(s)

  adr(s)

  adr(s)

• 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 fol-
• lowing. isli(mkli(α))

  α = arg(mkli(α))

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

  null(rest(mkli(α)))

  isli(s) ⊃ f irst(s) = s

  isload(mkload(x))

  x = adr(mkload(x))

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

  null(rest(mkload(x)))

  isload(s) ⊃ f irst(s) = s

  issto(mksto(x))

  x = adr(mksto(x))

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

  null(rest(mksto(x)))

  issto(s) ⊃ f irst(s) = s

  isadd(mkadd(x))

  x = adr(mkadd(x))

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

  null(rest(mkadd(x)))

  isadd(x) ⊃ f irst(s) = s

  (3.1)

  (3.2)

  (3.3)

  (3.4)

  (3.5)

  (3.6)

  (3.7)

  ¬ null(p) ⊃ p = f irst(p) ∗ rest(p),

  ¬null(p1) ∧ null(rest(p1)) ⊃ p1 = f irst(p1 ∗ p2)

  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 vec-
• tor η 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), η)

  (3.11)

  else if isload(s) then a(ac, c(adr(s), η), η)

  else if issto(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 cor-
• responding 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

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

• and
• 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
• outcome(compile(e, t), η) = outcome(mkli(val(e)), η) = step(mkli(val(e)), η)

  = a(ac, arg(mkli(val(e))), η)

  = a(ac, val(e), η)

  = a(ac, value(e, ξ), η)

  =t a(ac, value(e, ξ), η).

  Justification

  4.2

  3.12, 3.1

  3.1, 3.11

  3.1

  2.1

  4.3, 4.4

• II. isvar(e). We have
• outcome(compile(e, t), η) = outcome(mkload(loc(e, map)), η)

  = a(ac, c(adr(mkload(loc(e))), η), η)

  = a(ac, c(loc(e, map), η, η)

  = a(ac, c(e, ξ), η)

  = a(ac, value(e, ξ), η)

  =t a(ac, value(e, ξ), η).

  4.2

  3.12, 3.2, 3.113.2

  4.1

  2.1

  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 func-
• tions 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
• Now
• and
• Next c(ac, ζ1) = ν1.

  3.8

  ζ2 = outcome(mksto(t), ζ1)

  = a(t, c(ac, ζ1), ζ1)

  = a(t, ν1), ζ1)

  =t+1 a(t, ν1, a(ac, ν1, η))

  =t+1,ac a(t, ν1, η)

  3.12, 3.3, 3.11

  Substitution

  4.5

  4.5, 3.9

  c(t, ζ2) = ν1

  3.8

  ζ3 = outcome(compile(s2(e), t + 1), ζ2)

  = t+1a(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.

  ζ3 =t+1 a(ac, ν2, a(t, ν1, η))

  by 3.9

• Now we can continue with
• Finally, ζ4 = outcome(mkadd (t), ζ3)

  = a(ac, c(t, ζ3) + c(ac, ζ3), ζ3)

  = a(ac, ν, ζ3)

  =t+1 a(ac, ν, a(ac, ν2, a(t, ν1, η)))

  =t+1 a(ac, ν, a(t, ν1, η))

  =t a(ac, ν, η).

• This concludes the proof. Definition of ν, substitution

  3.12, 3.4, 3.114.53.93.9, 4.6, 4.7- 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
• to Equation (2.1).
• 3. Add if isprod(e) then value(p1(e), ζ)× value(p2(e), ζ)

  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 Com-
• puter programming and formal systems, edited by P. Braffort and D. Hersh-
• berg, 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.