Changeset 1740


Ignore:
Timestamp:
Feb 24, 2012, 2:32:04 PM (7 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D1.2/CompilerProofOutline/outline.tex

    r1739 r1740  
    6666\end{center}
    6767
     68Here, by `endo-transformation', we mean a mapping from language back to itself:
     69the loop optimization step maps the Clight language to itself.
     70
    6871%Our overall statements of correctness with respect to costs will
    6972%require a correctly labelled program
    70 
    7173There are three layers in most of the proofs proposed:
    7274\begin{enumerate}
     
    275277\end{center}
    276278
    277 Here, by `endo-transformation', we mean a mapping from language back to itself.
    278 For example, the constant propagation step maps the RTL language to the RTL language.
    279 
    280279\subsection{The RTLabs to RTL translation}
    281280\label{subsect.rtlabs.rtl.translation}
Note: See TracChangeset for help on using the changeset viewer.