 Timestamp:
 Jun 21, 2011, 12:27:02 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/CPP2011/cpp2011.tex
r1023 r1024 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$. 224 224 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. 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.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 with the system than that of Coq. 226 226 227 227 %  % … … 283 283 284 284 This 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 pseudoinstructions 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. 285 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. 286 That address is a function of the \emph{machine code} generated for the pseudoinstructions already expanded. 287 Thus, we must assemble each psedutoinstruction into machine code before moving on, and this must be eventually reflected in the proof of correctness. 288 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. 294 289 295 290 %  %
Note: See TracChangeset
for help on using the changeset viewer.