Changeset 2069


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

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2012-asm/cpp-2012-asm.tex

    r2068 r2069  
    359359\subsection{Correctness of the assembler with respect to fetching}
    360360\label{subsect.total.correctness.of.the.assembler}
    361 
    362361Using our policies, we now work toward proving the total correctness of the assembler.
    363362By `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.
     363
     364The aim of this section is to prove the following informal statement:
     365when we fetch an assembly pseudoinstruction $I$ at address $ppc$, then
     366we can fetch the expanded pseudoinstruction(s) $[J^1;\ldots;J^n] = fetch\_pseudo\_instruction \ldots I~ppc$ from
     367$\sigma(ppc)$ in the code memory obtained loading the assembled object code.
     368
     369This constitutes the first major step in the proof of correctness of the
     370assembler, the next one being the simulation of $I$ by $[J^1;\ldots;J^n]$
     371(see Section~\ref{???}).
    364372
    365373We can express the following lemma, expressing the correctness of the assembly function (slightly simplified):
Note: See TracChangeset for help on using the changeset viewer.