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