# Changeset 1725

Ignore:
Timestamp:
Feb 23, 2012, 12:51:24 PM (8 years ago)
Message:

commit to avoid conflicts

File:
1 edited

### Legend:

Unmodified
 r1724 linearise graph visited required generated todo else -- Get the instruction at label l'' in the graph -- Get the instruction at label l' in the graph let lookup := graph(l) in let generated := generated $\cup\ \{$ lookup $\}$ in -- Find the successor of the instruction at label l'' in the graph -- Find the successor of the instruction at label l' in the graph let successor := succ(l, graph) in let todo := successor::todo in \end{lstlisting} It is easy to see that this linearisation process eventually terminates. In particular, the size of the visited label set is monotonically increasing, and is bounded above by the size of the graph that we are linearising. The initial call to \texttt{linearise} sees the \texttt{visited}, \texttt{required} and \texttt{generated} sets set to the empty set, and \texttt{todo} initialized with the singleton list consisting of the entry point of the graph. We envisage needing to prove the following invariants on the linearisation function above: \begin{enumerate} \item $\mathtt{visited} \approx \mathtt{generated}$, where $\approx$ is \emph{multiset} equality, as \texttt{generated} is a set of instructions where instructions may mention labels multiple times, and \texttt{visited} is a set of labels, \item $\forall \mathtt{l} \in \mathtt{generated}.\ \mathtt{succ(l,\ graph)} \subseteq \mathtt{required} \cup \mathtt{todo}$, \item $\mathtt{required} \subseteq \mathtt{visited}$, \item $\mathtt{visited} \cap \mathtt{todo} = \emptyset$. \end{enumerate} The invariants collectively imply the following properties, crucial to correctness, about the linearisation process: \begin{enumerate} \item Every graph node is visited at most once, \item Every instruction that is generated is generated due to some graph node being visited, \item The successor instruction of every instruction that has been visited already will eventually be visited too. \end{enumerate} Note, because the LTL to LIN transformation is the first time the program is linearised, we must discover a notion of `well formed program' suitable for linearised forms. In particular, we see the notion of well formedness (yet to be formally defined) resting on the following conditions: \begin{enumerate} \item For every jump to a label in a linearised program, the target label exists at some point in the program, \item Each label is unique, appearing only once in the program, \item The final instruction of a program must be a return. \end{enumerate} The final condition above is potentially a little opaque, so we explain further. \section{The LIN to ASM and ASM to MCS-51 machine code translations}