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