% !TEX program = xelatex

\usepackage{../slides}

\usepackage{../graphics}

\usepackage{../langs}

%%\usepackage{../data}

%%\usepackage[export]{adjustbox}

\usetikzlibrary{shapes,arrows,shadows}

\hfuzz=220pt 

%\setmonofont[Scale=.88]{Consolas}

%\newfontfamily{\consolas}{Consolas}

\lstset{language=Scala,

        style=mystyle,

        numbersep=0pt,

        numbers=none,

        xleftmargin=0mm}

\newcommand{\bl}[1]{\textcolor{blue}{#1}}     

% beamer stuff 

\renewcommand{\slidecaption}{PEP (Scala) 05, King's College London}

\begin{document}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}[t]

\frametitle{%

  \begin{tabular}{@ {}c@ {}}

  \\[5mm]

  \huge PEP Scala (5) 

  \end{tabular}}

  \normalsize

  \begin{center}

  \begin{tabular}{ll}

    Email:  & christian.urban at kcl.ac.uk\\

    Slides \& Code: & KEATS\\

  \end{tabular}

  \end{center}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

\begin{frame}[c]

\frametitle{Plan for Today}

\begin{itemize}

\item Being Lazy

\item Polymorphic Types

\item Immutable OOP

\item Making Fun about Scala

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

\begin{frame}[c,fragile]

\frametitle{How To calcululate 100 Mio Collatz Series?} 

\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=1mm]

(1L to 100_000_000).map(collatz).max

\end{lstlisting}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

\begin{frame}[c,fragile]

\frametitle{Polyorphic Types} 

To be avoided:\bigskip\bigskip

\small

\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-6mm]

def length_string_list(lst: List[String]): Int = 

 lst match {

   case Nil => 0

   case x::xs => 1 + length_string_list(xs)

 }

def length_int_list(lst: List[Int]): Int = 

 lst match {

   case Nil => 0

   case x::xs => 1 + length_int_list(xs)

 }

\end{lstlisting}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

\begin{frame}[c,fragile]

\frametitle{Polyorphic Types} 

\small

\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-6mm]

def length[A](lst: List[A]): Int = lst match {

  case Nil => 0

  case x::xs => 1 + length(xs)

}

length(List("1", "2", "3", "4"))

length(List(1, 2, 3, 4))

def map[A, B](lst: List[A], f: A => B): List[B] = 

 lst match {

   case Nil => Nil

   case x::xs => f(x)::map(xs, f) 

 }

\end{lstlisting}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}[c]

\frametitle{DFAs}  

\begin{center}

\begin{tikzpicture}[>=stealth',very thick,auto,

  every state/.style={minimum size=0pt,inner sep=2pt,

    draw=blue!50,very thick,fill=blue!20},]

\only<1,3->{\node[state,initial] (Q_0)  {$\mbox{Q}_0$};}

\only<2>{\node[state,initial,fill=red] (Q_0)  {$\mbox{Q}_0$};}  

\only<1,2,4->{\node[state] (Q_1) [right=of Q_0] {$\mbox{Q}_1$};}

\only<3>{\node[state,fill=red] (Q_1) [right=of Q_0] {$\mbox{Q}_1$};}

\only<-3,5->{\node[state] (Q_2) [below right=of Q_0] {$\mbox{Q}_2$};}

\only<4>{\node[state,fill=red] (Q_2) [below right=of Q_0] {$\mbox{Q}_2$};}

\only<-4,6->{\node[state] (Q_3) [right=of Q_2] {$\mbox{Q}_3$};}

\only<5>{\node[state,fill=red] (Q_3) [right=of Q_2] {$\mbox{Q}_3$};}

\only<-5>{\node[state, accepting] (Q_4) [right=of Q_1] {$\mbox{Q}_4$};}

\only<6->{\node[state, accepting,fill=red] (Q_4) [right=of Q_1] {$\mbox{Q}_4$};}

\path[->] (Q_0) edge node [above]  {\alert{$a$}} (Q_1);

\path[->] (Q_1) edge node [above]  {\alert{$a$}} (Q_4);

\path[->] (Q_4) edge [loop right] node  {\alert{$a, b$}} ();

\path[->] (Q_3) edge node [right]  {\alert{$a$}} (Q_4);

\path[->] (Q_2) edge node [above]  {\alert{$a$}} (Q_3);

\path[->] (Q_1) edge node [right]  {\alert{$b$}} (Q_2);

\path[->] (Q_0) edge node [above]  {\alert{$b$}} (Q_2);

\path[->] (Q_2) edge [loop left] node  {\alert{$b$}} ();

