# Changeset 2351 for Papers/cpp-asm-2012

Ignore:
Timestamp:
Sep 26, 2012, 5:55:28 PM (8 years ago)
Message:

Small consistency changes.

File:
1 edited

### Legend:

Unmodified
 r2350 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 \texttt{I} at address \texttt{ppc}, then we can fetch the expanded pseudoinstruction(s) \texttt{[J1, \ldots, Jn] = fetch\_pseudo\_instruction \ldots\ I\ ppc} from \texttt{sigma(ppc)} in the code memory obtained by loading the assembled object code. The aim of this section is to prove the following informal statement: when we fetch an assembly pseudoinstruction \texttt{I} at address \texttt{ppc}, then we can fetch the expanded pseudoinstruction(s) \texttt{[J1, \ldots, Jn] = fetch\_pseudo\_instruction \ldots\ I\ ppc} from \texttt{policy ppc} in the code memory obtained by 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 \texttt{I} by \texttt{[J1, \ldots, Jn]} (see Subsection~\ref{subsect.total.correctness.for.well.behaved.assembly.programs}). $\forall$ppc. ppc < $\mid$snd program$\mid$ $\rightarrow$ let $\langle$labels, costs$\rangle$ := create_label_cost_map program in let $\langle$assembled, costs'$\rangle$ := $\pi_1$ (assembly program sigma policy) in let $\langle$assembled, costs'$\rangle$ := $\pi_1$ (assembly program policy) in let cmem := load_code_memory assembled in let $\langle$pi, newppc$\rangle$ := fetch_pseudo_instruction program ppc in definition status_of_pseudo_status: internal_pseudo_address_map $\rightarrow$ $\forall$pap. $\forall$ps: PseudoStatus pap. $\forall$policy. Status (code_memory_of_pseudo_assembly_program pap sigma policy) $\forall$policy. Status (code_memory_of_pseudo_assembly_program pap policy) \end{lstlisting}