Changeset 1435 for Deliverables/D4.2-4.3
- Timestamp:
- Oct 21, 2011, 5:24:08 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
Deliverables/D4.2-4.3/reports/D4-2.tex
r1434 r1435 330 330 \label{subsect.use.of.dependent.types} 331 331 332 We see twopotential ways in which a compiler can fail to compile a program:332 We see several potential ways in which a compiler can fail to compile a program: 333 333 \begin{enumerate} 334 334 \item 335 335 The program is malformed, and there is no hope of making sense of the program. 336 336 \item 337 The compiler is buggy, or an invariant in the compiler is invalidated, for example, if the program is too large to fit into the processor's code memory. 337 The compiler is buggy, or an invariant in the compiler is invalidated. 338 \item Some non complete heuristics in the compiler fails. 339 \item The compiled code exhausts some bounded resource, tipically the 340 processor's code memory. 338 341 \end{enumerate} 342 Standard compilers can fail for all the above reasons. Certified compilers 343 are only required to rule out the second class of failures, but they can 344 still fail for all other reasons. In particular, a compiler that systematically 345 refuses to compile any well formed program is a sound compiler. On the contrary, 346 we would like our certified compiler to fail only in the fourth case. We 347 plan to achieve this aim using the following strategy. First of all, 348 the compiler is abstracted over all non complete heuristics, seen as total 349 functions. To obtain an executable code, the compiler is eventually composed 350 with implementations of the strategies, and the composition takes care of the 351 possibility that the heuristics can fail to find a solution. Secondly, 352 we will reject all malformed programs using dependent types: 353 only well-formed programs should typecheck and the compiler can be applied only 354 to well-typed programs. Finally, exhaustion of bounded resources can be checked 355 only at the very end of the compilation. Therefore, all intermediate compilation 356 steps are now total functions that cannot diverge, nor fail: these properties 357 are directly guaranteed by the type system of Matita. 358 359 At the moment, the plan has not been fulfilled, and we are improving the code 360 according to the plan by progressively strenghthening the code by means of 361 dependent types. We now detail the different ways in which dependent types 362 have been exploited so far. 363 339 364 First, we encode informal invariants, or uses of \texttt{assert false} in the O'Caml code, with dependent types, converting partial functions into total functions. 340 365 There are numerous examples of this throughout the backend. … … 370 395 \end{lstlisting} 371 396 Here, \texttt{codeT} is a parameterised type representing the `structure' of the function's body (a graph in graph based languages, and a list in the linearised LIN language). 372 Specifically, the \texttt{joint\_if\_entry} is a dependent pair consisting of a label and a proof that the label in question is a vertex in the function's graph. 373 A similar device exists for the exit label. 374 375 Finally, we make use of dependent types for another reason: experimentation. 397 Specifically, the \texttt{joint\_if\_entry} is a dependent pair consisting of a label and a proof that the label in question is a vertex in the function's graph. A similar device exists for the exit label. 398 399 We make use of dependent types also for another reason: experimentation. 376 400 Namely, CompCert makes little use of dependent types to encode invariants. 377 401 In contrast, we wish to make as much use of dependent types as possible, both to experiment with different ways of encoding compilers in a proof assistant, but also as a way of `stress testing' Matita's support for dependent types. 378 In particular, we would like to make use of Matita's support for `Russell'-style reasoning. 402 403 Moreover, at the moment we make practically no use of inductive predicates 404 to specify compiler invariants and to describe the semantics of intermediate 405 languages. On the contrary, all predicates are computable functions. Therefore, 406 the proof style that we will adopt will be necessarily significantly different 407 from, say, CompCert's one. At the moment, in Matita ``Russell-''-style reasoning 408 (in the sense of~\cite{sozeauXXX}) seems to be the best solution to work on 409 computable functions. This style is heavily based on the idea that all 410 computable functions should be specified using dependent types to describe 411 their pre and post-conditions. As a consequence, it is natural to add 412 dependent types almost everywhere in the code. 379 413 380 414 %-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%-%
Note: See TracChangeset
for help on using the changeset viewer.