| author | Christian Urban <urbanc@in.tum.de> | 
| Tue, 27 Nov 2018 00:45:26 +0000 | |
| changeset 609 | ff17a6f694dd | 
| parent 538 | e03107e79d26 | 
| child 610 | ce5e0426c92a | 
| permissions | -rw-r--r-- | 
| 
65
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
1  | 
\documentclass[dvipsnames,14pt,t]{beamer}
 | 
| 
309
 
640e4a05cd9b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
2  | 
\usepackage{../slides}
 | 
| 
215
 
828303e8e4af
updated slides
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
207 
diff
changeset
 | 
3  | 
\usepackage{../langs}
 | 
| 609 | 4  | 
\usepackage{../data}
 | 
| 
309
 
640e4a05cd9b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
5  | 
\usepackage{../graphics}
 | 
| 
379
 
fa2589ec0fae
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
312 
diff
changeset
 | 
6  | 
\usepackage{../grammar}
 | 
| 
310
 
d384fe01d0e8
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
309 
diff
changeset
 | 
7  | 
\usepackage{soul}
 | 
| 609 | 8  | 
|
| 
310
 
d384fe01d0e8
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
309 
diff
changeset
 | 
9  | 
|
| 609 | 10  | 
% beamer stuff  | 
| 459 | 11  | 
\renewcommand{\slidecaption}{CFL 09, King's College London}
 | 
| 609 | 12  | 
\newcommand{\bl}[1]{\textcolor{blue}{#1}}       
 | 
13  | 
||
| 
310
 
d384fe01d0e8
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
309 
diff
changeset
 | 
14  | 
|
| 
65
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
15  | 
\begin{document}
 | 
| 609 | 16  | 
|
| 
65
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
17  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
309
 
640e4a05cd9b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
215 
diff
changeset
 | 
18  | 
\begin{frame}[t]
 | 
| 
65
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
19  | 
\frametitle{%
 | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
20  | 
  \begin{tabular}{@ {}c@ {}}
 | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
21  | 
\\[-3mm]  | 
| 459 | 22  | 
\LARGE Compilers and \\[-2mm]  | 
| 538 | 23  | 
\LARGE Formal Languages (9)\\[3mm]  | 
| 
65
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
24  | 
  \end{tabular}}
 | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
25  | 
|
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
26  | 
\normalsize  | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
27  | 
  \begin{center}
 | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
28  | 
  \begin{tabular}{ll}
 | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
29  | 
Email: & christian.urban at kcl.ac.uk\\  | 
| 609 | 30  | 
  Office: & N\liningnums{7.07} (North Wing, Bush House)\\
 | 
31  | 
Slides: & KEATS (also homework is there)\\  | 
|
| 538 | 32  | 
  \end{tabular}
 | 
33  | 
  \end{center}
 | 
|
| 
310
 
d384fe01d0e8
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
309 
diff
changeset
 | 
34  | 
|
| 609 | 35  | 
\end{frame}
 | 
36  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
37  | 
||
38  | 
||
39  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
40  | 
\begin{frame}[t]
 | 
|
41  | 
\frametitle{While Language}
 | 
|
42  | 
||
43  | 
\begin{center}
 | 
|
44  | 
\bl{\begin{tabular}{@{}lcl@{}}
 | 
|
45  | 
\\[-12mm]  | 
|
46  | 
\meta{Stmt} & $::=$ &  $\texttt{skip}$\\
 | 
|
47  | 
              & $|$ & \textit{Id}\;\texttt{:=}\;\meta{AExp}\\
 | 
|
48  | 
              & $|$ & \texttt{if}\; \meta{BExp} \;\texttt{then}\; \meta{Block} \;\texttt{else}\; \meta{Block}\\
 | 
|
49  | 
              & $|$ & \texttt{while}\; \meta{BExp} \;\texttt{do}\; \meta{Block}\\
 | 
|
50  | 
              & $|$ & \texttt{read}\;\textit{Id}\\
 | 
|
51  | 
              & $|$ & \texttt{write}\;\textit{Id}\\
 | 
|
52  | 
              & $|$ & \texttt{write}\;\textit{String}\medskip\\
 | 
|
53  | 
\meta{Stmts} & $::=$ &  \meta{Stmt} \;\texttt{;}\; \meta{Stmts} $|$  \meta{Stmt}\medskip\\
 | 
|
54  | 
\meta{Block} & $::=$ &  \texttt{\{}\,\meta{Stmts}\,\texttt{\}} $|$ \meta{Stmt}\medskip\\
 | 
|
55  | 
\meta{AExp} & $::=$ & \ldots\\
 | 
|
56  | 
\meta{BExp} & $::=$ & \ldots\\
 | 
|
57  | 
\end{tabular}}
 | 
|
58  | 
\end{center}
 | 
|
59  | 
\end{frame}
 | 
|
60  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
61  | 
||
62  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
63  | 
\begin{frame}[c]
 | 
|
64  | 
\frametitle{\begin{tabular}{c}Fibonacci Numbers\end{tabular}}
 | 
|
65  | 
||
66  | 
\mbox{}\\[-18mm]\mbox{}
 | 
|
67  | 
||
68  | 
{\lstset{language=While}\fontsize{10}{12}\selectfont
 | 
|
69  | 
\texttt{\lstinputlisting{../progs/fib.while}}}
 | 
|
70  | 
||
71  | 
\end{frame}
 | 
|
72  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
73  | 
||
74  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
75  | 
\begin{frame}[c,fragile]
 | 
|
76  | 
\frametitle{BF***}
 | 
|
77  | 
||
78  | 
some big array, say \texttt{a}; 7 (8) instructions:
 | 
|
79  | 
||
80  | 
\begin{itemize}
 | 
|
81  | 
\item \texttt{>} move \texttt{ptr++}
 | 
|
82  | 
\item \texttt{<} move \texttt{ptr-{}-}
 | 
|
83  | 
\item \texttt{+} add \texttt{a[ptr]++}
 | 
|
84  | 
\item \texttt{-} subtract \texttt{a[ptr]-{}-}
 | 
|
85  | 
\item \texttt{.} print out \texttt{a[ptr]} as ASCII
 | 
|
86  | 
\item \texttt{[} if \texttt{a[ptr] == 0} jump just after the corresponding \texttt{]}; otherwise \texttt{ptr++}
 | 
|
87  | 
\item \texttt{]} if \texttt{a[ptr] != 0} jump just after the corresponding \texttt{[}; otherwise \texttt{ptr++}
 | 
|
88  | 
||
89  | 
\end{itemize}  
 | 
|
90  | 
||
91  | 
\end{frame}
 | 
|
92  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
93  | 
||
94  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
95  | 
\begin{frame}[c,fragile]
 | 
|
96  | 
\frametitle{Arrays in While}
 | 
|
| 
310
 
d384fe01d0e8
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
309 
diff
changeset
 | 
97  | 
|
| 609 | 98  | 
\begin{itemize}
 | 
99  | 
\item \texttt{new arr[15000]}\medskip 
 | 
|
100  | 
\item \texttt{x := 3 + arr[3 + y]}\medskip 
 | 
|
101  | 
\item \texttt{arr[42 * n] := ...}
 | 
|
102  | 
\end{itemize}  
 | 
|
103  | 
||
104  | 
\end{frame}
 | 
|
105  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
106  | 
||
107  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
108  | 
\begin{frame}[c,fragile]
 | 
|
109  | 
\frametitle{New Arrays}
 | 
|
110  | 
||
111  | 
\begin{lstlisting}[mathescape,numbers=none,language=While]
 | 
|
112  | 
new arr[number]  | 
|
113  | 
\end{lstlisting}\bigskip\bigskip
 | 
|
114  | 
||
115  | 
\begin{lstlisting}[mathescape,numbers=none,language=While]
 | 
|
116  | 
ldc number  | 
|
117  | 
newarray int  | 
|
118  | 
astore loc_var  | 
|
119  | 
\end{lstlisting}
 | 
|
120  | 
||
121  | 
||
122  | 
\end{frame}
 | 
|
123  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
124  | 
||
125  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
126  | 
\begin{frame}[c,fragile]
 | 
|
127  | 
\frametitle{Array Update}
 | 
|
128  | 
||
129  | 
\begin{lstlisting}[mathescape,numbers=none,language=While]
 | 
|
130  | 
arr[...] :=  | 
|
131  | 
\end{lstlisting}\bigskip\bigskip
 | 
|
132  | 
||
133  | 
\begin{lstlisting}[mathescape,numbers=none,language=While]
 | 
|
134  | 
aload loc_var  | 
|
135  | 
index_aexp  | 
|
136  | 
value_aexp  | 
|
137  | 
iastore  | 
|
138  | 
\end{lstlisting}
 | 
|
139  | 
||
140  | 
||
141  | 
\end{frame}
 | 
|
142  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
143  | 
||
144  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
145  | 
\begin{frame}[c,fragile]
 | 
|
146  | 
\frametitle{Array Lookup in AExp}
 | 
|
147  | 
||
148  | 
\begin{lstlisting}[mathescape,numbers=none,language=While]
 | 
|
149  | 
...arr[...]...  | 
|
150  | 
\end{lstlisting}\bigskip\bigskip
 | 
|
151  | 
||
152  | 
\begin{lstlisting}[mathescape,numbers=none,language=While]
 | 
|
153  | 
aload loc_var  | 
|
154  | 
index_aexp  | 
|
155  | 
iaload  | 
|
156  | 
\end{lstlisting}
 | 
|
157  | 
||
158  | 
||
159  | 
\end{frame}
 | 
|
160  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
|
| 
310
 
d384fe01d0e8
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
309 
diff
changeset
 | 
161  | 
|
| 
 
d384fe01d0e8
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
309 
diff
changeset
 | 
162  | 
|
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
163  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
164  | 
  \begin{frame}[c]
 | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
165  | 
  \frametitle{Dijkstra on Testing}
 | 
| 
206
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
166  | 
|
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
167  | 
  \begin{bubble}[10cm]
 | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
168  | 
``Program testing can be a very effective way to show the  | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
169  | 
presence of bugs, but it is hopelessly inadequate for showing  | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
170  | 
their absence.''  | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
171  | 
  \end{bubble}\bigskip
 | 
| 609 | 172  | 
|
173  | 
\small  | 
|
174  | 
What is good about compilers: the either seem to work,  | 
|
175  | 
or go horribly wrong (most of the time).  | 
|
176  | 
||
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
177  | 
  \end{frame}
 | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
178  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
206
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
179  | 
|
| 
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
180  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
181  | 
\begin{frame}[c]
 | 
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
182  | 
\frametitle{\Large Proving Programs to be Correct}
 | 
| 
206
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
183  | 
|
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
184  | 
\begin{bubble}[10cm]
 | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
185  | 
\small  | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
186  | 
{\bf Theorem:} There are infinitely many prime 
 | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
187  | 
numbers.\medskip\\  | 
| 
206
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
188  | 
|
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
189  | 
{\bf Proof} \ldots\\
 | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
190  | 
\end{bubble}\bigskip
 | 
| 
206
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
191  | 
|
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
192  | 
|
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
193  | 
similarly\bigskip  | 
| 
206
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
194  | 
|
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
195  | 
\begin{bubble}[10cm]
 | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
196  | 
\small  | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
197  | 
{\bf Theorem:} The program is doing what 
 | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
198  | 
it is supposed to be doing.\medskip  | 
| 
206
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
199  | 
|
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
200  | 
{\bf Long, long proof} \ldots\\
 | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
201  | 
\end{bubble}\bigskip\medskip
 | 
| 
206
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
202  | 
|
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
203  | 
\small This can be a gigantic proof. The only hope is to have  | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
204  | 
help from the computer. `Program' is here to be understood to be  | 
| 609 | 205  | 
quite general (compiler, OS, \ldots).  | 
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
206  | 
|
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
207  | 
\end{frame}
 | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
208  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
206
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
209  | 
|
| 
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
210  | 
|
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
211  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
212  | 
|
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
213  | 
\begin{frame}[c]
 | 
| 609 | 214  | 
\frametitle{Can This Be Done?}
 | 
| 
206
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
215  | 
|
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
216  | 
\begin{itemize}
 | 
| 609 | 217  | 
\item in 2008, verification of a small C-compiler  | 
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
218  | 
\begin{itemize}
 | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
219  | 
\item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour''  | 
| 609 | 220  | 
\item is as good as \texttt{gcc -O1}, but much, much less buggy 
 | 
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
221  | 
\end{itemize}
 | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
222  | 
\end{itemize}
 | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
223  | 
|
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
224  | 
\begin{center}
 | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
225  | 
  \includegraphics[scale=0.12]{../pics/compcert.png}
 | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
226  | 
\end{center}
 | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
227  | 
|
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
228  | 
\end{frame}
 | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
229  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
206
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
230  | 
|
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
231  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
232  | 
\begin{frame}[c]
 | 
| 609 | 233  | 
\frametitle{Fuzzy Testing C-Compilers}
 | 
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
234  | 
|
| 
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
235  | 
\begin{itemize}
 | 
| 609 | 236  | 
\item tested GCC, LLVM and others by randomly generating  | 
237  | 
C-programs  | 
|
238  | 
\item found more than 300 bugs in GCC and also  | 
|
239  | 
many in LLVM (some of them highest-level critical)\bigskip  | 
|
240  | 
\item about CompCert:  | 
|
| 
206
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
241  | 
|
| 609 | 242  | 
\begin{bubble}[10cm]\small ``The striking thing about our CompCert
 | 
243  | 
results is that the middle-end bugs we found in all other  | 
|
244  | 
compilers are absent. As of early 2011, the under-development  | 
|
245  | 
version of CompCert is the only compiler we have tested for  | 
|
246  | 
which Csmith cannot find wrong-code errors. This is not for  | 
|
247  | 
lack of trying: we have devoted about six CPU-years to the  | 
|
248  | 
task.''  | 
|
249  | 
\end{bubble} 
 | 
|
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
250  | 
\end{itemize}
 | 
| 
206
 
85b961f1eee9
added
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
151 
diff
changeset
 | 
251  | 
|
| 
383
 
a6a6bf32fade
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
381 
diff
changeset
 | 
252  | 
\end{frame}
 | 
| 609 | 253  | 
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%  | 
| 
82
 
06c3ec0b452e
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
81 
diff
changeset
 | 
254  | 
|
| 
65
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
255  | 
\end{document}
 | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
256  | 
|
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
257  | 
%%% Local Variables:  | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
258  | 
%%% mode: latex  | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
259  | 
%%% TeX-master: t  | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
260  | 
%%% End:  | 
| 
 
ade6af51402c
tuned
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
261  |