Changeset 1024 for src/ASM/CPP2011

Timestamp:

Jun 21, 2011, 12:27:02 PM (10 years ago)

Author:

mulligan

Message:

tidied explanation of proof

File:

• src/ASM/CPP2011/cpp-2011.tex (modified) (2 diffs)

src/ASM/CPP2011/cpp-2011.tex

@@ -223 +223 @@
  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$.
 This 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.
-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.
+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 with the system than that of Coq.
 
 % ---------------------------------------------------------------------------- %
@@ -283 +283 @@
 
 This is a tempting approach to the proof, but ultimately the wrong approach.
-In particular, to expand a pseudo instruction we need to know the address
-at which the expanded instructions will be located, for instance to determine
-if a short jump is possible. That address is a function of the
-\emph{object code} generated for the pseudo-instructions already visited.
-Thus we need to assemble each pseduto instruction down to object code before
-moving to the next one and this must be eventually reflected on the proof
-of correctness. Therefore we will have lemmas 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.
+In 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.
+That address is a function of the \emph{machine code} generated for the pseudoinstructions already expanded.
+Thus, we must assemble each psedutoinstruction into machine code before moving on, and this must be eventually reflected in the proof of correctness.
+Therefore 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.
 
 % ---------------------------------------------------------------------------- %