2459
+ − 1 (*<*)
+ − 2 theory Slides4
+ − 3 imports "LaTeXsugar" "Nominal"
+ − 4 begin
+ − 5
+ − 6 notation (latex output)
+ − 7 set ("_") and
+ − 8 Cons ("_::/_" [66,65] 65)
+ − 9
+ − 10 (*>*)
+ − 11
+ − 12 text_raw {*
+ − 13 \renewcommand{\slidecaption}{Nanjing, 31.~August 2010}
+ − 14
+ − 15 \newcommand{\abst}[2]{#1.#2}% atom-abstraction
+ − 16 \newcommand{\pair}[2]{\langle #1,#2\rangle} % pairing
+ − 17 \newcommand{\susp}{{\boldsymbol{\cdot}}}% for suspensions
+ − 18 \newcommand{\unit}{\langle\rangle}% unit
+ − 19 \newcommand{\app}[2]{#1\,#2}% application
+ − 20 \newcommand{\eqprob}{\mathrel{{\approx}?}}
+ − 21 \newcommand{\freshprob}{\mathrel{\#?}}
+ − 22 \newcommand{\redu}[1]{\stackrel{#1}{\Longrightarrow}}% reduction
+ − 23 \newcommand{\id}{\varepsilon}% identity substitution
+ − 24
+ − 25 \newcommand{\bl}[1]{\textcolor{blue}{#1}}
+ − 26 \newcommand{\gr}[1]{\textcolor{gray}{#1}}
+ − 27 \newcommand{\rd}[1]{\textcolor{red}{#1}}
+ − 28
+ − 29 \newcommand{\ok}{\includegraphics[scale=0.07]{ok.png}}
+ − 30 \newcommand{\notok}{\includegraphics[scale=0.07]{notok.png}}
+ − 31 \newcommand{\largenotok}{\includegraphics[scale=1]{notok.png}}
+ − 32
+ − 33 \renewcommand{\Huge}{\fontsize{61.92}{77}\selectfont}
+ − 34 \newcommand{\veryHuge}{\fontsize{74.3}{93}\selectfont}
+ − 35 \newcommand{\VeryHuge}{\fontsize{89.16}{112}\selectfont}
+ − 36 \newcommand{\VERYHuge}{\fontsize{107}{134}\selectfont}
+ − 37
+ − 38 \newcommand{\LL}{$\mathbb{L}\,$}
+ − 39
+ − 40
+ − 41 \pgfdeclareradialshading{smallbluesphere}{\pgfpoint{0.5mm}{0.5mm}}%
+ − 42 {rgb(0mm)=(0,0,0.9);
+ − 43 rgb(0.9mm)=(0,0,0.7);
+ − 44 rgb(1.3mm)=(0,0,0.5);
+ − 45 rgb(1.4mm)=(1,1,1)}
+ − 46
+ − 47 \def\myitemi{\begin{pgfpicture}{-1ex}{-0.55ex}{1ex}{1ex}
+ − 48 \usebeamercolor[fg]{subitem projected}
+ − 49 {\pgftransformscale{0.8}\pgftext{\normalsize\pgfuseshading{bigsphere}}}
+ − 50 \pgftext{%
+ − 51 \usebeamerfont*{subitem projected}}
+ − 52 \end{pgfpicture}}
+ − 53
+ − 54 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 55 \mode<presentation>{
+ − 56 \begin{frame}<1>[t]
+ − 57 \frametitle{%
+ − 58 \begin{tabular}{@ {\hspace{-3mm}}c@ {}}
+ − 59 \\
+ − 60 \huge Error-Free Programming\\[-1mm]
+ − 61 \huge with Theorem Provers\\[5mm]
+ − 62 \end{tabular}}
+ − 63 \begin{center}
+ − 64 Christian Urban
+ − 65 \end{center}
+ − 66 \begin{center}
+ − 67 \small Technical University of Munich, Germany\\[7mm]
+ − 68
+ − 69 \small in Nanjing on the kind invitation of\\ Professor Xingyuan Zhang
+ − 70 and his group
+ − 71 \end{center}
+ − 72 \end{frame}}
+ − 73 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 74
+ − 75 *}
+ − 76 text_raw {*
+ − 77 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 78 \mode<presentation>{
+ − 79 \begin{frame}<1->[c]
+ − 80 \frametitle{My Background}
+ − 81
+ − 82 \begin{itemize}
+ − 83 \item researcher in Theoretical Computer Science\medskip
+ − 84
+ − 85 \item programmer on a \alert<2->{software system} with 800 kloc (though I am
+ − 86 responsible only for 35 kloc)
+ − 87 \end{itemize}
+ − 88
+ − 89 \only<2->{
+ − 90 \begin{textblock}{6}(2,11)
+ − 91 \begin{tikzpicture}
+ − 92 \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ − 93 {\color{darkgray}
+ − 94 \begin{minipage}{4cm}\raggedright
+ − 95 A theorem prover called {\bf Isabelle}.
+ − 96 \end{minipage}};
+ − 97 \end{tikzpicture}
+ − 98 \end{textblock}}
+ − 99
+ − 100
+ − 101 \only<3>{
+ − 102 \begin{textblock}{6}(9,11)
+ − 103 \begin{tikzpicture}
+ − 104 \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ − 105 {\color{darkgray}
+ − 106 \begin{minipage}{4cm}\raggedright
+ − 107 Like every other code, this code is very hard to
+ − 108 get correct.
+ − 109 \end{minipage}};
+ − 110 \end{tikzpicture}
+ − 111 \end{textblock}}
+ − 112
+ − 113 \end{frame}}
+ − 114 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 115 *}
+ − 116
+ − 117 text_raw {*
+ − 118 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 119 \mode<presentation>{
+ − 120 \begin{frame}<1->[t]
+ − 121 \frametitle{Regular Expressions}
+ − 122
+ − 123 An example many (should) know about:\\
+ − 124 \rd{\bf Regular Expressions:}
+ − 125
+ − 126 \only<2>{
+ − 127 \begin{center}
+ − 128 \bl{[] $\;\;\;|\;\;\;$ c $\;\;\;|\;\;\;$ r$_1$$|$r$_2$ $\;\;\;|\;\;\;$
+ − 129 r$_1$$\cdot$r$_2$ $\;\;\;|\;\;\;$ r$^*$}
+ − 130 \end{center}}
+ − 131 \only<3->{
+ − 132 \begin{center}
+ − 133 \begin{tabular}{@ {}rrll@ {}}
+ − 134 \bl{r} & \bl{$::=$} & \bl{NULL} & \gr{(matches no string)}\\
+ − 135 & \bl{$\mid$} & \bl{EMPTY} & \gr{(matches the empty string, [])}\\
+ − 136 & \bl{$\mid$} & \bl{CHR c} & \gr{(matches the character c)}\\
+ − 137 & \bl{$\mid$} & \bl{ALT r$_1$ r$_2$} & \gr{(alternative, r$_1 |\,$r$_2$)}\\
+ − 138 & \bl{$\mid$} & \bl{SEQ r$_1$ r$_2$} & \gr{(sequential, r$_1\cdot\,$r$_2$)}\\
+ − 139 & \bl{$\mid$} & \bl{STAR r} & \gr{(repeat, r$^*$)}\\
+ − 140 \end{tabular}
+ − 141 \end{center}\medskip}
+ − 142
+ − 143 \small
+ − 144 \begin{textblock}{14.5}(1,12.5)
+ − 145 \only<2->{\gr{(a$\cdot$b)$^*$ \hspace{3mm}$\mapsto$\hspace{3mm} \{[], ab, abab, ababab, \ldots\}}\\}
+ − 146 \only<2->{\gr{x$\cdot$(0 $|$ 1 $|$ 2 \ldots 8 $|$ 9)$^*$ \hspace{3mm}$\mapsto$\hspace{3mm}
+ − 147 \{x, x0, x1, \ldots, x00, \ldots, x123, \ldots\}}}
+ − 148 \end{textblock}
+ − 149 \end{frame}}
+ − 150 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 151 *}
+ − 152
+ − 153 text_raw {*
+ − 154 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 155 \mode<presentation>{
+ − 156 \begin{frame}<1>[c]
+ − 157 \frametitle{RegExp Matcher}
+ − 158
+ − 159 Let's implement a regular expression matcher:\bigskip
+ − 160
+ − 161 \begin{center}
+ − 162 \begin{tikzpicture}
+ − 163 %%\draw[help lines, black] (-3,0) grid (6,3);
+ − 164
+ − 165 \draw[line width=1mm, red] (0.0,0.0) rectangle (4,2.3);
+ − 166 \node[anchor=base] at (2,1)
+ − 167 {\small\begin{tabular}{@ {}c@ {}}\Large\bf Regular\\
+ − 168 \Large\bf Expression \\
+ − 169 \Large\bf Matcher\end{tabular}};
+ − 170
+ − 171 \coordinate (m1) at (0,1.5);
+ − 172 \draw (-2,2) node (m2) {\small\begin{tabular}{c}\bl{regular}\\[-1mm] \bl{expression}\end{tabular}};
+ − 173 \path[overlay, ->, line width = 1mm, shorten <=-3mm] (m2) edge (m1);
+ − 174
+ − 175 \coordinate (s1) at (0,0.5);
+ − 176 \draw (-1.8,-0) node (s2) {\small\begin{tabular}{c}\bl{string}\end{tabular}};
+ − 177 \path[overlay, ->, line width = 1mm, shorten <=-3mm] (s2) edge (s1);
+ − 178
+ − 179 \coordinate (r1) at (4,1.2);
+ − 180 \draw (6,1.2) node (r2) {\small\begin{tabular}{c}\bl{true}, \bl{false}\end{tabular}};
+ − 181 \path[overlay, ->, line width = 1mm, shorten >=-3mm] (r1) edge (r2);
+ − 182
+ − 183 \end{tikzpicture}
+ − 184 \end{center}
+ − 185
+ − 186
+ − 187 \end{frame}}
+ − 188 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 189 *}
+ − 190
+ − 191 text_raw {*
+ − 192 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 193 \mode<presentation>{
+ − 194 \begin{frame}<1->[t]
+ − 195 \frametitle{RegExp Matcher}
+ − 196 \small
+ − 197
+ − 198 {\bf input:} a \underline{list} of RegExps and a string \hspace{6mm}{\bf output:} true or false
+ − 199
+ − 200 \only<2->{
+ − 201 \begin{center}
+ − 202 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
+ − 203 \bl{match [] []} & \bl{$=$} & \bl{true}\\
+ − 204 \bl{match [] \_} & \bl{$=$} & \bl{false}\\
+ − 205 \bl{match (NULL::rs) s} & \bl{$=$} & \bl{false}\\
+ − 206 \bl{match (EMPTY::rs) s} & \bl{$=$} & \bl{match rs s}\\
+ − 207 \bl{match (CHR c::rs) (c::s)} & \bl{$=$} & \bl{match rs s}\\
+ − 208 \bl{match (CHR c::rs) \_} & \bl{$=$} & \bl{false}\\
+ − 209 \bl{match (ALT r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s}\\
+ − 210 & & \bl{\;\;\;\;orelse match (r$_2$::rs) s}\\
+ − 211 \bl{match (SEQ r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s}\\
+ − 212 \bl{match (STAR r::rs) s} & \bl{$=$} & \bl{match rs s}\\
+ − 213 & & \bl{\;\;\;\;orelse match (r::STAR r::rs) s}\\
+ − 214 \end{tabular}
+ − 215 \end{center}}
+ − 216
+ − 217 \onslide<3->{we start the program with\\
+ − 218 \hspace{6mm}\bl{matches r s $=$ match [r] s}}
+ − 219
+ − 220 \end{frame}}
+ − 221 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 222 *}
+ − 223
+ − 224
+ − 225 text_raw {*
+ − 226 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 227 \mode<presentation>{
+ − 228 \begin{frame}<1>[c]
+ − 229 \frametitle{Program in Scala}
+ − 230
+ − 231 \bl{\footnotesize
+ − 232 \begin{tabular}{l}
+ − 233 sealed abstract class Rexp\\
+ − 234 sealed case class Null extends Rexp\\
+ − 235 sealed case class Empty extends Rexp\\
+ − 236 sealed case class Chr(c: Char) extends Rexp\\
+ − 237 sealed case class Alt(r1 : Rexp, r2 : Rexp) extends Rexp\\
+ − 238 sealed case class Seq(r1 : Rexp, r2 : Rexp) extends Rexp\\
+ − 239 sealed case class Star(r : Rexp) extends Rexp\medskip\\
+ − 240 def match1 (rs : List[Rexp], s : List[Char]) : Boolean = rs match \{\\
+ − 241 \hspace{3mm}case Nil @{text "\<Rightarrow>"} if (s == Nil) true else false\\
+ − 242 \hspace{3mm}case (Null()::rs) @{text "\<Rightarrow>"} false\\
+ − 243 \hspace{3mm}case (Empty()::rs) @{text "\<Rightarrow>"} match1 (rs, s)\\
+ − 244 \hspace{3mm}case (Chr(c)::rs) @{text "\<Rightarrow>"} s match \\
+ − 245 \hspace{6mm}\{ case Nil @{text "\<Rightarrow>"} false\\
+ − 246 \hspace{8mm}case (d::s) @{text "\<Rightarrow>"} if (c==d) match1 (rs,s) else false \}\\
+ − 247 \hspace{3mm}case (Alt (r1, r2)::rs) @{text "\<Rightarrow>"} match1 (r1::rs, s) || match1 (r2::rs, s)\\
+ − 248 \hspace{3mm}case (Seq (r1, r2)::rs) @{text "\<Rightarrow>"} match1 (r1::r2::rs, s) \\
+ − 249 \hspace{3mm}case (Star (r)::rs) @{text "\<Rightarrow>"} match1 (r::rs, s) || match1 (r::Star (r)::rs, s)\\
+ − 250 \}
+ − 251 \end{tabular}}
+ − 252
+ − 253 \end{frame}}
+ − 254 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 255 *}
+ − 256
+ − 257
+ − 258 text_raw {*
+ − 259 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 260 \mode<presentation>{
+ − 261 \begin{frame}<1->[c]
+ − 262 \frametitle{Testing}
+ − 263
+ − 264 \small
+ − 265 Every good programmer should do thourough tests:
+ − 266
+ − 267
+ − 268 \begin{center}
+ − 269 \begin{tabular}{@ {\hspace{-20mm}}lcl}
+ − 270 \bl{matches (a$\cdot$b)$^*\;$ []} & \bl{$\mapsto$} & \bl{true}\\
+ − 271 \bl{matches (a$\cdot$b)$^*\;$ ab} & \bl{$\mapsto$} & \bl{true}\\
+ − 272 \bl{matches (a$\cdot$b)$^*\;$ aba} & \bl{$\mapsto$} & \bl{false}\\
+ − 273 \bl{matches (a$\cdot$b)$^*\;$ abab} & \bl{$\mapsto$} & \bl{true}\\
+ − 274 \bl{matches (a$\cdot$b)$^*\;$ abaa} & \bl{$\mapsto$} & \bl{false}\medskip\\
+ − 275 \onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x} & \bl{$\mapsto$} & \bl{true}}\\
+ − 276 \onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x0} & \bl{$\mapsto$} & \bl{true}}\\
+ − 277 \onslide<2->{\bl{matches x$\cdot$(0$|$1)$^*\;$ x3} & \bl{$\mapsto$} & \bl{false}}
+ − 278 \end{tabular}
+ − 279 \end{center}
+ − 280
+ − 281 \onslide<3->
+ − 282 {looks OK \ldots let's ship it to customers\hspace{5mm}
+ − 283 \raisebox{-5mm}{\includegraphics[scale=0.05]{sun.png}}}
+ − 284
+ − 285 \end{frame}}
+ − 286 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 287 *}
+ − 288
+ − 289 text_raw {*
+ − 290 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 291 \mode<presentation>{
+ − 292 \begin{frame}<1->[t]
+ − 293 \frametitle{Testing}
+ − 294
+ − 295 \begin{itemize}
+ − 296 \item While testing is an important part in the process of programming development\pause
+ − 297
+ − 298 \item we can only test a {\bf finite} amount of examples\bigskip\pause
+ − 299
+ − 300 \begin{center}
+ − 301 \colorbox{cream}
+ − 302 {\gr{\begin{minipage}{10cm}
+ − 303 ``Testing can only show the presence of errors, never their
+ − 304 absence'' (Edsger W.~Dijkstra)
+ − 305 \end{minipage}}}
+ − 306 \end{center}\bigskip\pause
+ − 307
+ − 308 \item In a theorem prover we can establish properties that apply to
+ − 309 {\bf all} input and {\bf all} output.\pause
+ − 310
+ − 311 \item For example we can establish that the matcher terminates
+ − 312 on all input.
+ − 313 \end{itemize}
+ − 314
+ − 315 \end{frame}}
+ − 316 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 317 *}
+ − 318
+ − 319 text_raw {*
+ − 320 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 321 \mode<presentation>{
+ − 322 \begin{frame}<1->[t]
+ − 323 \frametitle{RegExp Matcher}
+ − 324
+ − 325 \small
+ − 326 We need to find a measure that gets smaller in each recursive call.\bigskip
+ − 327
+ − 328 \onslide<1->{
+ − 329 \begin{center}
+ − 330 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-9mm}}l@ {}}
+ − 331 \bl{match [] []} & \bl{$=$} & \bl{true} & \onslide<2->{\ok}\\
+ − 332 \bl{match [] \_} & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\
+ − 333 \bl{match (NULL::rs) s} & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\
+ − 334 \bl{match (EMPTY::rs) s} & \bl{$=$} & \bl{match rs s} & \onslide<3->{\ok}\\
+ − 335 \bl{match (CHR c::rs) (c::s)} & \bl{$=$} & \bl{match rs s} & \onslide<4->{\ok}\\
+ − 336 \bl{match (CHR c::rs) \_} & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\
+ − 337 \bl{match (ALT r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s} & \onslide<5->{\ok}\\
+ − 338 & & \bl{\;\;\;\;orelse match (r$_2$::rs) s}\\
+ − 339 \bl{match (SEQ r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s} & \onslide<6->{\ok}\\
+ − 340 \bl{match (STAR r::rs) s} & \bl{$=$} & \bl{match rs s} & \onslide<7->{\notok}\\
+ − 341 & & \bl{\;\;\;\;orelse match (r::STAR r::rs) s}\\
+ − 342 \end{tabular}
+ − 343 \end{center}}
+ − 344
+ − 345
+ − 346 \begin{textblock}{5}(4,4)
+ − 347 \begin{tikzpicture}
+ − 348 %%\draw[help lines, black] (-3,0) grid (6,3);
+ − 349
+ − 350 \coordinate (m1) at (-2,0);
+ − 351 \coordinate (m2) at ( 2,0);
+ − 352 \path[overlay, ->, line width = 0.6mm, color = red] (m1) edge (m2);
+ − 353 \draw (0,0) node[above=-1mm] {\footnotesize\rd{needs to get smaller}};
+ − 354 \end{tikzpicture}
+ − 355 \end{textblock}
+ − 356
+ − 357
+ − 358 \end{frame}}
+ − 359 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 360 *}
+ − 361
+ − 362 text_raw {*
+ − 363 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 364 \mode<presentation>{
+ − 365 \begin{frame}<1->[c]
+ − 366 \frametitle{Bug Hunting}
+ − 367
+ − 368 \only<1>{Several hours later\ldots}\pause
+ − 369
+ − 370
+ − 371 \begin{center}
+ − 372 \begin{tabular}{@ {\hspace{-20mm}}lcl}
+ − 373 \bl{matches (STAR (EMPTY)) s} & \bl{$\mapsto$} & loops\\
+ − 374 \onslide<4->{\bl{matches (STAR (EMPTY $|$ \ldots)) s} & \bl{$\mapsto$} & loops\\}
+ − 375 \end{tabular}
+ − 376 \end{center}
+ − 377
+ − 378 \small
+ − 379 \onslide<3->{
+ − 380 \begin{center}
+ − 381 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
+ − 382 \ldots\\
+ − 383 \bl{match (EMPTY::rs) s} & \bl{$=$} & \bl{match rs s}\\
+ − 384 \ldots\\
+ − 385 \bl{match (STAR r::rs) s} & \bl{$=$} & \bl{match rs s}\\
+ − 386 & & \bl{\;\;\;\;orelse match (r::STAR r::rs) s}\\
+ − 387 \end{tabular}
+ − 388 \end{center}}
+ − 389
+ − 390
+ − 391 \end{frame}}
+ − 392 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 393 *}
+ − 394
+ − 395 text_raw {*
+ − 396 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 397 \mode<presentation>{
+ − 398 \begin{frame}<1->[c]
+ − 399 \frametitle{RegExp Matcher}
+ − 400 \small
+ − 401
+ − 402 \begin{center}
+ − 403 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
+ − 404 \bl{match [] []} & \bl{$=$} & \bl{true}\\
+ − 405 \bl{match [] \_} & \bl{$=$} & \bl{false}\\
+ − 406 \bl{match (NULL::rs) s} & \bl{$=$} & \bl{false}\\
+ − 407 \bl{match (EMPTY::rs) s} & \bl{$=$} & \bl{match rs s}\\
+ − 408 \bl{match (CHR c::rs) (c::s)} & \bl{$=$} & \bl{match rs s}\\
+ − 409 \bl{match (CHR c::rs) \_} & \bl{$=$} & \bl{false}\\
+ − 410 \bl{match (ALT r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::rs) s}\\
+ − 411 & & \bl{\;\;\;\;orelse match (r$_2$::rs) s}\\
+ − 412 \bl{match (SEQ r$_1$ r$_2$::rs) s} & \bl{$=$} & \bl{match (r$_1$::r$_2$::rs) s}\\
+ − 413 \bl{match (STAR r::rs) s} & \bl{$=$} & \bl{match rs s}\\
+ − 414 & & \bl{\;\;\;\;orelse match (r::STAR r::rs) s}\\
+ − 415 \end{tabular}
+ − 416 \end{center}
+ − 417
+ − 418 \only<1>{
+ − 419 \begin{textblock}{5}(4,4)
+ − 420 \largenotok
+ − 421 \end{textblock}}
+ − 422
+ − 423 \end{frame}}
+ − 424 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 425 *}
+ − 426
+ − 427
+ − 428
+ − 429 text_raw {*
+ − 430 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 431 \mode<presentation>{
+ − 432 \begin{frame}<1->[t]
+ − 433 \frametitle{Second Attempt}
+ − 434
+ − 435 Can a regular expression match the empty string?
+ − 436
+ − 437 \small
+ − 438 \begin{center}
+ − 439 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}
+ − 440 \bl{nullable (NULL)} & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\
+ − 441 \bl{nullable (EMPTY)} & \bl{$=$} & \bl{true} & \onslide<2->{\ok}\\
+ − 442 \bl{nullable (CHR c)} & \bl{$=$} & \bl{false} & \onslide<2->{\ok}\\
+ − 443 \bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) orelse (nullable r$_2$)}
+ − 444 & \onslide<2->{\ok}\\
+ − 445 \bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) andalso (nullable r$_2$)}
+ − 446 & \onslide<2->{\ok}\\
+ − 447 \bl{nullable (STAR r)} & \bl{$=$} & \bl{true} & \onslide<2->{\ok}\\
+ − 448 \end{tabular}
+ − 449 \end{center}
+ − 450
+ − 451 \end{frame}}
+ − 452 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 453 *}
+ − 454
+ − 455
+ − 456 text_raw {*
+ − 457 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 458 \mode<presentation>{
+ − 459 \begin{frame}<1->[t]
+ − 460 \frametitle{RegExp Matcher 2}
+ − 461
+ − 462 If \bl{r} matches \bl{c::s}, which regular expression can match the string \bl{s}?
+ − 463
+ − 464 \small
+ − 465 \begin{center}
+ − 466 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
+ − 467 \bl{der c (NULL)} & \bl{$=$} & \bl{NULL} & \onslide<3->{\ok}\\
+ − 468 \bl{der c (EMPTY)} & \bl{$=$} & \bl{NULL} & \onslide<3->{\ok}\\
+ − 469 \bl{der c (CHR d)} & \bl{$=$} & \bl{if c=d then EMPTY else NULL} & \onslide<3->{\ok}\\
+ − 470 \bl{der c (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (der c r$_1$) (der c r$_2$)} & \onslide<3->{\ok}\\
+ − 471 \bl{der c (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (SEQ (der c r$_1$) r$_2$)} & \onslide<3->{\ok}\\
+ − 472 & & \bl{\phantom{ALT} (if nullable r$_1$ then der c r$_2$ else NULL)}\\
+ − 473 \bl{der c (STAR r)} & \bl{$=$} & \bl{SEQ (der c r) (STAR r)} & \onslide<3->{\ok}\medskip\\
+ − 474 \pause
+ − 475
+ − 476 \bl{derivative r []} & \bl{$=$} & \bl{r} & \onslide<3->{\ok}\\
+ − 477 \bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \onslide<3->{\ok}\\
+ − 478 \end{tabular}
+ − 479 \end{center}
+ − 480
+ − 481 we call the program with\\
+ − 482 \bl{matches r s $=$ nullable (derivative r s)}
+ − 483
+ − 484
+ − 485 \end{frame}}
+ − 486 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 487 *}
+ − 488
+ − 489 text_raw {*
+ − 490 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 491 \mode<presentation>{
+ − 492 \begin{frame}<1->[c]
+ − 493 \frametitle{But Now What?}
+ − 494
+ − 495 \begin{center}
+ − 496 {\usefont{T1}{ptm}{b}{N}\VERYHuge{\rd{?}}}
+ − 497 \end{center}
+ − 498
+ − 499 \end{frame}}
+ − 500 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 501 *}
+ − 502
+ − 503 text_raw {*
+ − 504 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 505 \mode<presentation>{
+ − 506 \begin{frame}<1->[c]
+ − 507 \frametitle{Testing}
+ − 508
+ − 509 \small
+ − 510
+ − 511 \begin{center}
+ − 512 \begin{tabular}{@ {\hspace{-20mm}}lcl}
+ − 513 \bl{matches []$^*$ []} & \bl{$\mapsto$} & \bl{true}\\
+ − 514 \bl{matches ([]$|$a)$^*$ a} & \bl{$\mapsto$} & \bl{true}\medskip\\
+ − 515
+ − 516 \bl{matches (a$\cdot$b)$^*\;$ []} & \bl{$\mapsto$} & \bl{true}\\
+ − 517 \bl{matches (a$\cdot$b)$^*\;$ ab} & \bl{$\mapsto$} & \bl{true}\\
+ − 518 \bl{matches (a$\cdot$b)$^*\;$ aba} & \bl{$\mapsto$} & \bl{false}\\
+ − 519 \bl{matches (a$\cdot$b)$^*\;$ abab} & \bl{$\mapsto$} & \bl{true}\\
+ − 520 \bl{matches (a$\cdot$b)$^*\;$ abaa} & \bl{$\mapsto$} & \bl{false}\medskip\\
+ − 521
+ − 522 \bl{matches x$\cdot$(0$|$1)$^*\;$ x} & \bl{$\mapsto$} & \bl{true}\\
+ − 523 \bl{matches x$\cdot$(0$|$1)$^*\;$ x0} & \bl{$\mapsto$} & \bl{true}\\
+ − 524 \bl{matches x$\cdot$(0$|$1)$^*\;$ x3} & \bl{$\mapsto$} & \bl{false}
+ − 525 \end{tabular}
+ − 526 \end{center}
+ − 527
+ − 528
+ − 529 \end{frame}}
+ − 530 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 531 *}
+ − 532
+ − 533 text_raw {*
+ − 534 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 535 \mode<presentation>{
+ − 536 \begin{frame}<1->[t]
+ − 537 \frametitle{Specification}
+ − 538
+ − 539 We have to specify what it means for a regular expression to match
+ − 540 a string.
+ − 541 %
+ − 542 \only<2>{
+ − 543 \mbox{}\\[8mm]
+ − 544 \bl{(a$\cdot$b)$^*$}\\
+ − 545 \hspace{7mm}\bl{$\mapsto$\hspace{3mm}\{[], ab, abab, ababab, \ldots\}}\bigskip\\
+ − 546 \bl{x$\cdot$(0 $|$ 1 $|$ 2 \ldots 8 $|$ 9 )$^*$}\\
+ − 547 \hspace{7mm}\bl{$\mapsto$\hspace{3mm}
+ − 548 \{x, x0, x1, \ldots, x00, \ldots, x123, \ldots\}}}
+ − 549 %
+ − 550 \only<3->{
+ − 551 \begin{center}
+ − 552 \begin{tabular}{rcl}
+ − 553 \bl{\LL (NULL)} & \bl{$\dn$} & \bl{\{\}}\\
+ − 554 \bl{\LL (EMPTY)} & \bl{$\dn$} & \bl{\{[]\}}\\
+ − 555 \bl{\LL (CHR c)} & \bl{$\dn$} & \bl{\{c\}}\\
+ − 556 \bl{\LL (ALT r$_1$ r$_2$)} & \bl{$\dn$} & \onslide<4->{\bl{\LL (r$_1$) $\cup$ \LL (r$_2$)}}\\
+ − 557 \bl{\LL (SEQ r$_1$ r$_2$)} & \bl{$\dn$} & \onslide<6->{\bl{\LL (r$_1$) ; \LL (r$_2$)}}\\
+ − 558 \bl{\LL (STAR r)} & \bl{$\dn$} & \onslide<8->{\bl{(\LL (r))$^\star$}}\\
+ − 559 \end{tabular}
+ − 560 \end{center}}
+ − 561
+ − 562 \only<5-6>{
+ − 563 \begin{textblock}{6}(2.9,13.3)
+ − 564 \colorbox{cream}{\bl{S$_1$ ; S$_2$ $\;\dn\;$ \{ s$_1$@s$_2$ $|$ s$_1$$\in$S$_1$ $\wedge$
+ − 565 s$_2$$\in$S$_2$ \}}}
+ − 566 \end{textblock}}
+ − 567
+ − 568 \only<7->{
+ − 569 \begin{textblock}{9}(4,13)
+ − 570 \colorbox{cream}{\bl{$\infer{\mbox{[]} \in \mbox{S}^\star}{}$}}\hspace{3mm}
+ − 571 \colorbox{cream}{\bl{$\infer{\mbox{s}_1\mbox{@}\mbox{s}_2 \in \mbox{S}^\star}
+ − 572 {\mbox{s}_1 \in \mbox{S} & \mbox{s}_2 \in \mbox{S}^\star}$}}
+ − 573 \end{textblock}}
+ − 574
+ − 575 \end{frame}}
+ − 576 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 577 *}
+ − 578
+ − 579 text_raw {*
+ − 580 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 581 \mode<presentation>{
+ − 582 \begin{frame}<1->[t]
+ − 583 \frametitle{Is the Matcher Error-Free?}
+ − 584
+ − 585 We expect that
+ − 586
+ − 587 \begin{center}
+ − 588 \begin{tabular}{lcl}
+ − 589 \bl{matches r s = true} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}%
+ − 590 \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\in$ \LL(r)}\\
+ − 591 \bl{matches r s = false} & \only<1>{\rd{$\Longrightarrow\,\,$}}\only<2>{\rd{$\Longleftarrow\,\,$}}%
+ − 592 \only<3->{\rd{$\Longleftrightarrow$}} & \bl{s $\notin$ \LL(r)}\\
+ − 593 \end{tabular}
+ − 594 \end{center}
+ − 595 \pause\pause\bigskip
+ − 596 By \alert<4->{induction}, we can {\bf prove} these properties.\bigskip
+ − 597
+ − 598 \begin{tabular}{lrcl}
+ − 599 Lemmas: & \bl{nullable (r)} & \bl{$\Longleftrightarrow$} & \bl{[] $\in$ \LL (r)}\\
+ − 600 & \bl{s $\in$ \LL (der c r)} & \bl{$\Longleftrightarrow$} & \bl{(c::s) $\in$ \LL (r)}\\
+ − 601 \end{tabular}
+ − 602
+ − 603 \only<4->{
+ − 604 \begin{textblock}{3}(0.9,4.5)
+ − 605 \rd{\huge$\forall$\large{}r s.}
+ − 606 \end{textblock}}
+ − 607 \end{frame}}
+ − 608 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 609 *}
+ − 610
+ − 611 text_raw {*
+ − 612 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 613 \mode<presentation>{
+ − 614 \begin{frame}<1->[t]
+ − 615
+ − 616 \mbox{}\\[-2mm]
+ − 617
+ − 618 \small
+ − 619 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}
+ − 620 \bl{nullable (NULL)} & \bl{$=$} & \bl{false} &\\
+ − 621 \bl{nullable (EMPTY)} & \bl{$=$} & \bl{true} &\\
+ − 622 \bl{nullable (CHR c)} & \bl{$=$} & \bl{false} &\\
+ − 623 \bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) orelse (nullable r$_2$)} & \\
+ − 624 \bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) andalso (nullable r$_2$)} & \\
+ − 625 \bl{nullable (STAR r)} & \bl{$=$} & \bl{true} & \\
+ − 626 \end{tabular}\medskip
+ − 627
+ − 628 \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
+ − 629 \bl{der c (NULL)} & \bl{$=$} & \bl{NULL} & \\
+ − 630 \bl{der c (EMPTY)} & \bl{$=$} & \bl{NULL} & \\
+ − 631 \bl{der c (CHR d)} & \bl{$=$} & \bl{if c=d then EMPTY else NULL} & \\
+ − 632 \bl{der c (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (der c r$_1$) (der c r$_2$)} & \\
+ − 633 \bl{der c (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (SEQ (der c r$_1$) r$_2$)} & \\
+ − 634 & & \bl{\phantom{ALT} (if nullable r$_1$ then der c r$_2$ else NULL)}\\
+ − 635 \bl{der c (STAR r)} & \bl{$=$} & \bl{SEQ (der c r) (STAR r)} &\smallskip\\
+ − 636
+ − 637 \bl{derivative r []} & \bl{$=$} & \bl{r} & \\
+ − 638 \bl{derivative r (c::s)} & \bl{$=$} & \bl{derivative (der c r) s} & \\
+ − 639 \end{tabular}\medskip
+ − 640
+ − 641 \bl{matches r s $=$ nullable (derivative r s)}
+ − 642
+ − 643 \only<2>{
+ − 644 \begin{textblock}{8}(1.5,4)
+ − 645 \includegraphics[scale=0.3]{approved.png}
+ − 646 \end{textblock}}
+ − 647
+ − 648
+ − 649 \end{frame}}
+ − 650 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 651 *}
+ − 652
+ − 653
+ − 654 text_raw {*
+ − 655 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 656 \mode<presentation>{
+ − 657 \begin{frame}<1->[c]
+ − 658 \frametitle{Interlude: TCB}
+ − 659
+ − 660 \begin{itemize}
+ − 661 \item The \alert{\bf Trusted Code Base} (TCB) is the code that can make your
+ − 662 program behave in unintended ways (i.e.~cause bugs).\medskip
+ − 663
+ − 664 \item Typically the TCB includes: CPUs, operating systems, C-libraries,
+ − 665 device drivers, (J)VMs\ldots\bigskip
+ − 666 \pause
+ − 667
+ − 668 \item It also includes the compiler.
+ − 669 \end{itemize}
+ − 670
+ − 671 \end{frame}}
+ − 672 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 673 *}
+ − 674
+ − 675 text_raw {*
+ − 676
+ − 677 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 678 \mode<presentation>{
+ − 679 \begin{frame}<1-3>
+ − 680 \frametitle{\LARGE\begin{tabular}{c}Hacking Compilers
+ − 681 \end{tabular}}
+ − 682
+ − 683 %Why is it so paramount to have a small trusted code base (TCB)?
+ − 684 \bigskip\bigskip
+ − 685
+ − 686 \begin{columns}
+ − 687 \begin{column}{2.7cm}
+ − 688 \begin{minipage}{2.5cm}%
+ − 689 \begin{tabular}{c@ {}}
+ − 690 \includegraphics[scale=0.2]{ken-thompson.jpg}\\[-1.8mm]
+ − 691 \footnotesize Ken Thompson\\[-1.8mm]
+ − 692 \footnotesize Turing Award, 1983\\
+ − 693 \end{tabular}
+ − 694 \end{minipage}
+ − 695 \end{column}
+ − 696 \begin{column}{9cm}
+ − 697 \begin{tabular}{l@ {\hspace{1mm}}p{8cm}}
+ − 698 \myitemi
+ − 699 & Ken Thompson showed how to hide a Trojan Horse in a
+ − 700 compiler \textcolor{red}{without} leaving any traces in the source code.\\[2mm]
+ − 701 \myitemi
+ − 702 & No amount of source level verification will protect
+ − 703 you from such Thompson-hacks.\\[2mm]
+ − 704
+ − 705 \myitemi
+ − 706 & Therefore in safety-critical systems it is important to rely
+ − 707 on only a very small TCB.
+ − 708 \end{tabular}
+ − 709 \end{column}
+ − 710 \end{columns}
+ − 711
+ − 712 \only<2>{
+ − 713 \begin{textblock}{6}(4,2)
+ − 714 \begin{tikzpicture}
+ − 715 \draw (0,0) node[inner sep=3mm,fill=cream, ultra thick, draw=red, rounded corners=2mm]
+ − 716 {\normalsize
+ − 717 \begin{minipage}{8cm}
+ − 718 \begin{quote}
+ − 719 \includegraphics[scale=0.05]{evil.png}
+ − 720 \begin{enumerate}
+ − 721 \item[1)] Assume you ship the compiler as binary and also with sources.
+ − 722 \item[2)] Make the compiler aware when it compiles itself.
+ − 723 \item[3)] Add the Trojan horse.
+ − 724 \item[4)] Compile.
+ − 725 \item[5)] Delete Trojan horse from the sources of the compiler.
+ − 726 \item[6)] Go on holiday for the rest of your life. ;o)\\[-7mm]\mbox{}
+ − 727 \end{enumerate}
+ − 728 \end{quote}
+ − 729 \end{minipage}};
+ − 730 \end{tikzpicture}
+ − 731 \end{textblock}}
+ − 732
+ − 733 \end{frame}}
+ − 734 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 735
+ − 736 *}
+ − 737
+ − 738 text_raw {*
+ − 739 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 740 \mode<presentation>{
+ − 741 \begin{frame}
+ − 742 \frametitle{\LARGE\begin{tabular}{c}An Example: Small TCB for\\[-2mm]
+ − 743 A Critical Infrastructure\end{tabular}}
+ − 744 \mbox{}\\[-14mm]\mbox{}
+ − 745
+ − 746 \begin{columns}
+ − 747 \begin{column}{0.2\textwidth}
+ − 748 \begin{tabular}{@ {} c@ {}}
+ − 749 \includegraphics[scale=0.3]{appel.jpg}\\[-2mm]
+ − 750 {\footnotesize Andrew Appel}\\[-2.5mm]
+ − 751 {\footnotesize (Princeton)}
+ − 752 \end{tabular}
+ − 753 \end{column}
+ − 754
+ − 755 \begin{column}{0.8\textwidth}
+ − 756 \begin{textblock}{10}(4.5,3.95)
+ − 757 \begin{block}{Proof-Carrying Code}
+ − 758 \begin{center}
+ − 759 \begin{tikzpicture}
+ − 760 \draw[help lines,cream] (0,0.2) grid (8,4);
+ − 761
+ − 762 \draw[line width=1mm, red] (5.5,0.6) rectangle (7.5,4);
+ − 763 \node[anchor=base] at (6.5,2.8)
+ − 764 {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering user needs to run untrusted code\end{tabular}};
+ − 765
+ − 766 \draw[line width=1mm, red] (0.5,0.6) rectangle (2.5,4);
+ − 767 \node[anchor=base] at (1.5,2.3)
+ − 768 {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\centering code developer/ web server/ Apple
+ − 769 Store\end{tabular}};
+ − 770
+ − 771 \onslide<4->{
+ − 772 \draw[line width=1mm, red, fill=red] (5.5,0.6) rectangle (7.5,1.8);
+ − 773 \node[anchor=base,white] at (6.5,1.1)
+ − 774 {\small\begin{tabular}{@ {}p{1.9cm}@ {}}\bf\centering proof- checker\end{tabular}};}
+ − 775
+ − 776 \node at (3.8,3.0) [single arrow, fill=red,text=white, minimum height=3cm]{\bf code};
+ − 777 \onslide<3->{
+ − 778 \node at (3.8,1.3) [single arrow, fill=red,text=white, minimum height=3cm]{\bf LF proof};
+ − 779 \node at (3.8,1.9) {\small certificate};
+ − 780 }
+ − 781
+ − 782 \onslide<2>{\node at (4.0,1.3) [text=red]{\begin{tabular}{c}\bf Highly\\\bf Dangerous!\end{tabular}};}
+ − 783 % Code Developer
+ − 784 % User (runs untrusted code)
+ − 785 % transmits a proof that the code is safe
+ − 786 %
+ − 787 \end{tikzpicture}
+ − 788 \end{center}
+ − 789 \end{block}
+ − 790 \end{textblock}
+ − 791 \end{column}
+ − 792 \end{columns}
+ − 793
+ − 794 \small\mbox{}\\[2.5cm]
+ − 795 \begin{itemize}
+ − 796 \item<4-> TCB of the checker is $\sim$2700 lines of code (1865 loc of\\ LF definitions;
+ − 797 803 loc in C including 2 library functions)\\[-3mm]
+ − 798 \item<5-> 167 loc in C implement a type-checker
+ − 799 \end{itemize}
+ − 800
+ − 801 \end{frame}}
+ − 802 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 803
+ − 804 *}
+ − 805
+ − 806
+ − 807
+ − 808 text {*
+ − 809 \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
+ − 810 \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick,
+ − 811 draw=black!50, top color=white, bottom color=black!20]
+ − 812 \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick,
+ − 813 draw=red!70, top color=white, bottom color=red!50!black!20]
+ − 814 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 815 \mode<presentation>{
+ − 816 \begin{frame}[squeeze]
+ − 817 \frametitle{Type-Checking in LF}
+ − 818
+ − 819 \begin{columns}
+ − 820 \begin{column}{0.2\textwidth}
+ − 821 \begin{tabular}{@ {\hspace{-4mm}}c@ {}}
+ − 822 \\[-4mm]
+ − 823 \includegraphics[scale=0.1]{harper.jpg}\\[-2mm]
+ − 824 {\footnotesize Bob Harper}\\[-2.5mm]
+ − 825 {\footnotesize (CMU)}\\[2mm]
+ − 826
+ − 827 \includegraphics[scale=0.3]{pfenning.jpg}\\[-2mm]
+ − 828 {\footnotesize Frank Pfenning}\\[-2.5mm]
+ − 829 {\footnotesize (CMU)}\\[2mm]
+ − 830
+ − 831 \onslide<-6>{
+ − 832 {\footnotesize 31 pages in }\\[-2.5mm]
+ − 833 {\footnotesize ACM Transact.~on}\\[-2.5mm]
+ − 834 {\footnotesize Comp.~Logic.,~2005}\\}
+ − 835 \end{tabular}
+ − 836 \end{column}
+ − 837
+ − 838 \begin{column}{0.8\textwidth}
+ − 839 \begin{textblock}{0}(3.1,2)
+ − 840
+ − 841 \begin{tikzpicture}
+ − 842 \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]
+ − 843 { \&[-10mm]
+ − 844 \node (def1) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&
+ − 845 \node (proof1) [node1] {\large Proof}; \&
+ − 846 \node (alg1) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\
+ − 847
+ − 848 \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+ − 849 \onslide<4->{\node (def2) [node2] {\large Spec$^\text{+ex}$};} \&
+ − 850 \onslide<4->{\node (proof2) [node1] {\large Proof};} \&
+ − 851 \onslide<4->{\node (alg2) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
+ − 852
+ − 853 \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+ − 854 \onslide<5->{\node (def3) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
+ − 855 \onslide<5->{\node (proof3) [node1] {\large Proof};} \&
+ − 856 \onslide<5->{\node (alg3) [node2] {\large Alg$^\text{-ex}$};} \\
+ − 857
+ − 858 \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+ − 859 \onslide<6->{\node (def4) [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
+ − 860 \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&
+ − 861 \onslide<6->{\node (alg4) [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
+ − 862 };
+ − 863
+ − 864 \draw[->,black!50,line width=2mm] (proof1) -- (def1);
+ − 865 \draw[->,black!50,line width=2mm] (proof1) -- (alg1);
+ − 866
+ − 867 \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}
+ − 868 \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}
+ − 869
+ − 870 \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}
+ − 871 \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}
+ − 872
+ − 873 \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}
+ − 874 \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}
+ − 875
+ − 876 \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);}
+ − 877 \end{tikzpicture}
+ − 878
+ − 879 \end{textblock}
+ − 880 \end{column}
+ − 881 \end{columns}
+ − 882
+ − 883 \only<2>{%
+ − 884 \begin{textblock}{2}(.1,12.85)
+ − 885 \begin{tikzpicture}
+ − 886 \draw[line width=1mm, red] (0,0) ellipse (1.5cm and 0.88cm);
+ − 887 \end{tikzpicture}
+ − 888 \end{textblock}
+ − 889 }
+ − 890
+ − 891 \begin{textblock}{3}(14,3.6)
+ − 892 \onslide<4->{
+ − 893 \begin{tikzpicture}
+ − 894 \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
+ − 895 \end{tikzpicture}}
+ − 896 \end{textblock}
+ − 897
+ − 898 \only<7->{
+ − 899 \begin{textblock}{14}(0.6,12.8)
+ − 900 \begin{block}{}
+ − 901 \small Each time one needs to check $\sim$31pp~of informal paper proofs.
+ − 902 You have to be able to keep definitions and proofs consistent.
+ − 903 \end{block}
+ − 904 \end{textblock}}
+ − 905
+ − 906 \end{frame}}
+ − 907 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 908
+ − 909 *}
+ − 910
+ − 911 text_raw {*
+ − 912 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 913 \mode<presentation>{
+ − 914 \begin{frame}<1>[c]
+ − 915 \frametitle{Theorem Provers}
+ − 916
+ − 917 \begin{itemize}
+ − 918 \item Theorem provers help with keeping large proofs consistent;
+ − 919 make them modifiable.\medskip
+ − 920
+ − 921 \item They can ensure that all cases are covered.\medskip
+ − 922
+ − 923 \item Sometimes, tedious reasoning can be automated.
+ − 924 \end{itemize}
+ − 925
+ − 926 \end{frame}}
+ − 927 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 928 *}
+ − 929
+ − 930 text_raw {*
+ − 931 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 932 \mode<presentation>{
+ − 933 \begin{frame}<1>[c]
+ − 934 \frametitle{Theorem Provers}
+ − 935
+ − 936 \begin{itemize}
+ − 937 \item You also pay a (sometimes heavy) price: reasoning can be much, much harder.\medskip
+ − 938
+ − 939 \item Depending on your domain, suitable reasoning infrastructure
+ − 940 might not yet be available.
+ − 941 \end{itemize}
+ − 942
+ − 943 \end{frame}}
+ − 944 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 945 *}
+ − 946
+ − 947 text_raw {*
+ − 948 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 949 \mode<presentation>{
+ − 950 \begin{frame}<1>[c]
+ − 951 \frametitle{Theorem Provers}
+ − 952
+ − 953 Recently impressive work has been accomplished proving the correctness
+ − 954
+ − 955 \begin{itemize}
+ − 956 \item of a compiler for C-light (compiled code has the same observable
+ − 957 behaviour as the original source code),\medskip
+ − 958
+ − 959 \item a mirco-kernel operating system (absence of certain
+ − 960 bugs\ldots no nil pointers, no buffer overflows).
+ − 961 \end{itemize}
+ − 962
+ − 963 \end{frame}}
+ − 964 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 965 *}
+ − 966
+ − 967
+ − 968 text_raw {*
+ − 969 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 970 \mode<presentation>{
+ − 971 \begin{frame}<1>[c]
+ − 972 \frametitle{Trust in Theorem Provers}
+ − 973
+ − 974 \begin{center}
+ − 975 Why should we trust theorem provers?
+ − 976 \end{center}
+ − 977
+ − 978 \end{frame}}
+ − 979 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 980 *}
+ − 981
+ − 982 text_raw {*
+ − 983
+ − 984 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 985 \mode<presentation>{
+ − 986 \begin{frame}
+ − 987 \frametitle{Theorem Provers}
+ − 988
+ − 989 \begin{itemize}
+ − 990 \item Theorem provers are a \textcolor{red}{special kind} of software.
+ − 991
+ − 992 \item We do \textcolor{red}{\bf not} need to trust them; we only need to trust:
+ − 993 \end{itemize}
+ − 994
+ − 995 \begin{quote}
+ − 996 \begin{itemize}
+ − 997 \item The logic they are based on \textcolor{gray}{(e.g.~HOL)}, and\smallskip
+ − 998 \item a proof checker that checks the proofs
+ − 999 \textcolor{gray}{(this can be a very small program)}.\smallskip\pause
+ − 1000 \item To a little extend, we also need to trust our definitions
+ − 1001 \textcolor{gray}{(this can be mitigated)}.
+ − 1002 \end{itemize}
+ − 1003 \end{quote}
+ − 1004
+ − 1005 \end{frame}}
+ − 1006 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1007
+ − 1008 *}
+ − 1009
+ − 1010 text_raw {*
+ − 1011
+ − 1012 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1013 \mode<presentation>{
+ − 1014 \begin{frame}
+ − 1015 \frametitle{Isabelle}
+ − 1016
+ − 1017 \begin{itemize}
+ − 1018 \item I am using the Isabelle theorem prover (development since 1990).\bigskip\bigskip\bigskip
+ − 1019
+ − 1020 \item It follows the LCF-approach:
+ − 1021
+ − 1022 \begin{itemize}
+ − 1023 \item Have a special abstract type \alert{\bf thm}.
+ − 1024 \item Make the constructors of this abstract type the inference rules
+ − 1025 of your logic.
+ − 1026 \item Implement the theorem prover in a strongly-typed language (e.g.~ML).
+ − 1027 \end{itemize}
+ − 1028
+ − 1029 $\Rightarrow$ everything of type {\bf thm} has been proved (even if we do not
+ − 1030 have to explicitly generate proofs).
+ − 1031 \end{itemize}
+ − 1032
+ − 1033 \only<1>{
+ − 1034 \begin{textblock}{5}(11,2.3)
+ − 1035 \begin{center}
+ − 1036 \includegraphics[scale=0.18]{robin-milner.jpg}\\[-0.8mm]
+ − 1037 \footnotesize Robin Milner\\[-0.8mm]
+ − 1038 \footnotesize Turing Award, 1991\\
+ − 1039 \end{center}
+ − 1040 \end{textblock}}
+ − 1041
+ − 1042
+ − 1043 \end{frame}}
+ − 1044 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1045 *}
+ − 1046
+ − 1047 text_raw {*
+ − 1048 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1049 \mode<presentation>{
+ − 1050 \begin{frame}<1>[c]
+ − 1051 \frametitle{
+ − 1052 \begin{tabular}{c}
+ − 1053 \mbox{}\\[23mm]
+ − 1054 \LARGE Demo
+ − 1055 \end{tabular}}
+ − 1056
+ − 1057 \end{frame}}
+ − 1058 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1059 *}
+ − 1060
+ − 1061
+ − 1062 text_raw {*
+ − 1063 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1064 \mode<presentation>{
+ − 1065 \begin{frame}<1->[c]
+ − 1066 \frametitle{Future Research}
+ − 1067
+ − 1068 \begin{itemize}
+ − 1069 \item Make theorem provers more like a programming environment.\medskip\pause
+ − 1070
+ − 1071 \item Use all the computational power we get from the hardware to
+ − 1072 automate reasoning (GPUs).\medskip\pause
+ − 1073
+ − 1074 \item Provide a comprehensive reasoning infrastructure for many domains and
+ − 1075 design automated decision procedures.
+ − 1076 \end{itemize}\pause
+ − 1077
+ − 1078
+ − 1079 \begin{center}
+ − 1080 \colorbox{cream}{
+ − 1081 \begin{minipage}{10cm}
+ − 1082 \color{gray}
+ − 1083 \small
+ − 1084 ``Formal methods will never have a significant impact until
+ − 1085 they can be used by people that don't understand them.''\smallskip\\
+ − 1086 \mbox{}\footnotesize\hfill attributed to Tom Melham
+ − 1087 \end{minipage}}
+ − 1088 \end{center}
+ − 1089
+ − 1090 \end{frame}}
+ − 1091 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1092 *}
+ − 1093
+ − 1094 text_raw {*
+ − 1095 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1096 \mode<presentation>{
+ − 1097 \begin{frame}<1->[c]
+ − 1098 \frametitle{Conclusion}
+ − 1099
+ − 1100 \begin{itemize}
+ − 1101 \item The plan is to make this kind of programming the ``future''.\medskip\pause
+ − 1102
+ − 1103 \item Though the technology is already there\\ (compiler + micro-kernel os).\medskip\pause
+ − 1104
+ − 1105 \item Logic and reasoning (especially induction) are important skills for
+ − 1106 Computer Scientists.
+ − 1107 \end{itemize}
+ − 1108
+ − 1109 \end{frame}}
+ − 1110 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1111 *}
+ − 1112
+ − 1113
+ − 1114 text_raw {*
+ − 1115 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1116 \mode<presentation>{
+ − 1117 \begin{frame}<1>[c]
+ − 1118 \frametitle{
+ − 1119 \begin{tabular}{c}
+ − 1120 \mbox{}\\[23mm]
+ − 1121 \alert{\LARGE Thank you very much!}\\
+ − 1122 \alert{\Large Questions?}
+ − 1123 \end{tabular}}
+ − 1124
+ − 1125 \end{frame}}
+ − 1126 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+ − 1127 *}
+ − 1128
+ − 1129
+ − 1130
+ − 1131 (*<*)
+ − 1132 end
+ − 1133 (*>*)