Changeset 1723 for Deliverables/D1.2/CompilerProofOutline/outline.tex

Timestamp:

Feb 23, 2012, 10:41:56 AM (8 years ago)

Author:

mulligan

Message:

added more to header of file, commit to avoid conflicts with jaap

File:

• Deliverables/D1.2/CompilerProofOutline/outline.tex (modified) (2 diffs)

Deliverables/D1.2/CompilerProofOutline/outline.tex

@@ -6 +6 @@
 \usepackage{amssymb}
 \usepackage[english]{babel}
+\usepackage{color}
 \usepackage{diagrams}
+\usepackage{graphicx}
 \usepackage[colorlinks]{hyperref}
+\usepackage[utf8x]{inputenc}
+\usepackage{listings}
 \usepackage{microtype}
 \usepackage{skull}
 \usepackage{stmaryrd}
+
+\lstdefinelanguage{matita-ocaml} {
+  mathescape=true
+}
+\lstset{
+  language=matita-ocaml,basicstyle=\tt,columns=flexible,breaklines=false,
+  showspaces=false, showstringspaces=false, extendedchars=false,
+  inputencoding=utf8x, tabsize=2
+}
 
 \title{Proof outline for the correctness of the CerCo compiler}
@@ -162 +175 @@
 \end{displaymath}
 
-The linerisation process is as follows:
-
-\begin{enumerate}
-\item
-Perform a previsit of the graph
-\end{enumerate}
+The LTL to LIN translation pass also linearises the graph data structure into a list of instructions.
+Pseudocode for the linearisation process is as follows:
+
+\begin{lstlisting}
+let rec linearise graph visited required generated todo :=
+  match todo with
+  | l::todo ->
+    if l $\in$ visited then
+      let generated := generated $\cup\ \{$ Goto l $\}$ in
+      let required := required $\cup$ l in
+        linearise graph visited required generated todo
+    else
+      -- 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
+      let successor := succ(l, graph) in
+      let todo := successor::todo in
+        linearise graph visited required generated todo
+  | []      -> (required, generated)
+\end{lstlisting}