Changeset 2351 for Papers/cpp-asm-2012


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

Small consistency changes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Papers/cpp-asm-2012/cpp-2012-asm.tex

    r2350 r2351  
    386386By `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.
    387387
    388 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.
     388The 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.
    389389This 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}).
    390390
     
    471471 $\forall$ppc. ppc < $\mid$snd program$\mid$ $\rightarrow$
    472472  let $\langle$labels, costs$\rangle$ := create_label_cost_map program in
    473   let $\langle$assembled, costs'$\rangle$ := $\pi_1$ (assembly program sigma policy) in
     473  let $\langle$assembled, costs'$\rangle$ := $\pi_1$ (assembly program policy) in
    474474  let cmem := load_code_memory assembled in
    475475  let $\langle$pi, newppc$\rangle$ := fetch_pseudo_instruction program ppc in
     
    554554definition status_of_pseudo_status:
    555555 internal_pseudo_address_map $\rightarrow$ $\forall$pap. $\forall$ps: PseudoStatus pap.
    556  $\forall$policy. Status (code_memory_of_pseudo_assembly_program pap sigma policy)
     556 $\forall$policy. Status (code_memory_of_pseudo_assembly_program pap policy)
    557557\end{lstlisting}
    558558
Note: See TracChangeset for help on using the changeset viewer.