Changeset 1024 for src/ASM/CPP2011


Ignore:
Timestamp:
Jun 21, 2011, 12:27:02 PM (8 years ago)
Author:
mulligan
Message:

tidied explanation of proof

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CPP2011/cpp-2011.tex

    r1023 r1024  
    223223 For instance, to apply a coercion to force $\lambda x.M : A \to B$ to have type $\forall x:A.\Sigma y:B.P~x~y$, the system looks for a coercion from $M: B$ to $\Sigma y:B.P~x~y$ in a context augmented with $x:A$.
    224224This is significant when the coercion opens a proof obligation, as the user will be presented with multiple, but simpler proof obligations in the correct context.
    225 In this way, Matita supports the proof methodology developed by Sozeau in~\cite{sozeau:subset:2006}, with an implementation that is lighter and more tightly integrated than that of Coq.
     225In this way, Matita supports the proof methodology developed by Sozeau in~\cite{sozeau:subset:2006}, with an implementation that is lighter and more tightly integrated with the system than that of Coq.
    226226
    227227% ---------------------------------------------------------------------------- %
     
    283283
    284284This is a tempting approach to the proof, but ultimately the wrong approach.
    285 In particular, to expand a pseudo instruction we need to know the address
    286 at which the expanded instructions will be located, for instance to determine
    287 if a short jump is possible. That address is a function of the
    288 \emph{object code} generated for the pseudo-instructions already visited.
    289 Thus we need to assemble each pseduto instruction down to object code before
    290 moving to the next one and this must be eventually reflected on the proof
    291 of correctness. Therefore we will have lemmas for the \texttt{assembly1}
    292 function and for the composition of \texttt{expand\_pseudo\_instruction} and
    293 \texttt{assembly1}, but not for \texttt{expand\_pseudo\_instruction} alone.
     285In particular, to expand a pseudoinstruction we need to know the address at which the expanded instructions will be located, for instance to determine if a short jump is possible.
     286That address is a function of the \emph{machine code} generated for the pseudoinstructions already expanded.
     287Thus, we must assemble each psedutoinstruction into machine code before moving on, and this must be eventually reflected in the proof of correctness.
     288Therefore we will have lemmas proving correctness for the \texttt{assembly1} function, and for the composition of \texttt{expand\_pseudo\_instruction} and \texttt{assembly1}, but not for \texttt{expand\_pseudo\_instruction} alone.
    294289
    295290% ---------------------------------------------------------------------------- %
Note: See TracChangeset for help on using the changeset viewer.