Changeset 1726 for Deliverables


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

Finished description of LTL to LIN

File:
1 edited

Legend:

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

    r1725 r1726  
    283283\end{enumerate}
    284284
     285We assume that these properties will be easy consequences of the invariants on the linearisation function defined above.
     286
    285287The final condition above is potentially a little opaque, so we explain further.
     288First, 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).
     289However, 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.
     290Each 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.
    286291
    287292\section{The LIN to ASM and ASM to MCS-51 machine code translations}
Note: See TracChangeset for help on using the changeset viewer.