\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.00003500001 0.225271000001 0.627521500001 0.884852000001 1.398152500001 1.686193000001 1.949573500001 2.158784000001 2.599184500001 5.906795000001 13.112955500001 19.153766000001 40.16373\end{filecontents}\begin{filecontents}{re-python2.data}1 0.0335 0.03610 0.03415 0.03618 0.05919 0.08420 0.14121 0.24822 0.48523 0.87824 1.7125 3.4026 7.0827 14.1228 26.69\end{filecontents}\begin{filecontents}{re-java.data}5 0.0029810 0.0041815 0.0099616 0.0171017 0.0349218 0.0330319 0.0508420 0.1017721 0.1996022 0.4115923 0.8223424 1.7025125 3.3611226 6.6399827 13.3512028 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}\bigskipsimilarly\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 havehelp from the computer. `Program' is here to be understood to bequite 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 alsomany in LLVM (some of them highest-level critical)\bigskip\item about CompCert:\begin{bubble}[10cm]\small ``The striking thing about our CompCertresults is that the middle-end bugs we found in all othercompilers are absent. As of early 2011, the under-developmentversion of CompCert is the only compiler we have tested forwhich Csmith cannot find wrong-code errors. This is not forlack of trying: we have devoted about six CPU-years to thetask.'' \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: