source: Deliverables/D3.4/Report/report.tex @ 3158

Last change on this file since 3158 was 3158, checked in by campbell, 7 years ago

Some text on measurable subtraces throughout the front-end.

File size: 25.5 KB
Line 
1\documentclass[11pt,epsf,a4wide]{article}
2\usepackage[mathletters]{ucs}
3\usepackage[utf8x]{inputenc}
4\usepackage{listings}
5\usepackage{../../style/cerco}
6\newcommand{\ocaml}{OCaml}
7\newcommand{\clight}{Clight}
8\newcommand{\matita}{Matita}
9\newcommand{\sdcc}{\texttt{sdcc}}
10
11\newcommand{\textSigma}{\ensuremath{\Sigma}}
12
13% LaTeX Companion, p 74
14\newcommand{\todo}[1]{\marginpar{\raggedright - #1}}
15
16\lstdefinelanguage{coq}
17  {keywords={Definition,Lemma,Theorem,Remark,Qed,Save,Inductive,Record},
18   morekeywords={[2]if,then,else},
19  }
20
21\lstdefinelanguage{matita}
22  {keywords={definition,lemma,theorem,remark,inductive,record,qed,let,rec,match,with,Type,and,on},
23   morekeywords={[2]whd,normalize,elim,cases,destruct},
24   mathescape=true,
25   morecomment=[n]{(*}{*)},
26  }
27
28\lstset{language=matita,basicstyle=\small\tt,columns=flexible,breaklines=false,
29        keywordstyle=\color{red}\bfseries,
30        keywordstyle=[2]\color{blue},
31        commentstyle=\color{green},
32        stringstyle=\color{blue},
33        showspaces=false,showstringspaces=false}
34
35\lstset{extendedchars=false}
36\lstset{inputencoding=utf8x}
37\DeclareUnicodeCharacter{8797}{:=}
38\DeclareUnicodeCharacter{10746}{++}
39\DeclareUnicodeCharacter{9001}{\ensuremath{\langle}}
40\DeclareUnicodeCharacter{9002}{\ensuremath{\rangle}}
41
42
43\title{
44INFORMATION AND COMMUNICATION TECHNOLOGIES\\
45(ICT)\\
46PROGRAMME\\
47\vspace*{1cm}Project FP7-ICT-2009-C-243881 \cerco{}}
48
49\date{ }
50\author{}
51
52\begin{document}
53\thispagestyle{empty}
54
55\vspace*{-1cm}
56\begin{center}
57\includegraphics[width=0.6\textwidth]{../../style/cerco_logo.png}
58\end{center}
59
60\begin{minipage}{\textwidth}
61\maketitle
62\end{minipage}
63
64
65\vspace*{0.5cm}
66\begin{center}
67\begin{LARGE}
68\bf
69Report n. D3.4\\
70Front-end Correctness Proofs\\
71\end{LARGE} 
72\end{center}
73
74\vspace*{2cm}
75\begin{center}
76\begin{large}
77Version 1.0
78\end{large}
79\end{center}
80
81\vspace*{0.5cm}
82\begin{center}
83\begin{large}
84Authors:\\
85Brian~Campbell, Ilias~Garnier, James~McKinna, Ian~Stark
86\end{large}
87\end{center}
88
89\vspace*{\fill}
90\noindent
91Project Acronym: \cerco{}\\
92Project full title: Certified Complexity\\
93Proposal/Contract no.: FP7-ICT-2009-C-243881 \cerco{}\\
94
95\clearpage \pagestyle{myheadings} \markright{\cerco{}, FP7-ICT-2009-C-243881}
96
97\newpage
98
99\vspace*{7cm}
100\paragraph{Abstract}
101We report on the correctness proofs for the front-end of the \cerco{} cost
102lifting compiler, considering three distinct parts of the task: showing that
103the \emph{annotated source code} output by the compiler has equivalent
104behaviour to the original input (up to the annotations); showing that a
105\emph{measurable} subtrace of the annotated source code corresponds to an
106equivalent measurable subtrace in the code produced by the front-end, including
107costs; and finally showing that the enriched \emph{structured} execution traces
108required for cost correctness in the back-end can be constructed from the
109properties of the code produced by the front-end.
110
111A key part of our work is that the intensional correctness results that show
112that we get consistent cost measurements throughout the intermediate languages
113of the compiler can be layered on top of normal forward simulation results,
114if we split them into local call-structure preserving results.
115
116This deliverable shows correctness results about the formalised compiler
117described in D3.2, using the source language semantics from D3.1 and
118intermediate language semantics from D3.3.  Together with the companion
119deliverable about the correctness of the back-end, D4.4, we obtain results
120about the whole formalised compiler.
121
122% TODO: mention the deliverable about the extracted compiler et al?
123
124\newpage 
125
126\tableofcontents
127
128% CHECK: clear up any -ize vs -ise
129% CHECK: clear up any "front end" vs "front-end"
130% CHECK: clear up any mentions of languages that aren't textsf'd.
131% CHECK: fix unicode in listings
132
133\section{Introduction}
134
135\todo{add stack space for more precise statement.  Also do some
136translation validation on sound, precise labelling properties.}
137
138The \cerco{} compiler compiles C code targeting microcontrollers implementing
139the Intel 8051 architecture, which produces both the object code and source
140code containing annotations describing the timing behavior of the object code.
141There are two versions: first, an initial prototype implemented in
142\ocaml{}~\cite{d2.2}, and a version formalised in the \matita{} proof
143assistant~\cite{d3.2,d4.2} and then extracted to \ocaml{} code to produce an
144executable compiler.  In this document we present results formalised in
145\matita{} about the front-end of that version of the compiler, and how that fits
146into the verification of the whole compiler.
147
148\todo{maybe mention stack space here?  other additions?  refer to "layering"?}
149A key part of this work was to separate the proofs about the compiled code's
150extensional behaviour (that is, the functional correctness of the compiler)
151from the intensional correctness that the costs given are correct.
152Unfortunately, the ambitious goal of completely verifying the compiler was not
153feasible within the time available, but thanks to this separation of extensional
154and intensional proofs we are able to axiomatize simulation results similar to
155those in other compiler verification projects and concentrate on the novel
156intensional proofs.  The proofs were also made more tractable by introducing
157compile-time checks for the `sound and precise' cost labelling properties
158rather than proving that they are preserved throughout.
159
160The overall statement of correctness says that the annotated program has the
161same behaviour as the input, and that for any suitably well-structured part of
162the execution (which we call \emph{measurable}), the object code will execute
163the same behaviour taking precisely the time given by the cost annotations in
164the annotated source program.
165
166In the next section we recall the structure of the compiler and make the overall
167statement more precise.  Following that, in Section~\ref{sec:fegoals} we
168describe the statements we need to prove about the intermediate \textsf{RTLabs}
169programs sufficient for the back-end proofs.  \todo{rest of document structure}
170
171\section{The compiler and main goals}
172
173TODO: outline compiler, maybe figure from talk, maybe something like the figure
174below.
175
176TODO: might want a version of this figure
177\begin{figure}
178\begin{center}
179\begin{minipage}{.8\linewidth}
180\begin{tabbing}
181\quad \= $\downarrow$ \quad \= \kill
182\textsf{C} (unformalized)\\
183\> $\downarrow$ \> CIL parser (unformalized \ocaml)\\
184\textsf{Clight}\\
185%\> $\downarrow$ \> add runtime functions\\
186\> $\downarrow$ \> \lstinline[language=C]'switch' removal\\
187\> $\downarrow$ \> labelling\\
188\> $\downarrow$ \> cast removal\\
189\> $\downarrow$ \> stack variable allocation and control structure
190 simplification\\
191\textsf{Cminor}\\
192%\> $\downarrow$ \> generate global variable initialization code\\
193\> $\downarrow$ \> transform to RTL graph\\
194\textsf{RTLabs}\\
195\> $\downarrow$ \> check cost labelled properties of RTL graph\\
196\> $\downarrow$ \> start of target specific back-end\\
197\>\quad \vdots
198\end{tabbing}
199\end{minipage}
200\end{center}
201\caption{Front-end languages and compiler passes}
202\label{fig:summary}
203\end{figure}
204
205The compiler function returns the following record on success:
206\begin{lstlisting}[language=matita]
207record compiler_output : Type[0] :=
208 { c_labelled_object_code: labelled_object_code
209 ; c_stack_cost: stack_cost_model
210 ; c_max_stack: nat
211 ; c_init_costlabel: costlabel
212 ; c_labelled_clight: clight_program
213 ; c_clight_cost_map: clight_cost_map
214 }.
215\end{lstlisting}
216It consists of annotated 8051 object code, a mapping from function
217identifiers to the function's stack space usage\footnote{The compiled
218  code's only stack usage is to allocate a fixed-size frame on each
219  function entry and discard it on exit.}, a cost label covering the
220initialisation of global variables and calling the
221\lstinline[language=C]'main' function, the annotated source code, and
222finally a mapping from cost labels to actual execution time costs.
223
224An \ocaml{} pretty printer is used to provide a concrete version of the output
225code.  In the case of the annotated source code, it also inserts the actual
226costs alongside the cost labels, and optionally adds a global cost variable
227and instrumentation to support further reasoning.  \todo{Cross-ref case study
228deliverables}
229
230\subsection{Revisions to the prototype compiler}
231
232TODO: could be a good idea to have this again; stack space,
233initialisation, cost checks, had we dropped cminor loops in previous
234writing?, check mailing list in case I've forgotten something
235
236\subsection{Main goals}
237
238TODO: need an example for this
239
240Informally, our main intensional result links the time difference in a source
241code execution to the time difference in the object code, expressing the time
242for the source by summing the values for the cost labels in the trace, and the
243time for the target by a clock built in to the 8051 executable semantics.
244
245The availability of precise timing information for 8501
246implementations and the design of the compiler allow it to give exact
247time costs in terms of processor cycles.  However, these exact results
248are only available if the subtrace we measure starts and ends at
249suitable points.  In particular, pure computation with no observable
250effects may be reordered and moved past cost labels, so we cannot
251measure time between arbitrary statements in the program.
252
253There is also a constraint on the subtraces that we
254measure due to the requirements of the correctness proof for the
255object code timing analysis.  To be sure that the timings are assigned
256to the correct cost label, we need to know that each return from a
257function call must go to the correct return address.  It is difficult
258to observe this property locally in the object code because it relies
259on much earlier stages in the compiler.  To convey this information to
260the timing analysis extra structure is imposed on the subtraces, which
261we will give more details on in Section~\ref{sec:fegoals}.
262
263% Regarding the footnote, would there even be much point?
264These restrictions are reflected in the subtraces that we give timing
265guarantees on; they must start at a cost label and end at the return
266of the enclosing function of the cost label\footnote{We expect that
267  this would generalise to subtraces between cost labels in the same
268  function, but could not justify the extra complexity that would be
269  required to show this.}.  A typical example of such a subtrace is
270the execution of an entire function from the cost label at the start
271of the function until it returns.  We call such any such subtrace
272\emph{measurable} if it (and the prefix of the trace before it) can
273also be executed within the available stack space.
274
275Now we can give the main intensional statement for the compiler.
276Given a \emph{measurable} subtrace for a labelled \textsf{Clight}
277program, there is a subtrace of the 8051 object code program where the
278time differences match.  Moreover, \emph{observable} parts of the
279trace also match --- these are the appearance of cost labels and
280function calls and returns.
281
282More formally, the definition of this statement in \matita{} is
283\begin{lstlisting}[language=matita]
284definition simulates :=
285  $\lambda$p: compiler_output.
286  let initial_status := initialise_status $\dots$ (cm (c_labelled_object_code $\dots$ p)) in
287  $\forall$m1,m2.
288   measurable Clight_pcs (c_labelled_clight $\dots$ p) m1 m2
289    (lookup_stack_cost (c_stack_cost $\dots$ p)) (c_max_stack $\dots$ p) $\rightarrow$
290  $\forall$c1,c2.
291   clock_after Clight_pcs (c_labelled_clight $\dots$ p) m1 (c_clight_cost_map $\dots$ p) = OK $\dots$ c1 $\rightarrow$
292   clock_after Clight_pcs (c_labelled_clight $\dots$ p) (m1+m2) (c_clight_cost_map $\dots$ p) = OK $\dots$ c2 $\rightarrow$
293  $\exists$n1,n2.
294   observables Clight_pcs (c_labelled_clight $\dots$ p) m1 m2 =
295   observables (OC_preclassified_system (c_labelled_object_code $\dots$ p))
296    (c_labelled_object_code $\dots$ p) n1 n2
297  $\wedge$
298   c2 - c1 = clock $\dots$ (execute n2 ? initial_status) - clock $\dots$ (execute n1 ? initial_status).
299\end{lstlisting}
300where the \lstinline'measurable', \lstinline'clock_after' and
301\lstinline'observables' definitions can be applied to multiple
302languages; in this case the \lstinline'Clight_pcs' record applies them
303to \textsf{Clight} programs.
304
305There is a second part to the statement, which says that the initial
306processing of the input program to produce the cost labelled version
307does not affect the semantics of the program:
308% Yes, I'm paraphrasing the result a tiny bit to remove the observe non-function
309\begin{lstlisting}[language=matita]
310  $\forall$input_program,output.
311  compile input_program = return output $\rightarrow$
312  not_wrong … (exec_inf … clight_fullexec input_program) $\rightarrow$
313  sim_with_labels
314   (exec_inf … clight_fullexec input_program)
315   (exec_inf … clight_fullexec (c_labelled_clight … output))
316\end{lstlisting}
317That is, any successful compilation produces a labelled program that
318has identical behaviour to the original, so long as there is no
319`undefined behaviour'.
320
321Note that this provides full functional correctness, including
322preservation of (non-)termination.  The intensional result above does
323not do this directly --- it does not guarantee the same result or same
324termination.  There are two mitigating factors, however: first, to
325prove the intensional property you need local simulation results that
326can be pieced together to form full behavioural equivalence, only time
327constraints have prevented us from doing so.  Second, if we wish to
328confirm a result, termination, or non-termination we could add an
329observable witness, such as a function that is only called if the
330correct result is given.  The intensional result guarantees that the
331observable witness is preserved, so the program must behave correctly.
332
333\section{Intermediate goals for the front-end}
334\label{sec:fegoals}
335
336The essential parts of the intensional proof were outlined during work
337on a toy
338compiler~\cite{d2.1,springerlink:10.1007/978-3-642-32469-7_3}.  These
339are
340\begin{enumerate}
341\item functional correctness, in particular preserving the trace of
342  cost labels,
343\item the \emph{soundness} and \emph{precision} of the cost labelling
344  on the object code, and
345\item the timing analysis on the object code produces a correct
346  mapping from cost labels to time.
347\end{enumerate}
348
349However, that toy development did not include function calls.  For the
350full \cerco{} compiler we also need to maintain the invariant that
351functions return to the correct program location in the caller, as we
352mentioned in the previous section.  During work on the back-end timing
353analysis (describe in more detail in the companion deliverable, D4.4)
354the notion of a \emph{structured trace} was developed to enforce this
355return property, and also most of the cost labelling properties too.
356
357\begin{figure}
358\begin{center}
359\includegraphics[width=0.5\linewidth]{compiler.pdf}
360\end{center}
361\caption{The compiler and proof outline}
362\label{fig:compiler}
363\end{figure}
364
365Jointly, we generalised the structured traces to apply to any of the
366intermediate languages with some idea of program counter.  This means
367that they are introduced part way through the compiler, see
368Figure~\ref{fig:compiler}.  Proving that a structured trace can be
369constructed at \textsf{RTLabs} has several virtues:
370\begin{itemize}
371\item This is the first language where every operation has its own
372  unique, easily addressable, statement.
373\item Function calls and returns are still handled in the language and
374  so the structural properties are ensured by the semantics.
375\item Many of the back-end languages from \textsf{RTL} share a common
376  core set of definitions, and using structured traces throughout
377  increases this uniformity.
378\end{itemize}
379
380\begin{figure}
381\begin{center}
382\includegraphics[width=0.6\linewidth]{strtraces.pdf}
383\end{center}
384\caption{Nesting of functions in structured traces}
385\label{fig:strtrace}
386\end{figure}
387A structured trace is a mutually inductive data type which principally
388contains the steps from a normal program trace, but arranged into a
389nested structure which groups entire function calls together and
390aggregates individual steps between cost labels (or between the final
391cost label and the return from the function), see
392Figure~\ref{fig:strtrace}.  This capture the idea that the cost labels
393only represent costs \emph{within} a function --- calls to other
394functions are accounted for in the trace for their execution, and we
395can locally regard function calls as a single step.
396
397These structured traces form the core part of the intermediate results
398that we must prove so that the back-end can complete the main
399intensional result stated above.  In full, we provide the back-end
400with
401\begin{enumerate}
402\item A normal trace of the \textbf{prefix} of the program's execution
403  before reaching the measurable subtrace.  (This needs to be
404  preserved so that we know that the stack space consumed is correct.)
405\item The \textbf{structured trace} corresponding to the measurable
406  subtrace.
407\item An additional property about the structured trace that no
408  `program counter' is \textbf{repeated} between cost labels.  Together with
409  the structure in the trace, this takes over from showing that
410  cost labelling is sound and precise.
411\item A proof that the \textbf{observables} have been preserved.
412\item A proof that the \textbf{stack limit} is still observed by the prefix and
413  the structure trace.  (This is largely a consequence of the
414  preservation of observables.)
415\end{enumerate}
416
417Following the outline in Figure~\ref{fig:compiler}, we will first deal
418with the transformations in \textsf{Clight} that produce the source
419program with cost labels, then show that measurable traces can be
420lifted to \textsf{RTLabs}, and finally that we can construct the
421properties listed above ready for the back-end proofs.
422
423\section{Input code to cost labelled program}
424
425The simple form of labelling used in the formalised compiler is not
426quite capable of capturing costs arising from complex C
427\lstinline[language=C]'switch' statements, largely due to the
428fall-through behaviour.  Our first pass replaces these statements with
429simpler C code, allowing our second pass to perform the cost
430labelling.  We show that the behaviour of programs is unchanged by
431these passes.
432
433TODO: both give one-step-sim-by-many forward sim results; switch
434removal tricky, uses aux var to keep result of expr, not central to
435intensional correctness so curtailed proof effort once reasonable
436level of confidence in code gained; labelling much simpler; don't care
437what the labels are at this stage, just need to know when to go
438through extra steps.  Rolled up into a single result with a cofixpoint
439to obtain coinductive statement of equivalence (show).
440
441\section{Finding corresponding measurable subtraces}
442
443There follow the three main passes of the front-end:
444\begin{enumerate}
445\item simplification of casts in \textsf{Clight} code
446\item \textsf{Clight} to \textsf{Cminor} translation, performing stack
447  variable allocation and simplifying control structures
448\item transformation to \textsf{RTLabs} control flow graph
449\end{enumerate}
450\todo{I keep mentioning forward sim results - I probably ought to say
451  something about determinancy} We have taken a common approach to
452each pass: first we build (or axiomatise) forward simulation results
453that are similar to normal compiler proofs, but slightly more
454fine-grained so that we can see that the call structure and relative
455placement of cost labels is preserved.
456
457Then we instantiate a general result which shows that we can find a
458\emph{measurable} subtrace in the target of the pass that corresponds
459to the measurable subtract in the source.  By repeated application of
460this result we can find a measurable subtrace of the execution of the
461\textsf{RTLabs} code, suitable for the construction of a structured
462trace (see Section~\ref{sec:structuredtrace}.  This is essentially an
463extra layer on top of the simulation proofs that provides us with the
464extra information required for our intensional correctness proof.
465
466\subsection{Generic measurable subtrace lifting proof}
467
468Our generic proof is parametrised on a record containing small-step
469semantics for the source and target language, a classification of
470states (the same form of classification is used when defining
471structured traces), a simulation relation which loosely respects the
472classification and cost labelling \todo{this isn't very helpful} and
473four simulation results:
474\begin{enumerate}
475\item a step from a `normal' state (which is not classified as a call
476  or return) which is not a cost label is simulated by zero or more
477  `normal' steps;
478\item a step from a `call' state followed by a cost label step is
479  simulated by a step from a `call' state, a corresponding label step,
480  then zero or more `normal' steps;
481\item a step from a `call' state not followed by a cost label
482  similarly (note that this case cannot occur in a well-labelled
483  program, but we do not have enough information locally to exploit
484  this); and
485\item a cost label step is simulated by a cost label step.
486\end{enumerate}
487Finally, we need to know that a successfully translated program will
488have an initial state in the simulation relation with the original
489program's initial state.
490
491\begin{figure}
492\begin{center}
493\includegraphics[width=0.5\linewidth]{meassim.pdf}
494\end{center}
495\caption{Tiling of simulation for a measurable subtrace}
496\label{fig:tiling}
497\end{figure}
498
499To find the measurable subtrace in the target program's execution we
500walk along the original program's execution trace applying the
501appropriate simulation result by induction on the number of steps.
502While the number of steps taken varies, the overall structure is
503preserved, as illustrated in Figure~\ref{fig:tiling}.  By preserving
504the structure we also maintain the same intensional observables.  One
505delicate point is that the cost label following a call must remain
506directly afterwards\footnote{The prototype compiler allowed some
507  straight-line code to appear before the cost label until a later
508  stage of the compiler, but we must move the requirement forward to
509  fit with the structured traces.}
510% Damn it, I should have just moved the cost label forwards in RTLabs,
511% like the prototype does in RTL to ERTL; the result would have been
512% simpler.  Or was there some reason not to do that?
513(both in the program code and in the execution trace), even if we
514introduce extra steps, for example to store parameters in memory in
515\textsf{Cminor}.  Thus we have a version of the call simulation
516that deals with both in one result.
517
518In addition to the subtrace we are interested in measuring we must
519also prove that the earlier part of the trace is also preserved in
520order to use the simulation from the initial state.  It also
521guarantees that we do not run out of stack space before the subtrace
522we are interested in.  The lemmas for this prefix and the measurable
523subtrace are similar, following the pattern above.  However, the
524measurable subtrace also requires us to rebuild the termination
525proof.  This has a recursive form:
526\begin{lstlisting}[language=matita]
527let rec will_return_aux C (depth:nat)
528                             (trace:list (cs_state … C × trace)) on trace : bool :=
529match trace with
530[ nil $\Rightarrow$ false
531| cons h tl $\Rightarrow$
532  let $\langle$s,tr$\rangle$ := h in
533  match cs_classify C s with
534  [ cl_call $\Rightarrow$ will_return_aux C (S depth) tl
535  | cl_return $\Rightarrow$
536      match depth with
537      [ O $\Rightarrow$ match tl with [ nil $\Rightarrow$ true | _ $\Rightarrow$ false ]
538      | S d $\Rightarrow$ will_return_aux C d tl
539      ]
540  | _ $\Rightarrow$ will_return_aux C depth tl
541  ]
542].
543\end{lstlisting}
544The \lstinline'depth' is the number of return states we need to see
545before we have returned to the original function (initially zero) and
546\lstinline'trace' the measurable subtrace obtained from the running
547the semantics for the correct number of steps.  This definition
548unfolds tail recursively for each step, and once the corresponding
549simulation result has been applied a new one for the target can be
550asserted by unfolding and applying the induction hypothesis on the
551shorter trace.
552
553This then gives us an overall result for any simulation fitting the
554requirements above (contained in the \lstinline'meas_sim' record):
555\begin{lstlisting}[language=matita]
556theorem measured_subtrace_preserved :
557  $\forall$MS:meas_sim.
558  $\forall$p1,p2,m,n,stack_cost,max.
559  ms_compiled MS p1 p2 $\rightarrow$
560  measurable (ms_C1 MS) p1 m n stack_cost max $\rightarrow$
561  $\exists$m',n'.
562    measurable (ms_C2 MS) p2 m' n' stack_cost max $\wedge$
563    observables (ms_C1 MS) p1 m n = observables (ms_C2 MS) p2 m' n'.
564\end{lstlisting}
565The stack space requirement that is embedded in \lstinline'measurable'
566is a consequence of the preservation of observables.
567
568TODO: how to deal with untidy edges wrt to sim rel; anything to
569say about obs?
570
571TODO: say something about termination measures; cost labels are
572statements/exprs in these languages; split call/return gives simpler
573simulations
574
575\subsection{Simulation results for each pass}
576
577\todo{don't use loop structures from CompCert, go straight to jumps}
578
579\section{Checking cost labelling properties}
580
581TODO: ideal for this development would be to prove at labelling stage,
582preserve throughout, fits with use of dep types to reduce partiality
583of phases; time pressures suggest different approach: t.v. style,
584runtime check only do proof in one place rather than three; can't push
585further due to structured traces, possible future investigation if ...
586
587\section{Existence of a structured trace}
588\label{sec:structuredtrace}
589
590TODO: design, basic structure from termination proof, how cost
591labelling props are baked in; unrepeating PCs, remainder of sound
592labellings; coinductive version for whole programs, reason/relevance,
593use of em (maybe a general comment about uses of classical reasoning
594in development)
595
596\section{Conclusion}
597
598TODO
599
600TODO: appendix on code layout?
601
602\bibliographystyle{plain}
603\bibliography{report}
604
605\end{document}
Note: See TracBrowser for help on using the repository browser.