# Changeset 2069

Ignore:
Timestamp:
Jun 13, 2012, 7:58:55 PM (6 years ago)
Message:

...

File:
1 edited

### Legend:

Unmodified
 r2068 \subsection{Correctness of the assembler with respect to fetching} \label{subsect.total.correctness.of.the.assembler} Using our policies, we now work toward proving the total correctness of the assembler. By `total correctness', we mean that the assembly process never fails when provided with a correct policy and that the process does not change the semantics of a certain class of well behaved assembly programs. The aim of this section is to prove the following informal statement: when we fetch an assembly pseudoinstruction $I$ at address $ppc$, then we can fetch the expanded pseudoinstruction(s) $[J^1;\ldots;J^n] = fetch\_pseudo\_instruction \ldots I~ppc$ from $\sigma(ppc)$ in the code memory obtained loading the assembled object code. This constitutes the first major step in the proof of correctness of the assembler, the next one being the simulation of $I$ by $[J^1;\ldots;J^n]$ (see Section~\ref{???}). We can express the following lemma, expressing the correctness of the assembly function (slightly simplified):