239
+ − 1
\documentclass[dvipsnames,14pt,t,xelatex]{beamer}
+ − 2
\usepackage{../slides}
+ − 3
\usepackage{../graphics}
+ − 4
\usepackage{../langs}
+ − 5
%%\usepackage{../data}
+ − 6
\usepackage[export]{adjustbox}
+ − 7
+ − 8
\hfuzz=220pt
+ − 9
+ − 10
%\setmonofont[Scale=.88]{Consolas}
+ − 11
%\newfontfamily{\consolas}{Consolas}
+ − 12
+ − 13
\lstset{language=Scala,
+ − 14
style=mystyle,
+ − 15
numbersep=0pt,
+ − 16
numbers=none,
+ − 17
xleftmargin=0mm}
+ − 18
+ − 19
\newcommand{\bl}[1]{\textcolor{blue}{#1}}
+ − 20
+ − 21
% beamer stuff
+ − 22
\renewcommand{\slidecaption}{PEP (Scala) 05, King's College London}
+ − 23
+ − 24
\begin{filecontents}{re3a.data}
+ − 25
1 0.00003
+ − 26
500001 0.22527
+ − 27
1000001 0.62752
+ − 28
1500001 0.88485
+ − 29
2000001 1.39815
+ − 30
2500001 1.68619
+ − 31
3000001 1.94957
+ − 32
3500001 2.15878
+ − 33
4000001 2.59918
+ − 34
4500001 5.90679
+ − 35
5000001 13.11295
+ − 36
5500001 19.15376
+ − 37
6000001 40.16373
+ − 38
\end{filecontents}
+ − 39
\begin{filecontents}{re-python2.data}
+ − 40
1 0.033
+ − 41
5 0.036
+ − 42
10 0.034
+ − 43
15 0.036
+ − 44
18 0.059
+ − 45
19 0.084
+ − 46
20 0.141
+ − 47
21 0.248
+ − 48
22 0.485
+ − 49
23 0.878
+ − 50
24 1.71
+ − 51
25 3.40
+ − 52
26 7.08
+ − 53
27 14.12
+ − 54
28 26.69
+ − 55
\end{filecontents}
+ − 56
+ − 57
\begin{filecontents}{re-java.data}
+ − 58
5 0.00298
+ − 59
10 0.00418
+ − 60
15 0.00996
+ − 61
16 0.01710
+ − 62
17 0.03492
+ − 63
18 0.03303
+ − 64
19 0.05084
+ − 65
20 0.10177
+ − 66
21 0.19960
+ − 67
22 0.41159
+ − 68
23 0.82234
+ − 69
24 1.70251
+ − 70
25 3.36112
+ − 71
26 6.63998
+ − 72
27 13.35120
+ − 73
28 29.81185
+ − 74
\end{filecontents}
+ − 75
+ − 76
%All O2 technical teams are working closely with one of our third party suppliers who has identified a global software issue in their system which has impacted data services.
+ − 77
+ − 78
+ − 79
\begin{document}
+ − 80
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 81
\begin{frame}[t]
+ − 82
\frametitle{%
+ − 83
\begin{tabular}{@ {}c@ {}}
+ − 84
\\[5mm]
+ − 85
\huge PEP Scala (5)
+ − 86
\end{tabular}}
+ − 87
+ − 88
\normalsize
+ − 89
\begin{center}
+ − 90
\begin{tabular}{ll}
+ − 91
Email: & christian.urban at kcl.ac.uk\\
+ − 92
Office: & N\liningnums{7.07} (North Wing, Bush House)\\
+ − 93
Slides \& Code: & KEATS\medskip\\
+ − 94
Office Hours: & Mondays 12:00 -- 14:00\\
+ − 95
\end{tabular}
+ − 96
\end{center}
+ − 97
+ − 98
+ − 99
\end{frame}
+ − 100
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 101
240
+ − 102
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 103
+ − 104
\begin{frame}[c]
+ − 105
\frametitle{Marks for CW7 (Part 1 + 2)}
+ − 106
+ − 107
Raw marks (234 submissions):
+ − 108
+ − 109
\begin{itemize}
+ − 110
\item 6\%: \hspace{4mm}192 students
+ − 111
\item 5\%: \hspace{4mm}16
+ − 112
\item 4\%: \hspace{4mm}7
+ − 113
\item 3\%: \hspace{4mm}2
+ − 114
\item 2\%: \hspace{4mm}6
+ − 115
\item 1\%: \hspace{4mm}1
+ − 116
\item 0\%: \hspace{4mm}9
+ − 117
\end{itemize}
+ − 118
\end{frame}
+ − 119
+ − 120
+ − 121
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 122
+ − 123
+ − 124
239
+ − 125
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 126
\begin{frame}[c,fragile]
+ − 127
\small
+ − 128
+ − 129
\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-7mm]
+ − 130
def get_csv_url(url: String) : List[String] = {
+ − 131
val csv = Try(Source.fromURL(url)).getOrElse(null)
+ − 132
if (csv == null){
+ − 133
List()
+ − 134
}
+ − 135
else {
+ − 136
....
+ − 137
}
+ − 138
}
+ − 139
\end{lstlisting}
+ − 140
+ − 141
\pause
+ − 142
\bigskip
+ − 143
\rule{11cm}{0.3mm}
+ − 144
\bigskip
+ − 145
+ − 146
\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-7mm]
+ − 147
def get_csv_url(url: String) : List[String] = {
+ − 148
Try(Source.fromURL(url)....).getOrElse(Nil)
+ − 149
\end{lstlisting}
+ − 150
+ − 151
+ − 152
\end{frame}
+ − 153
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 154
+ − 155
+ − 156
+ − 157
+ − 158
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 159
\begin{frame}[c,fragile]
+ − 160
\small
+ − 161
+ − 162
\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-7mm]
+ − 163
def get_csv_url(url: String) : List[String] = {
+ − 164
try {
+ − 165
val csvFile = Source.fromURL(url)
+ − 166
....
+ − 167
} catch {
+ − 168
case unknown : Throwable => List()
+ − 169
}
+ − 170
}
+ − 171
\end{lstlisting}
+ − 172
+ − 173
+ − 174
\bigskip
+ − 175
\rule{11cm}{0.3mm}
+ − 176
\bigskip
+ − 177
+ − 178
\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-7mm]
+ − 179
def get_csv_url(url: String) : List[String] = {
+ − 180
Try(Source.fromURL(url)....).getOrElse(Nil)
+ − 181
\end{lstlisting}
+ − 182
+ − 183
+ − 184
\end{frame}
+ − 185
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 186
+ − 187
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 188
\begin{frame}[c]
+ − 189
\frametitle{Dijkstra on Testing}
+ − 190
+ − 191
\begin{bubble}[10cm]
+ − 192
``Program testing can be a very effective way to show the
+ − 193
presence of bugs, but it is hopelessly inadequate for showing
+ − 194
their absence.''
+ − 195
\end{bubble}\bigskip
+ − 196
+ − 197
+ − 198
\end{frame}
+ − 199
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 200
+ − 201
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 202
\begin{frame}[c]
+ − 203
\frametitle{\Large Proving Programs to be Correct}
+ − 204
+ − 205
\begin{bubble}[10cm]
+ − 206
\small
+ − 207
{\bf Theorem:} There are infinitely many prime
+ − 208
numbers.\medskip\\
+ − 209
+ − 210
{\bf Proof} \ldots\\
+ − 211
\end{bubble}\bigskip
+ − 212
+ − 213
+ − 214
similarly\bigskip
+ − 215
+ − 216
\begin{bubble}[10cm]
+ − 217
\small
+ − 218
{\bf Theorem:} The program is doing what
+ − 219
it is supposed to be doing.\medskip
+ − 220
+ − 221
{\bf Long, long proof} \ldots\\
+ − 222
\end{bubble}\bigskip\medskip
+ − 223
+ − 224
\small This can be a gigantic proof. The only hope is to have
+ − 225
help from the computer. `Program' is here to be understood to be
+ − 226
quite general (compiler, OS, \ldots).
+ − 227
+ − 228
\end{frame}
+ − 229
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 230
+ − 231
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 232
+ − 233
\begin{frame}[c]
+ − 234
\frametitle{Can This Be Done?}
+ − 235
+ − 236
\begin{itemize}
+ − 237
\item in 2011, verification of a small C-compiler (CompCert)
+ − 238
\begin{itemize}
+ − 239
\item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour''
+ − 240
\item is as good as \texttt{gcc -O1}, but much, much less buggy
+ − 241
\end{itemize}
+ − 242
\end{itemize}
+ − 243
+ − 244
\begin{center}
+ − 245
\includegraphics[scale=0.12]{../pics/compcert.png}
+ − 246
\end{center}
+ − 247
+ − 248
\end{frame}
+ − 249
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 250
265
+ − 251
%% ~2,237,800 lines of proof in 474
239
+ − 252
+ − 253
+ − 254
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 255
\begin{frame}[c]
+ − 256
\frametitle{Fuzzy Testing C-Compilers}
+ − 257
+ − 258
\begin{itemize}
+ − 259
\item tested GCC, LLVM and others by randomly generating
+ − 260
C-programs
+ − 261
\item found more than 300 bugs in GCC and also
+ − 262
many in LLVM (some of them highest-level critical)\bigskip
+ − 263
\item about CompCert:
+ − 264
+ − 265
\begin{bubble}[10cm]\small ``The striking thing about our CompCert
+ − 266
results is that the middle-end bugs we found in all other
+ − 267
compilers are absent. As of early 2011, the under-development
+ − 268
version of CompCert is the only compiler we have tested for
+ − 269
which Csmith cannot find wrong-code errors. This is not for
+ − 270
lack of trying: we have devoted about six CPU-years to the
+ − 271
task.''
+ − 272
\end{bubble}
+ − 273
\end{itemize}
+ − 274
+ − 275
\end{frame}
+ − 276
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 277
+ − 278
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 279
\begin{frame}[c]
+ − 280
\frametitle{seL4 / Isabelle}
+ − 281
+ − 282
\begin{itemize}
+ − 283
\item verified a microkernel operating system ($\approx$8000 lines of C code)\bigskip
+ − 284
\item US DoD has competitions to hack into drones; they found that the
+ − 285
isolation guarantees of seL4 hold up\bigskip
+ − 286
\item CompCert and seL4 sell their code
+ − 287
\end{itemize}
+ − 288
+ − 289
\only<2>{
+ − 290
\begin{textblock}{5}(5.5,1.9)
+ − 291
\includegraphics[scale=0.25]{../pics/drone.jpg}
+ − 292
\end{textblock}}
+ − 293
+ − 294
\end{frame}
+ − 295
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 296
+ − 297
+ − 298
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 299
\begin{frame}[c]
+ − 300
\frametitle{CW9 : Regexes}
+ − 301
+ − 302
\begin{center}
+ − 303
Graphs: $(a^*)^* b$ and strings $\underbrace{\;a\ldots a\;}_{n}$\bigskip
+ − 304
+ − 305
\begin{tabular}[t]{@{\hspace{-8mm}}c@{\hspace{-4mm}}c@{}}
+ − 306
\raisebox{6mm}{\begin{tikzpicture}
+ − 307
\begin{axis}[
+ − 308
xlabel={$n$},
+ − 309
x label style={at={(1.05,0.0)}},
+ − 310
ylabel={time in secs},
+ − 311
enlargelimits=false,
+ − 312
xtick={0,5,...,30},
+ − 313
xmax=33,
+ − 314
ymax=35,
+ − 315
ytick={0,5,...,30},
+ − 316
scaled ticks=false,
+ − 317
axis lines=left,
+ − 318
width=5.5cm,
+ − 319
height=5cm,
+ − 320
legend entries={Python, Java 8},
+ − 321
legend pos=north west,
+ − 322
legend cell align=left]
+ − 323
\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};
+ − 324
\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};
+ − 325
\end{axis}
+ − 326
\end{tikzpicture}}
+ − 327
&
+ − 328
\onslide<1>{\begin{tikzpicture}
+ − 329
\begin{axis}[
+ − 330
xlabel={$n$},
+ − 331
x label style={at={(1.05,0.0)}},
+ − 332
ylabel={time in secs},
+ − 333
enlargelimits=false,
+ − 334
ymax=35,
+ − 335
ytick={0,5,...,30},
+ − 336
axis lines=left,
+ − 337
%%scaled ticks=false,
+ − 338
width=5.5cm,
+ − 339
height=5cm]
+ − 340
%%\addplot[green,mark=square*,mark options={fill=white}] table {re2a.data};
+ − 341
\addplot[red,mark=square*,mark options={fill=white}] table {re3a.data};
+ − 342
\end{axis}
+ − 343
\end{tikzpicture}}
+ − 344
\end{tabular}
+ − 345
\end{center}
+ − 346
+ − 347
+ − 348
\small
+ − 349
\hfill Kuklewicz: most POSIX matchers are buggy\\
+ − 350
\footnotesize
+ − 351
\hfill \url{http://www.haskell.org/haskellwiki/Regex_Posix}
+ − 352
\end{frame}
+ − 353
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 354
+ − 355
\begin{frame}[c]
+ − 356
\frametitle{Where to go on from here?}
+ − 357
+ − 358
\begin{itemize}
+ − 359
\item Martin Odersky (EPFL)\ldots he is currently throwing out everything
+ − 360
and starts again with the dotty compiler for Scala\medskip
+ − 361
+ − 362
\item Elm (\url{http://elm-lang.org})\ldots web applications with style\medskip
+ − 363
+ − 364
\item Haskell, Ocaml, Standard ML, Scheme, \ldots
+ − 365
\end{itemize}
+ − 366
\end{frame}
+ − 367
+ − 368
+ − 369
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 370
+ − 371
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 372
\begin{frame}[c,fragile]
+ − 373
\frametitle{\alert{Questions?}}
+ − 374
+ − 375
{\tiny
+ − 376
\begin{verbatim}
+ − 377
*
+ − 378
* *
+ − 379
* *
+ − 380
* * * *
+ − 381
* *
+ − 382
* * * *
+ − 383
* * * *
+ − 384
* * * * * * * *
+ − 385
* *
+ − 386
* * * *
+ − 387
* * * *
+ − 388
* * * * * * * *
+ − 389
* * * *
+ − 390
* * * * * * * *
+ − 391
* * * * * * * *
+ − 392
* * * * * * * * * * * * * * * *
+ − 393
* *
+ − 394
* * * *
+ − 395
* * * *
+ − 396
* * * * * * * *
+ − 397
* * * *
+ − 398
* * * * * * * *
+ − 399
* * * * * * * *
+ − 400
* * * * * * * * * * * * * * * *
+ − 401
* * * *
+ − 402
* * * * * * * *
+ − 403
* * * * * * * *
+ − 404
* * * * * * * * * * * * * * * *
+ − 405
* * * * * * * *
+ − 406
* * * * * * * * * * * * * * * *
+ − 407
* * * * * * * * * * * * * * * *
+ − 408
* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *
+ − 409
\end{verbatim}}
+ − 410
+ − 411
+ − 412
\begin{textblock}{6}(8.5,3.5)
+ − 413
\begin{bubble}[5cm]
+ − 414
\footnotesize
+ − 415
\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-1mm]
+ − 416
++++++++[>+>++++<<-]>++>>
+ − 417
+<[-[>>+<<-]+>>]>+[-<<<[-
+ − 418
>[+[-]+>++>>>-<<]<[<]>>++
+ − 419
++++[<<+++++>>-]+<<++.[-]
+ − 420
<<]>.>+[>>]>+]
+ − 421
\end{lstlisting}
+ − 422
\end{bubble}
+ − 423
\end{textblock}
+ − 424
+ − 425
\end{frame}
+ − 426
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 427
+ − 428
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 429
+ − 430
\begin{frame}[c]
+ − 431
\frametitle{Marks for CW6 (Part 1 + 2)}
+ − 432
+ − 433
Raw marks:
+ − 434
+ − 435
\begin{itemize}
+ − 436
\item 6\%: 154 students
+ − 437
\item 5\%: 66
+ − 438
\item 4\%: 18
+ − 439
\item 3\%: 13
+ − 440
\item 2\%: 2
+ − 441
\item 1\%: 1
+ − 442
\item 0\%: 21
+ − 443
\end{itemize}
+ − 444
\end{frame}
+ − 445
+ − 446
+ − 447
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 448
+ − 449
\end{document}
+ − 450
+ − 451
+ − 452
\end{document}
+ − 453
+ − 454
%%% Local Variables:
+ − 455
%%% mode: latex
+ − 456
%%% TeX-master: t
+ − 457
%%% End:
+ − 458