A proof of the correctness of a simple compiling algorithm for compiling arithmetic expressions into machine language.
Ultimate goal, is to make it possible to use a computer to check proofs that compilers are correct.
Conceptions inherited from [c3]:
Example expression:
$(x+3) + (x+(y+2))$
Assembly example:
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
# Abstract syntax will be used, so there is no commitment to a precise form for the object code.Abstract analytic syntax of the source expressions:
| predicate | associated functions |
|---|---|
| isconst(e) | |
| isvar(e) | |
| issum(e) | s1(e) s2(e) |
==> Expressions comprise constants, variables and binary sums; Each sum $e$ has summands $s1(e)$ and $s2(e).
Semantics:
(2.1) value$(e,\xi)$ = if isconst(e) then val(e) else if isvar(e) then $c(e,\xi)$ else if issum(e) then value$(s1(e),\xi)$ + value$(s2(e),\xi)$.
==> val(e) gives the numerical value of an expression e representing a constant; $c(e,\xi)$ gives the value of the variable e in the state vector $\xi$ and $+$ is some binary operation.
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 $\Phi$ is a predicate applicable to expressions, and suppose that for all expressions $e$ we have:
isconst(e) $\supset \Phi$(e) and
isvar(e) $\supset \Phi$(e) and
issum(e) $\supset \Phi(s1(e)) \wedge \Phi(s2(e)) \supset \Phi(e)$.
==> Then we may conclude that $\Phi(e)$ is true for all expressions $e$.
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.
Analytic and synthetic syntaxes for instructions:
| operation | predicate | analytic operation | synthetic operation |
|---|---|---|---|
| li $\alpha$ | isli(s) | arg(s) | mkli($\alpha$) |
| load x | isload(x) | adr(s) | mkload(x) |
| sto x | issto (s) | adr (s) | mksto (x) |
| add x | isadd(s) | addr(s) | mkadd(x) |
References:
References: J. McCarthy, Towards a mathematical theory(science) of computation. 1962. More
If you could revise
the fundmental principles of
computer system design
to improve security...
... what would you change?