\documentclass[dvipsnames,14pt,t,xelatex]{beamer}

\usepackage{../slides}

\usepackage{../graphics}

\usepackage{../langs}

%%\usepackage{../data}

\usepackage[export]{adjustbox}

\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{filecontents}{re3a.data}

1 0.00003

500001 0.22527

1000001 0.62752

1500001 0.88485

2000001 1.39815

2500001 1.68619

3000001 1.94957

3500001 2.15878

4000001 2.59918

4500001 5.90679

5000001 13.11295

5500001 19.15376

6000001 40.16373

\end{filecontents}

\begin{filecontents}{re-python2.data}

1 0.033

5 0.036

10 0.034

15 0.036

18 0.059

19 0.084

20 0.141

21 0.248

22 0.485

23 0.878

24 1.71

25 3.40

26 7.08

27 14.12

28 26.69

\end{filecontents}

\begin{filecontents}{re-java.data}

5  0.00298

10  0.00418

15  0.00996

16  0.01710

17  0.03492

18  0.03303

19  0.05084

20  0.10177

21  0.19960

22  0.41159

23  0.82234

24  1.70251

25  3.36112

26  6.63998

27  13.35120

28  29.81185

\end{filecontents}

%All O2 technical teams are working closely with one of our third party suppliers who has identified a global software issue in their system which has impacted data services.  

\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\\

    Office: & N\liningnums{7.07} (North Wing, Bush House)\\

    Slides \& Code: & KEATS\medskip\\

    Office Hours: &  Mondays 12:00 -- 14:00\\

  \end{tabular}

  \end{center}

\end{frame}

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

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

\begin{frame}[c]

\frametitle{Marks for CW7 (Part 1 +  2)}

Raw marks (234 submissions):

\begin{itemize}

\item 6\%: \hspace{4mm}192 students

\item 5\%: \hspace{4mm}16

\item 4\%: \hspace{4mm}7

\item 3\%: \hspace{4mm}2

\item 2\%: \hspace{4mm}6

\item 1\%: \hspace{4mm}1

\item 0\%: \hspace{4mm}9 

\end{itemize}  

\end{frame}

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

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

\begin{frame}[c,fragile]

\small

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

def get_csv_url(url: String) : List[String] = {

  val csv = Try(Source.fromURL(url)).getOrElse(null)

   if (csv == null){

     List()

   }

   else {

     ....

   }

}

\end{lstlisting}

\pause

\bigskip

\rule{11cm}{0.3mm}

\bigskip

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

def get_csv_url(url: String) : List[String] = {

  Try(Source.fromURL(url)....).getOrElse(Nil)

\end{lstlisting}

\end{frame}

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

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

\begin{frame}[c,fragile]

\small

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

def get_csv_url(url: String) : List[String] = {

    try {

        val csvFile = Source.fromURL(url)

        ....

    } catch {

        case unknown : Throwable => List()

    }

}

\end{lstlisting}

\bigskip

\rule{11cm}{0.3mm}

\bigskip

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

def get_csv_url(url: String) : List[String] = {

  Try(Source.fromURL(url)....).getOrElse(Nil)

\end{lstlisting}

\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{CW9 : Regexes}

\begin{center}

  Graphs: $(a^*)^* b$ and strings $\underbrace{\;a\ldots a\;}_{n}$\bigskip

\begin{tabular}[t]{@{\hspace{-8mm}}c@{\hspace{-4mm}}c@{}}

\raisebox{6mm}{\begin{tikzpicture}

\begin{axis}[

    xlabel={$n$},

    x label style={at={(1.05,0.0)}},

    ylabel={time in secs},

    enlargelimits=false,

    xtick={0,5,...,30},

    xmax=33,

    ymax=35,

    ytick={0,5,...,30},

    scaled ticks=false,

    axis lines=left,

    width=5.5cm,

    height=5cm, 

    legend entries={Python,  Java 8},  

    legend pos=north west,

    legend cell align=left]

\addplot[blue,mark=*, mark options={fill=white}] table {re-python2.data};  

\addplot[cyan,mark=*, mark options={fill=white}] table {re-java.data};

\end{axis}

\end{tikzpicture}}

  &

\onslide<1>{\begin{tikzpicture}

  \begin{axis}[

    xlabel={$n$},

    x label style={at={(1.05,0.0)}},

    ylabel={time in secs},

    enlargelimits=false,

    ymax=35,

    ytick={0,5,...,30},

    axis lines=left,

    %%scaled ticks=false,

    width=5.5cm, 

    height=5cm]

%%\addplot[green,mark=square*,mark options={fill=white}] table {re2a.data};    

\addplot[red,mark=square*,mark options={fill=white}] table {re3a.data};

\end{axis}

\end{tikzpicture}}

\end{tabular}

\end{center}

\small

\hfill Kuklewicz: most POSIX matchers are buggy\\

\footnotesize

\hfill \url{http://www.haskell.org/haskellwiki/Regex_Posix}

\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\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}[c]

\frametitle{Marks for CW6 (Part 1 + 2)}

Raw marks:

\begin{itemize}

\item 6\%: 154 students

\item 5\%: 66

\item 4\%: 18

\item 3\%: 13

\item 2\%: 2

\item 1\%: 1

\item 0\%: 21 

\end{itemize}  

\end{frame}

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

\end{document}

\end{document}

%%% Local Variables:  

%%% mode: latex

%%% TeX-master: t

%%% End: