# Changeset 1726 for Deliverables

Ignore:
Timestamp:
Feb 23, 2012, 1:14:56 PM (9 years ago)
Message:

Finished description of LTL to LIN

File:
1 edited

### Legend:

Unmodified
 r1725 \end{enumerate} We assume that these properties will be easy consequences of the invariants on the linearisation function defined above. The final condition above is potentially a little opaque, so we explain further. First, the only instructions that can reasonably appear in final position at the end of a program are returns or backward jumps, as any other instruction would cause execution to fall out' of the end of the program (for example, when a function invoked with \texttt{CALL} returns, it returns to the next instruction past the \texttt{CALL} that invoked it). However, in LIN, though each function's graph has been linearised, the entire program is not yet fully linearised into a list of instructions, but rather, a list of functions', each consisting of a linearised body along with other data. Each well-formed function must end with a call to \texttt{RET}, and therefore the only correct instruction that can terminate a LIN program is a \texttt{RET} instruction. \section{The LIN to ASM and ASM to MCS-51 machine code translations}