Changeset 1721 for Deliverables/D1.2/CompilerProofOutline
 Timestamp:
 Feb 22, 2012, 2:38:59 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1718 r1721 140 140 \end{displaymath} 141 141 142 \section{The RTL to ERTL translation} 143 \label{sect.rtl.ertl.translation} 144 142 145 \begin{displaymath} 143 146 \begin{diagram} 144 147 & & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket & & \\ 145 148 & \ldTo^{\text{external}} & & \rdTo^{\text{internal}} & \\ 146 \skull & & & 149 \skull & & & & FINISH ME 147 150 \end{diagram} 148 151 \end{displaymath} 149 150 \section{The RTL to ERTL translation}151 \label{sect.rtl.ertl.translation}152 152 153 153 \section{The ERTL to LTL translation} … … 157 157 \label{sect.ltl.lin.translation} 158 158 159 \section{The LIN to ASM translation} 159 We require a map, $\sigma$, from LTL statuses, where program counters are represented as labels in a graph data structure, to LIN statuses, where program counters are natural numbers: 160 \begin{displaymath} 161 \mathtt{pc : label} \stackrel{\sigma}{\longrightarrow} \mathbb{N} 162 \end{displaymath} 163 164 The linerisation process is as follows: 165 166 \begin{enumerate} 167 \item 168 Perform a previsit of the graph 169 \end{enumerate} 170 171 172 \section{The LIN to ASM and ASM to MCS51 machine code translations} 160 173 \label{sect.lin.asm.translation} 161 174 162 \section{The ASM to MCS51 machine code translation} 163 \label{sect.asm.mcs51.machine.code.translation} 175 The LIN to ASM translation step is trivial, being almost the identity function. 176 The only nontrivial feature of the LIN to ASM translation is that all labels are `named apart' so that there is no chance of freshly generated labels from different namespaces clashing with labels from another namespace. 177 178 The ASM to MCS51 machine code translation step, and the required statements of correctness, are found in an unpublished manuscript attached to this document. 164 179 165 180 \end{document}
Note: See TracChangeset
for help on using the changeset viewer.