Changeset 2069 for src

Timestamp:

Jun 13, 2012, 7:58:55 PM (9 years ago)

Author:

sacerdot

Message:

...

File:

• src/ASM/CPP2012-asm/cpp-2012-asm.tex (modified) (1 diff)

src/ASM/CPP2012-asm/cpp-2012-asm.tex

@@ -359 +359 @@
 \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):