|
327
|
1 |
% !TEX program = xelatex
|
|
239
|
2 |
\documentclass[dvipsnames,14pt,t,xelatex]{beamer}
|
|
|
3 |
\usepackage{../slides}
|
|
|
4 |
\usepackage{../graphics}
|
|
|
5 |
\usepackage{../langs}
|
|
|
6 |
%%\usepackage{../data}
|
|
327
|
7 |
%%\usepackage[export]{adjustbox}
|
|
|
8 |
\usetikzlibrary{shapes,arrows,shadows}
|
|
|
9 |
|
|
239
|
10 |
|
|
|
11 |
\hfuzz=220pt
|
|
|
12 |
|
|
|
13 |
%\setmonofont[Scale=.88]{Consolas}
|
|
|
14 |
%\newfontfamily{\consolas}{Consolas}
|
|
|
15 |
|
|
|
16 |
\lstset{language=Scala,
|
|
|
17 |
style=mystyle,
|
|
|
18 |
numbersep=0pt,
|
|
|
19 |
numbers=none,
|
|
|
20 |
xleftmargin=0mm}
|
|
|
21 |
|
|
|
22 |
\newcommand{\bl}[1]{\textcolor{blue}{#1}}
|
|
|
23 |
|
|
|
24 |
% beamer stuff
|
|
|
25 |
\renewcommand{\slidecaption}{PEP (Scala) 05, King's College London}
|
|
|
26 |
|
|
|
27 |
\begin{document}
|
|
|
28 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
29 |
\begin{frame}[t]
|
|
|
30 |
\frametitle{%
|
|
|
31 |
\begin{tabular}{@ {}c@ {}}
|
|
|
32 |
\\[5mm]
|
|
|
33 |
\huge PEP Scala (5)
|
|
|
34 |
\end{tabular}}
|
|
|
35 |
|
|
|
36 |
\normalsize
|
|
|
37 |
\begin{center}
|
|
|
38 |
\begin{tabular}{ll}
|
|
|
39 |
Email: & christian.urban at kcl.ac.uk\\
|
|
327
|
40 |
Office: & N\liningnums{7.07} (North Wing, Bush House)\bigskip\\
|
|
|
41 |
Slides \& Code: & KEATS\\
|
|
|
42 |
& \onslide<2>{\alert{PDF: A Crash-Course in Scala}}\bigskip\\
|
|
|
43 |
Office Hours: & Thursdays 12:00 -- 14:00\\
|
|
|
44 |
Additionally: & (for Scala) Tuesdays 10:45 -- 11:45\\
|
|
239
|
45 |
\end{tabular}
|
|
|
46 |
\end{center}
|
|
|
47 |
|
|
|
48 |
\end{frame}
|
|
|
49 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
50 |
|
|
240
|
51 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
52 |
|
|
|
53 |
\begin{frame}[c]
|
|
327
|
54 |
\frametitle{Marks for Preliminary 8}
|
|
|
55 |
|
|
|
56 |
Raw marks (265 submissions):\bigskip
|
|
240
|
57 |
|
|
327
|
58 |
\begin{itemize}
|
|
|
59 |
\item 4\%: \hspace{4mm}211
|
|
|
60 |
\item 3\%: \hspace{4mm}11
|
|
|
61 |
\item 2\%: \hspace{4mm}14
|
|
|
62 |
\item 1\%: \hspace{4mm}8
|
|
|
63 |
\item 0\%: \hspace{4mm}21
|
|
|
64 |
\end{itemize}\bigskip\bigskip
|
|
|
65 |
|
|
|
66 |
\footnotesize
|
|
|
67 |
(plagiarism/collusion interviews ongoing again!)
|
|
|
68 |
|
|
|
69 |
\end{frame}
|
|
|
70 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
71 |
|
|
|
72 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
73 |
|
|
|
74 |
\begin{frame}[c]
|
|
|
75 |
\frametitle{Plan for Today}
|
|
240
|
76 |
|
|
|
77 |
\begin{itemize}
|
|
327
|
78 |
\item Being Lazy
|
|
|
79 |
\item Polymorphic Types
|
|
|
80 |
\item Immutable OOP
|
|
|
81 |
\item Making Fun about Scala
|
|
|
82 |
\end{itemize}
|
|
|
83 |
|
|
240
|
84 |
\end{frame}
|
|
327
|
85 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
86 |
|
|
|
87 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
88 |
\begin{frame}[c,fragile]
|
|
|
89 |
\frametitle{How To calcululate 100 Mio Collatz Series?}
|
|
|
90 |
|
|
|
91 |
\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=1mm]
|
|
|
92 |
(1L to 100_000_000).map(collatz).max
|
|
|
93 |
\end{lstlisting}
|
|
|
94 |
|
|
|
95 |
\end{frame}
|
|
|
96 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
97 |
|
|
|
98 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
99 |
\begin{frame}[c,fragile]
|
|
|
100 |
\frametitle{Polyorphic Types}
|
|
|
101 |
|
|
|
102 |
To be avoided:\bigskip\bigskip
|
|
|
103 |
\small
|
|
|
104 |
|
|
|
105 |
\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-6mm]
|
|
|
106 |
def length_string_list(lst: List[String]): Int =
|
|
|
107 |
lst match {
|
|
|
108 |
case Nil => 0
|
|
|
109 |
case x::xs => 1 + length_string_list(xs)
|
|
|
110 |
}
|
|
240
|
111 |
|
|
|
112 |
|
|
327
|
113 |
def length_int_list(lst: List[Int]): Int =
|
|
|
114 |
lst match {
|
|
|
115 |
case Nil => 0
|
|
|
116 |
case x::xs => 1 + length_int_list(xs)
|
|
|
117 |
}
|
|
|
118 |
\end{lstlisting}
|
|
|
119 |
|
|
|
120 |
\end{frame}
|
|
|
121 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
122 |
|
|
|
123 |
|
|
|
124 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
125 |
\begin{frame}[c,fragile]
|
|
|
126 |
\frametitle{Polyorphic Types}
|
|
|
127 |
|
|
|
128 |
\small
|
|
|
129 |
|
|
|
130 |
\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-6mm]
|
|
|
131 |
def length[A](lst: List[A]): Int = lst match {
|
|
|
132 |
case Nil => 0
|
|
|
133 |
case x::xs => 1 + length(xs)
|
|
|
134 |
}
|
|
|
135 |
|
|
|
136 |
length(List("1", "2", "3", "4"))
|
|
|
137 |
length(List(1, 2, 3, 4))
|
|
|
138 |
|
|
|
139 |
|
|
|
140 |
def map[A, B](lst: List[A], f: A => B): List[B] =
|
|
|
141 |
lst match {
|
|
|
142 |
case Nil => Nil
|
|
|
143 |
case x::xs => f(x)::map(xs, f)
|
|
|
144 |
}
|
|
|
145 |
\end{lstlisting}
|
|
|
146 |
\end{frame}
|
|
240
|
147 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
148 |
|
|
|
149 |
|
|
|
150 |
|
|
239
|
151 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
327
|
152 |
\begin{frame}[c]
|
|
|
153 |
\frametitle{DFAs}
|
|
|
154 |
|
|
|
155 |
\begin{center}
|
|
|
156 |
\begin{tikzpicture}[>=stealth',very thick,auto,
|
|
|
157 |
every state/.style={minimum size=0pt,inner sep=2pt,
|
|
|
158 |
draw=blue!50,very thick,fill=blue!20},]
|
|
239
|
159 |
|
|
327
|
160 |
\only<1,3->{\node[state,initial] (Q_0) {$\mbox{Q}_0$};}
|
|
|
161 |
\only<2>{\node[state,initial,fill=red] (Q_0) {$\mbox{Q}_0$};}
|
|
|
162 |
\only<1,2,4->{\node[state] (Q_1) [right=of Q_0] {$\mbox{Q}_1$};}
|
|
|
163 |
\only<3>{\node[state,fill=red] (Q_1) [right=of Q_0] {$\mbox{Q}_1$};}
|
|
|
164 |
\only<-3,5->{\node[state] (Q_2) [below right=of Q_0] {$\mbox{Q}_2$};}
|
|
|
165 |
\only<4>{\node[state,fill=red] (Q_2) [below right=of Q_0] {$\mbox{Q}_2$};}
|
|
|
166 |
\only<-4,6->{\node[state] (Q_3) [right=of Q_2] {$\mbox{Q}_3$};}
|
|
|
167 |
\only<5>{\node[state,fill=red] (Q_3) [right=of Q_2] {$\mbox{Q}_3$};}
|
|
|
168 |
\only<-5>{\node[state, accepting] (Q_4) [right=of Q_1] {$\mbox{Q}_4$};}
|
|
|
169 |
\only<6->{\node[state, accepting,fill=red] (Q_4) [right=of Q_1] {$\mbox{Q}_4$};}
|
|
|
170 |
|
|
|
171 |
\path[->] (Q_0) edge node [above] {\alert{$a$}} (Q_1);
|
|
|
172 |
\path[->] (Q_1) edge node [above] {\alert{$a$}} (Q_4);
|
|
|
173 |
\path[->] (Q_4) edge [loop right] node {\alert{$a, b$}} ();
|
|
|
174 |
\path[->] (Q_3) edge node [right] {\alert{$a$}} (Q_4);
|
|
|
175 |
\path[->] (Q_2) edge node [above] {\alert{$a$}} (Q_3);
|
|
|
176 |
\path[->] (Q_1) edge node [right] {\alert{$b$}} (Q_2);
|
|
|
177 |
\path[->] (Q_0) edge node [above] {\alert{$b$}} (Q_2);
|
|
|
178 |
\path[->] (Q_2) edge [loop left] node {\alert{$b$}} ();
|
|
|
179 |
\path[->] (Q_3) edge [bend left=95, looseness=1.3] node [below] {\alert{$b$}} (Q_0);
|
|
|
180 |
\end{tikzpicture}
|
|
|
181 |
\end{center}
|
|
239
|
182 |
|
|
327
|
183 |
\begin{textblock}{9}(4,12)
|
|
|
184 |
\LARGE{}
|
|
|
185 |
\only<3->{\boldmath\alert{$a$}}%
|
|
|
186 |
\only<4->{\boldmath\alert{$b$}}%
|
|
|
187 |
\only<5->{\boldmath\alert{$a$}}%
|
|
|
188 |
\only<6->{\boldmath\alert{$a$}}%
|
|
|
189 |
\only<7->{\boldmath\alert{$a\quad\Rightarrow \textbf{yes}$}}%
|
|
|
190 |
\end{textblock}
|
|
|
191 |
|
|
|
192 |
\end{frame}
|
|
|
193 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
194 |
|
|
|
195 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
196 |
\begin{frame}[t]
|
|
|
197 |
\frametitle{DFAs}
|
|
239
|
198 |
|
|
327
|
199 |
A \alert{\bf deterministic finite automaton} (DFA) consists of
|
|
|
200 |
5 things:
|
|
239
|
201 |
|
|
327
|
202 |
\begin{itemize}
|
|
|
203 |
\item an alphabet \bl{$\varSigma$}
|
|
|
204 |
\item a set of states \bl{$\mbox{Qs}$}
|
|
|
205 |
\item one of these states is the start state \bl{$\mbox{Q}_0$}
|
|
|
206 |
\item some states are accepting states \bl{$F$}, and
|
|
|
207 |
\item there is transition function \bl{$\delta$}\bigskip
|
|
|
208 |
|
|
|
209 |
\small
|
|
|
210 |
which takes a state and a character as arguments and produces a
|
|
|
211 |
new state; this function might not be everywhere defined
|
|
|
212 |
\end{itemize}
|
|
|
213 |
|
|
|
214 |
\begin{center}
|
|
|
215 |
\bl{$A(\varSigma, \mbox{Qs}, \mbox{Q}_0, F, \delta)$}
|
|
|
216 |
\end{center}
|
|
239
|
217 |
|
|
|
218 |
\end{frame}
|
|
327
|
219 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
220 |
|
|
|
221 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
222 |
\begin{frame}[c]
|
|
|
223 |
\frametitle{NFAs}
|
|
239
|
224 |
|
|
327
|
225 |
\begin{center}
|
|
|
226 |
\begin{tikzpicture}[>=stealth',very thick, auto,
|
|
|
227 |
every state/.style={minimum size=0pt,inner sep=3pt,
|
|
|
228 |
draw=blue!50,very thick,fill=blue!20},scale=2]
|
|
|
229 |
\node[state,initial] (Q_0) {$\mbox{Q}_0$};
|
|
|
230 |
\node[state] (Q_1) [right=of Q_0] {$\mbox{Q}_1$};
|
|
|
231 |
\node[state, accepting] (Q_2) [right=of Q_1] {$\mbox{Q}_2$};
|
|
|
232 |
\path[->] (Q_0) edge [loop above] node {\alert{$b$}} ();
|
|
|
233 |
\path[<-] (Q_0) edge node [below] {\alert{$b$}} (Q_1);
|
|
|
234 |
\path[->] (Q_0) edge [bend left] node [above] {\alert{$a$}} (Q_1);
|
|
|
235 |
\path[->] (Q_0) edge [bend right=45,looseness=1.3] node [below] {\alert{$a$}} (Q_2);
|
|
|
236 |
\path[->] (Q_1) edge [loop above] node {\alert{$a,b$}} ();
|
|
|
237 |
\path[->] (Q_1) edge node [above] {\alert{$a$}} (Q_2);
|
|
|
238 |
\end{tikzpicture}
|
|
|
239 |
\end{center}
|
|
239
|
240 |
|
|
327
|
241 |
\end{frame}
|
|
|
242 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
239
|
243 |
|
|
|
244 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
327
|
245 |
\tikzstyle{sensor}=[draw, fill=blue!20, text width=3.8em, line width=1mm,
|
|
|
246 |
text centered, minimum height=2em,drop shadow]
|
|
|
247 |
\tikzstyle{ann} = [above, text width=4em, text centered]
|
|
|
248 |
\tikzstyle{sc} = [sensor, text width=7em, fill=red!20,
|
|
|
249 |
minimum height=6em, rounded corners, drop shadow,line width=1mm]
|
|
|
250 |
|
|
|
251 |
\begin{frame}[fragile,c]
|
|
|
252 |
\frametitle{Compilers 6CCS3CFL}
|
|
239
|
253 |
|
|
327
|
254 |
\begin{tikzpicture}
|
|
|
255 |
% Validation Layer is the same except that there are a set of nodes and links which are added
|
|
|
256 |
|
|
|
257 |
\path (0,0) node (IR) [sc] {\textbf{WHILE Language}\\ compiler};
|
|
|
258 |
\path (IR.west)+(-2.2,1.7) node (sou1) [sensor] {Fact};
|
|
|
259 |
\path (IR.west)+(-2.2,0.5) node (sou2)[sensor] {Fib};
|
|
|
260 |
\path (IR.west)+(-2.2,-0.7) node (sou4)[sensor] {Primes};
|
|
|
261 |
\only<2>{\path (IR.west)+(-2.2,-1.9) node (sou3)[sensor] {BrainF**k};}
|
|
239
|
262 |
|
|
327
|
263 |
\path [draw,->,line width=1mm] (sou1.east) -- node [above] {} (IR.160);
|
|
|
264 |
\path [draw,->,line width=1mm] (sou2.east) -- node [above] {} (IR.180);
|
|
|
265 |
\only<2>{\path [draw,->,line width=1mm] (sou3.east) -- node [above] {} (IR.200);}
|
|
|
266 |
\path [draw,->,line width=1mm] (sou4.east) -- node [above] {} (IR.190);
|
|
|
267 |
|
|
|
268 |
\path (IR.east)+(2.2, 0.8) node (tar2)[sensor] {JVM};
|
|
|
269 |
\path (IR.east)+(2.2,-0.8) node (tar3)[sensor] {LLVM{\small(x86)}};
|
|
239
|
270 |
|
|
327
|
271 |
\path [draw,<-,line width=1mm] (tar2.west) -- node [above] {} (IR.5);
|
|
|
272 |
\path [draw,<-,line width=1mm] (tar3.west) -- node [above] {} (IR.-5);
|
|
239
|
273 |
|
|
327
|
274 |
|
|
|
275 |
\end{tikzpicture}
|
|
239
|
276 |
\end{frame}
|
|
327
|
277 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
278 |
|
|
239
|
279 |
|
|
|
280 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
281 |
\begin{frame}[c]
|
|
|
282 |
\frametitle{Dijkstra on Testing}
|
|
|
283 |
|
|
|
284 |
\begin{bubble}[10cm]
|
|
|
285 |
``Program testing can be a very effective way to show the
|
|
|
286 |
presence of bugs, but it is hopelessly inadequate for showing
|
|
|
287 |
their absence.''
|
|
|
288 |
\end{bubble}\bigskip
|
|
|
289 |
|
|
|
290 |
|
|
|
291 |
\end{frame}
|
|
|
292 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
293 |
|
|
|
294 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
295 |
\begin{frame}[c]
|
|
|
296 |
\frametitle{\Large Proving Programs to be Correct}
|
|
|
297 |
|
|
|
298 |
\begin{bubble}[10cm]
|
|
|
299 |
\small
|
|
|
300 |
{\bf Theorem:} There are infinitely many prime
|
|
|
301 |
numbers.\medskip\\
|
|
|
302 |
|
|
|
303 |
{\bf Proof} \ldots\\
|
|
|
304 |
\end{bubble}\bigskip
|
|
|
305 |
|
|
|
306 |
|
|
|
307 |
similarly\bigskip
|
|
|
308 |
|
|
|
309 |
\begin{bubble}[10cm]
|
|
|
310 |
\small
|
|
|
311 |
{\bf Theorem:} The program is doing what
|
|
|
312 |
it is supposed to be doing.\medskip
|
|
|
313 |
|
|
|
314 |
{\bf Long, long proof} \ldots\\
|
|
|
315 |
\end{bubble}\bigskip\medskip
|
|
|
316 |
|
|
|
317 |
\small This can be a gigantic proof. The only hope is to have
|
|
|
318 |
help from the computer. `Program' is here to be understood to be
|
|
|
319 |
quite general (compiler, OS, \ldots).
|
|
|
320 |
|
|
|
321 |
\end{frame}
|
|
|
322 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
323 |
|
|
|
324 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
325 |
|
|
|
326 |
\begin{frame}[c]
|
|
|
327 |
\frametitle{Can This Be Done?}
|
|
|
328 |
|
|
|
329 |
\begin{itemize}
|
|
|
330 |
\item in 2011, verification of a small C-compiler (CompCert)
|
|
|
331 |
\begin{itemize}
|
|
|
332 |
\item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour''
|
|
|
333 |
\item is as good as \texttt{gcc -O1}, but much, much less buggy
|
|
|
334 |
\end{itemize}
|
|
|
335 |
\end{itemize}
|
|
|
336 |
|
|
|
337 |
\begin{center}
|
|
|
338 |
\includegraphics[scale=0.12]{../pics/compcert.png}
|
|
|
339 |
\end{center}
|
|
|
340 |
|
|
|
341 |
\end{frame}
|
|
|
342 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
343 |
|
|
265
|
344 |
%% ~2,237,800 lines of proof in 474
|
|
239
|
345 |
|
|
|
346 |
|
|
|
347 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
348 |
\begin{frame}[c]
|
|
|
349 |
\frametitle{Fuzzy Testing C-Compilers}
|
|
|
350 |
|
|
|
351 |
\begin{itemize}
|
|
|
352 |
\item tested GCC, LLVM and others by randomly generating
|
|
|
353 |
C-programs
|
|
|
354 |
\item found more than 300 bugs in GCC and also
|
|
|
355 |
many in LLVM (some of them highest-level critical)\bigskip
|
|
|
356 |
\item about CompCert:
|
|
|
357 |
|
|
|
358 |
\begin{bubble}[10cm]\small ``The striking thing about our CompCert
|
|
|
359 |
results is that the middle-end bugs we found in all other
|
|
|
360 |
compilers are absent. As of early 2011, the under-development
|
|
|
361 |
version of CompCert is the only compiler we have tested for
|
|
|
362 |
which Csmith cannot find wrong-code errors. This is not for
|
|
|
363 |
lack of trying: we have devoted about six CPU-years to the
|
|
|
364 |
task.''
|
|
|
365 |
\end{bubble}
|
|
|
366 |
\end{itemize}
|
|
|
367 |
|
|
|
368 |
\end{frame}
|
|
|
369 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
370 |
|
|
|
371 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
372 |
\begin{frame}[c]
|
|
|
373 |
\frametitle{seL4 / Isabelle}
|
|
|
374 |
|
|
|
375 |
\begin{itemize}
|
|
|
376 |
\item verified a microkernel operating system ($\approx$8000 lines of C code)\bigskip
|
|
|
377 |
\item US DoD has competitions to hack into drones; they found that the
|
|
|
378 |
isolation guarantees of seL4 hold up\bigskip
|
|
|
379 |
\item CompCert and seL4 sell their code
|
|
|
380 |
\end{itemize}
|
|
|
381 |
|
|
|
382 |
\only<2>{
|
|
|
383 |
\begin{textblock}{5}(5.5,1.9)
|
|
|
384 |
\includegraphics[scale=0.25]{../pics/drone.jpg}
|
|
|
385 |
\end{textblock}}
|
|
|
386 |
|
|
|
387 |
\end{frame}
|
|
|
388 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
389 |
|
|
|
390 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
391 |
|
|
|
392 |
\begin{frame}[c]
|
|
|
393 |
\frametitle{Where to go on from here?}
|
|
|
394 |
|
|
|
395 |
\begin{itemize}
|
|
|
396 |
\item Martin Odersky (EPFL)\ldots he is currently throwing out everything
|
|
327
|
397 |
and starts again with the dotty compiler for Scala 3.0\medskip
|
|
239
|
398 |
|
|
|
399 |
\item Elm (\url{http://elm-lang.org})\ldots web applications with style\medskip
|
|
|
400 |
|
|
|
401 |
\item Haskell, Ocaml, Standard ML, Scheme, \ldots
|
|
|
402 |
\end{itemize}
|
|
|
403 |
\end{frame}
|
|
|
404 |
|
|
|
405 |
|
|
|
406 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
407 |
|
|
|
408 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
409 |
\begin{frame}[c,fragile]
|
|
|
410 |
\frametitle{\alert{Questions?}}
|
|
|
411 |
|
|
|
412 |
{\tiny
|
|
|
413 |
\begin{verbatim}
|
|
|
414 |
*
|
|
|
415 |
* *
|
|
|
416 |
* *
|
|
|
417 |
* * * *
|
|
|
418 |
* *
|
|
|
419 |
* * * *
|
|
|
420 |
* * * *
|
|
|
421 |
* * * * * * * *
|
|
|
422 |
* *
|
|
|
423 |
* * * *
|
|
|
424 |
* * * *
|
|
|
425 |
* * * * * * * *
|
|
|
426 |
* * * *
|
|
|
427 |
* * * * * * * *
|
|
|
428 |
* * * * * * * *
|
|
|
429 |
* * * * * * * * * * * * * * * *
|
|
|
430 |
* *
|
|
|
431 |
* * * *
|
|
|
432 |
* * * *
|
|
|
433 |
* * * * * * * *
|
|
|
434 |
* * * *
|
|
|
435 |
* * * * * * * *
|
|
|
436 |
* * * * * * * *
|
|
|
437 |
* * * * * * * * * * * * * * * *
|
|
|
438 |
* * * *
|
|
|
439 |
* * * * * * * *
|
|
|
440 |
* * * * * * * *
|
|
|
441 |
* * * * * * * * * * * * * * * *
|
|
|
442 |
* * * * * * * *
|
|
|
443 |
* * * * * * * * * * * * * * * *
|
|
|
444 |
* * * * * * * * * * * * * * * *
|
|
|
445 |
* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
|
|
|
446 |
\end{verbatim}}
|
|
|
447 |
|
|
|
448 |
|
|
|
449 |
\begin{textblock}{6}(8.5,3.5)
|
|
|
450 |
\begin{bubble}[5cm]
|
|
|
451 |
\footnotesize
|
|
|
452 |
\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-1mm]
|
|
|
453 |
++++++++[>+>++++<<-]>++>>
|
|
|
454 |
+<[-[>>+<<-]+>>]>+[-<<<[-
|
|
|
455 |
>[+[-]+>++>>>-<<]<[<]>>++
|
|
|
456 |
++++[<<+++++>>-]+<<++.[-]
|
|
|
457 |
<<]>.>+[>>]>+]
|
|
|
458 |
\end{lstlisting}
|
|
|
459 |
\end{bubble}
|
|
|
460 |
\end{textblock}
|
|
|
461 |
|
|
|
462 |
\end{frame}
|
|
|
463 |
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
464 |
|
|
|
465 |
\end{document}
|
|
|
466 |
|
|
|
467 |
|
|
|
468 |
\end{document}
|
|
|
469 |
|
|
|
470 |
%%% Local Variables:
|
|
|
471 |
%%% mode: latex
|
|
|
472 |
%%% TeX-master: t
|
|
|
473 |
%%% End:
|
|
|
474 |
|