--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/slides/slides05.tex Fri Dec 07 03:15:46 2018 +0000
@@ -0,0 +1,434 @@
+\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,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}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\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:
+
