Ignore:
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:
1 edited

Legend:

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

    r1721 r1723  
    66\usepackage{amssymb}
    77\usepackage[english]{babel}
     8\usepackage{color}
    89\usepackage{diagrams}
     10\usepackage{graphicx}
    911\usepackage[colorlinks]{hyperref}
     12\usepackage[utf8x]{inputenc}
     13\usepackage{listings}
    1014\usepackage{microtype}
    1115\usepackage{skull}
    1216\usepackage{stmaryrd}
     17
     18\lstdefinelanguage{matita-ocaml} {
     19  mathescape=true
     20}
     21\lstset{
     22  language=matita-ocaml,basicstyle=\tt,columns=flexible,breaklines=false,
     23  showspaces=false, showstringspaces=false, extendedchars=false,
     24  inputencoding=utf8x, tabsize=2
     25}
    1326
    1427\title{Proof outline for the correctness of the CerCo compiler}
     
    162175\end{displaymath}
    163176
    164 The linerisation process is as follows:
    165 
    166 \begin{enumerate}
    167 \item
    168 Perform a previsit of the graph
    169 \end{enumerate}
     177The LTL to LIN translation pass also linearises the graph data structure into a list of instructions.
     178Pseudocode for the linearisation process is as follows:
     179
     180\begin{lstlisting}
     181let rec linearise graph visited required generated todo :=
     182  match todo with
     183  | l::todo ->
     184    if l $\in$ visited then
     185      let generated := generated $\cup\ \{$ Goto l $\}$ in
     186      let required := required $\cup$ l in
     187        linearise graph visited required generated todo
     188    else
     189      -- Get the instruction at label ``l'' in the graph
     190      let lookup := graph(l) in
     191      let generated := generated $\cup\ \{$ lookup $\}$ in
     192      -- Find the successor of the instruction at label ``l'' in the graph
     193      let successor := succ(l, graph) in
     194      let todo := successor::todo in
     195        linearise graph visited required generated todo
     196  | []      -> (required, generated)
     197\end{lstlisting}
    170198
    171199
Note: See TracChangeset for help on using the changeset viewer.