Changeset 1740 for Deliverables

Timestamp:

Feb 24, 2012, 2:32:04 PM (8 years ago)

Author:

sacerdot

Message:

...

File:

• Deliverables/D1.2/CompilerProofOutline/outline.tex (modified) (2 diffs)

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -66 +66 @@
 \end{center}
 
+Here, by `endo-transformation', we mean a mapping from language back to itself:
+the loop optimization step maps the Clight language to itself.
+
 %Our overall statements of correctness with respect to costs will
 %require a correctly labelled program
-
 There are three layers in most of the proofs proposed:
 \begin{enumerate}
@@ -275 +277 @@
 \end{center}
 
-Here, by `endo-transformation', we mean a mapping from language back to itself.
-For example, the constant propagation step maps the RTL language to the RTL language.
-
 \subsection{The RTLabs to RTL translation}
 \label{subsect.rtlabs.rtl.translation}