# Changeset 1022 for src/ASM/CPP2011/cpp-2011.tex

Ignore:
Timestamp:
Jun 21, 2011, 12:18:28 PM (9 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r1021 %By composition, we then have that the whole assembly process is semantics preserving. %This is a tempting approach to the proof, but ultimately the wrong approach. %In particular, it is important that we track how the program counter indexing into the assembly program, and the machine's program counter evolve, so that we can relate them. %Expanding pseudoinstructions requires that the machine's program counter be incremented by $n$ steps, for $1 \leq n$, for every increment of the assembly program's program counter. %Keeping track of the correspondence between the two program counters quickly becomes unfeasible using a compositional approach, and hence the proof must be monolithic. This is a tempting approach to the proof, but ultimately the wrong approach. In particular, to expand a pseudo instruction we need to know the address at which the expanded instructions will be located, for instance to determine if a short jump is possible. That address is a function of the \emph{object code} generated for the pseudo-instructions already visited. Thus we need to assemble each pseduto instruction down to object code before moving to the next one and this must be eventually reflected on the proof of correctness. Therefore we will have lemmas for the \texttt{assembly1} function and for the composition of \texttt{expand\_pseudo\_instruction} and \texttt{assembly1}, but not for \texttt{expand\_pseudo\_instruction} alone. % ---------------------------------------------------------------------------- %