Changeset 1721 for Deliverables


Ignore:
Timestamp:
Feb 22, 2012, 2:38:59 PM (8 years ago)
Author:
mulligan
Message:

some changes to the report

File:
1 edited

Legend:

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

    r1718 r1721  
    140140\end{displaymath}
    141141
     142\section{The RTL to ERTL translation}
     143\label{sect.rtl.ertl.translation}
     144
    142145\begin{displaymath}
    143146\begin{diagram}
    144147        &                         & \llbracket \mathtt{CALL\_ID}(\mathtt{id}, \mathtt{args}, \mathtt{dst}, \mathtt{pc})\rrbracket &                         & \\
    145148        & \ldTo^{\text{external}} &                                                                                               & \rdTo^{\text{internal}} & \\
    146  \skull &                         &                                                                                               &
     149 \skull &                         &                                                                                               &                         & FINISH ME
    147150\end{diagram}
    148151\end{displaymath}
    149 
    150 \section{The RTL to ERTL translation}
    151 \label{sect.rtl.ertl.translation}
    152152
    153153\section{The ERTL to LTL translation}
     
    157157\label{sect.ltl.lin.translation}
    158158
    159 \section{The LIN to ASM translation}
     159We 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
     164The linerisation process is as follows:
     165
     166\begin{enumerate}
     167\item
     168Perform a previsit of the graph
     169\end{enumerate}
     170
     171
     172\section{The LIN to ASM and ASM to MCS-51 machine code translations}
    160173\label{sect.lin.asm.translation}
    161174
    162 \section{The ASM to MCS-51 machine code translation}
    163 \label{sect.asm.mcs-51.machine.code.translation}
     175The LIN to ASM translation step is trivial, being almost the identity function.
     176The only non-trivial 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
     178The ASM to MCS-51 machine code translation step, and the required statements of correctness, are found in an unpublished manuscript attached to this document.
    164179
    165180\end{document}
Note: See TracChangeset for help on using the changeset viewer.