A compiler for arithmetic expressions #
A formalization of the correctness of a compiler from arithmetic expressions to machine language described by McCarthy and Painter, which is considered the first proof of compiler correctness.
Main definitions #
Expr: the syntax of the source language.
value: the semantics of the source language.
Instruction: the syntax of the target language.
step: the semantics of the target language.
compile: the compiler.
Main results #
compiler_correctness: the compiler correctness theorem.
≃[t]/ac: partial equality of two machine states excluding registers x ≥ t and the accumulator.
≃[t]: partial equality of two machine states excluding registers x ≥ t.
- John McCarthy and James Painter. Correctness of a compiler for arithmetic expressions. In Mathematical Aspects of Computer Science, volume 19 of Proceedings of Symposia in Applied Mathematics. American Mathematical Society, 1967. http://jmc.stanford.edu/articles/mcpain/mcpain.pdf
Source language #
The semantics of the source language (2.1).
Target language #
- ac : Arithcc.Word
Machine state consists of the accumulator and a vector of registers.
The implementation of the compiler (4.2).
This definition explicitly takes a map from variables to registers.
- Arithcc.compile map (Arithcc.Expr.const v) x = [Arithcc.Instruction.li v]
- Arithcc.compile map (Arithcc.Expr.var x_2) x = [Arithcc.Instruction.load (Arithcc.loc x_2 map)]
- Arithcc.compile map (Arithcc.Expr.sum s₁ s₂) x = Arithcc.compile map s₁ x ++ [Arithcc.Instruction.sto x] ++ Arithcc.compile map s₂ (x + 1) ++ [Arithcc.Instruction.add x]
The main compiler correctness theorem.
Unlike Theorem 1 in the paper, both
map and the assumption on
t are explicit.