Did you know ... Search Documentation:
Pack logicmoo_nars -- ImportantDocs/jmc/mcpain.md

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.