Changeset 1723 for Deliverables/D1.2/CompilerProofOutline
 Timestamp:
 Feb 23, 2012, 10:41:56 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D1.2/CompilerProofOutline/outline.tex
r1721 r1723 6 6 \usepackage{amssymb} 7 7 \usepackage[english]{babel} 8 \usepackage{color} 8 9 \usepackage{diagrams} 10 \usepackage{graphicx} 9 11 \usepackage[colorlinks]{hyperref} 12 \usepackage[utf8x]{inputenc} 13 \usepackage{listings} 10 14 \usepackage{microtype} 11 15 \usepackage{skull} 12 16 \usepackage{stmaryrd} 17 18 \lstdefinelanguage{matitaocaml} { 19 mathescape=true 20 } 21 \lstset{ 22 language=matitaocaml,basicstyle=\tt,columns=flexible,breaklines=false, 23 showspaces=false, showstringspaces=false, extendedchars=false, 24 inputencoding=utf8x, tabsize=2 25 } 13 26 14 27 \title{Proof outline for the correctness of the CerCo compiler} … … 162 175 \end{displaymath} 163 176 164 The linerisation process is as follows: 165 166 \begin{enumerate} 167 \item 168 Perform a previsit of the graph 169 \end{enumerate} 177 The LTL to LIN translation pass also linearises the graph data structure into a list of instructions. 178 Pseudocode for the linearisation process is as follows: 179 180 \begin{lstlisting} 181 let 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} 170 198 171 199
Note: See TracChangeset
for help on using the changeset viewer.