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