\path[->] (Q_3) edge [bend left=95, looseness=1.3] node [below]  {\alert{$b$}} (Q_0);

\end{tikzpicture}

\end{center}

\end{textblock}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}[t]

\frametitle{DFAs}

A \alert{\bf deterministic finite automaton} (DFA) consists of

5 things:

\begin{itemize}

\item an alphabet \bl{$\varSigma$}  

\item a set of states \bl{$\mbox{Qs}$}

\item one of these states is the start state \bl{$\mbox{Q}_0$}

\item some states are accepting states \bl{$F$}, and

\item there is transition function \bl{$\delta$}\bigskip 

\small

which takes a state  and a character as arguments and produces a 

new state; this function might not be everywhere defined 

\end{itemize}

\begin{center}

\bl{$A(\varSigma, \mbox{Qs}, \mbox{Q}_0, F, \delta)$}

\end{center}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}[c]

\frametitle{NFAs}  

\begin{center}

\begin{tikzpicture}[>=stealth',very thick, auto,

    every state/.style={minimum size=0pt,inner sep=3pt,

      draw=blue!50,very thick,fill=blue!20},scale=2]

\node[state,initial]  (Q_0)  {$\mbox{Q}_0$};

\node[state] (Q_1) [right=of Q_0] {$\mbox{Q}_1$};

\node[state, accepting] (Q_2) [right=of Q_1] {$\mbox{Q}_2$};

\path[->] (Q_0) edge [loop above] node  {\alert{$b$}} ();

\path[<-] (Q_0) edge node [below]  {\alert{$b$}} (Q_1);

\path[->] (Q_0) edge [bend left] node [above]  {\alert{$a$}} (Q_1);

\path[->] (Q_0) edge [bend right=45,looseness=1.3] node [below]  {\alert{$a$}} (Q_2);

\path[->] (Q_1) edge [loop above] node  {\alert{$a,b$}} ();

\path[->] (Q_1) edge node  [above] {\alert{$a$}} (Q_2);

\end{tikzpicture}

\end{center}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\tikzstyle{sensor}=[draw, fill=blue!20, text width=3.8em, line width=1mm,

    text centered, minimum height=2em,drop shadow]

\tikzstyle{ann} = [above, text width=4em, text centered]

\tikzstyle{sc} = [sensor, text width=7em, fill=red!20, 

    minimum height=6em, rounded corners, drop shadow,line width=1mm]

\begin{frame}[fragile,c]

\frametitle{Compilers 6CCS3CFL}

\begin{tikzpicture}

    % Validation Layer is the same except that there are a set of nodes and links which are added

    \path (0,0) node (IR) [sc] {\textbf{WHILE Language}\\ compiler};

    \path (IR.west)+(-2.2,1.7) node (sou1) [sensor] {Fact};

    \path (IR.west)+(-2.2,0.5) node (sou2)[sensor] {Fib};

    \path (IR.west)+(-2.2,-0.7) node (sou4)[sensor] {Primes}; 

    \only<2>{\path (IR.west)+(-2.2,-1.9) node (sou3)[sensor] {BrainF**k};}    

    \path [draw,->,line width=1mm] (sou1.east) -- node [above] {} (IR.160);

    \path [draw,->,line width=1mm] (sou2.east) -- node [above] {} (IR.180);

    \only<2>{\path [draw,->,line width=1mm] (sou3.east) -- node [above] {} (IR.200);}

    \path [draw,->,line width=1mm] (sou4.east) -- node [above] {} (IR.190);

    \path (IR.east)+(2.2, 0.8) node (tar2)[sensor] {JVM};

    \path (IR.east)+(2.2,-0.8) node (tar3)[sensor] {LLVM{\small(x86)}}; 

    \path [draw,<-,line width=1mm] (tar2.west) -- node [above] {} (IR.5);

    \path [draw,<-,line width=1mm] (tar3.west) -- node [above] {} (IR.-5);

\end{tikzpicture}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  \begin{frame}[c]

  \frametitle{Dijkstra on Testing}

  \begin{bubble}[10cm]

  ``Program testing can be a very effective way to show the

  presence of bugs, but it is hopelessly inadequate for showing

  their absence.''

  \end{bubble}\bigskip

  \end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}[c]

\frametitle{\Large Proving Programs to be Correct}

\begin{bubble}[10cm]

\small

{\bf Theorem:} There are infinitely many prime 

numbers.\medskip\\

{\bf Proof} \ldots\\

\end{bubble}\bigskip

similarly\bigskip

\begin{bubble}[10cm]

\small

{\bf Theorem:} The program is doing what 

it is supposed to be doing.\medskip

{\bf Long, long proof} \ldots\\

\end{bubble}\bigskip\medskip

\small This can be a gigantic proof. The only hope is to have

help from the computer. `Program' is here to be understood to be

quite general (compiler, OS, \ldots).

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

\begin{frame}[c]

\frametitle{Can This Be Done?}

\begin{itemize}

\item in 2011, verification of a small C-compiler (CompCert)

\begin{itemize}

\item ``if my input program has a certain behaviour, then the compiled machine code has the same behaviour''

\item is as good as \texttt{gcc -O1}, but much, much less buggy 

\end{itemize}

\end{itemize}

\begin{center}

  \includegraphics[scale=0.12]{../pics/compcert.png}

\end{center}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%% ~2,237,800 lines of proof in 474

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

\begin{frame}[c]

\frametitle{Fuzzy Testing C-Compilers}

\begin{itemize}

\item tested GCC, LLVM and others by randomly generating 

C-programs

\item found more than 300 bugs in GCC and also

many in LLVM (some of them highest-level critical)\bigskip

\item about CompCert:

\begin{bubble}[10cm]\small ``The striking thing about our CompCert

results is that the middle-end bugs we found in all other

compilers are absent. As of early 2011, the under-development

version of CompCert is the only compiler we have tested for

which Csmith cannot find wrong-code errors. This is not for

lack of trying: we have devoted about six CPU-years to the

task.'' 

\end{bubble} 

\end{itemize}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}[c]

\frametitle{seL4 / Isabelle}

\begin{itemize}

\item verified a microkernel operating system ($\approx$8000 lines of C code)\bigskip

\item US DoD has competitions to hack into drones; they found that the

  isolation guarantees of seL4 hold up\bigskip

\item CompCert and seL4 sell their code  

\end{itemize}

\only<2>{

\begin{textblock}{5}(5.5,1.9)

  \includegraphics[scale=0.25]{../pics/drone.jpg}

\end{textblock}}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

\begin{frame}[c]

\frametitle{Where to go on from here?}

\begin{itemize}

\item Martin Odersky (EPFL)\ldots he is currently throwing out everything

  and starts again with the dotty compiler for Scala 3.0\medskip

\item Elm (\url{http://elm-lang.org})\ldots web applications with style\medskip   

\item Haskell, Ocaml, Standard ML, Scheme, \ldots 

\end{itemize}  

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}[c,fragile]

\frametitle{\alert{Questions?}}

{\tiny

\begin{verbatim}

                               *

                              * *

                             *   *

                            * * * *

                           *       *

                          * *     * *

                         *   *   *   *

                        * * * * * * * *

                       *               *

                      * *             * *

                     *   *           *   *

                    * * * *         * * * *

                   *       *       *       *

                  * *     * *     * *     * *

                 *   *   *   *   *   *   *   *

                * * * * * * * * * * * * * * * *

               *                               *

              * *                             * *

             *   *                           *   *

            * * * *                         * * * *

           *       *                       *       *

          * *     * *                     * *     * *

         *   *   *   *                   *   *   *   *

        * * * * * * * *                 * * * * * * * *

       *               *               *               *

      * *             * *             * *             * *

     *   *           *   *           *   *           *   *

    * * * *         * * * *         * * * *         * * * *

   *       *       *       *       *       *       *       *

  * *     * *     * *     * *     * *     * *     * *     * *

 *   *   *   *   *   *   *   *   *   *   *   *   *   *   *   *

* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *

\end{verbatim}}

\begin{textblock}{6}(8.5,3.5)

\begin{bubble}[5cm]

\footnotesize

\begin{lstlisting}[language=Scala, numbers=none, xleftmargin=-1mm]

++++++++[>+>++++<<-]>++>>

+<[-[>>+<<-]+>>]>+[-<<<[-

>[+[-]+>++>>>-<<]<[<]>>++

++++[<<+++++>>-]+<<++.[-]

<<]>.>+[>>]>+]

\end{lstlisting}

\end{bubble}

\end{textblock}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{frame}[t]

  \begin{center}  

  \includegraphics[scale=0.4]{../pics/mind2.jpg}

  \end{center}

  \begin{textblock}{14}(2,11.4)

  \large\bf{}Mind-Blowing Programming Languages:\\ 

  \centering Scala\;\;?

  \end{textblock}

\end{frame}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\end{document}

\end{document}

%%% Local Variables:  

%%% mode: latex

%%% TeX-master: t

%%% End: