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

\usepackage{../slides}

\usepackage{../langs}

\usepackage{../data}

\usepackage{../graphics}

\usepackage{soul}

\usepackage{proof}

% beamer stuff

\renewcommand{\slidecaption}{CFL, King's College London}

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

\newcommand\grid[1]{%

	\begin{tikzpicture}[baseline=(char.base)]

	\path[use as bounding box]

	(0,0) rectangle (1em,1em);

	\draw[red!50, fill=red!20]

	(0,0) rectangle (1em,1em);

	\node[inner sep=1pt,anchor=base west]

	(char) at (0em,\gridraiseamount) {#1};

	\end{tikzpicture}}

\newcommand\gridraiseamount{0.12em}

\makeatletter

\newcommand\Grid[1]{%

	\@tfor\z:=#1\do{\grid{\z}}}

\makeatother	

\newcommand\Vspace[1][.3em]{%

	\mbox{\kern.06em\vrule height.3ex}%

	\vbox{\hrule width#1}%

	\hbox{\vrule height.3ex}}

\def\VS{\Vspace[0.6em]}

\begin{document}

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

\begin{frame}[t]

\frametitle{%

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

  \\[-3mm]

  \LARGE Compilers and \\[-2mm] 

  \LARGE Formal Languages\\[3mm] 

  \end{tabular}}

  \normalsize

  \begin{center}

  \begin{tabular}{ll}

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

  Office: & N7.07 (North Wing, Bush House)\\

  Slides: & KEATS (also home work is there)\\

  \end{tabular}

  \end{center}

\end{frame}

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

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

\begin{frame}[c]

\frametitle{Compilers \& Boeings 777}

First flight in 1994. They want to achieve triple redundancy in hardware

faults.\bigskip

They compile 1 Ada program to\medskip

\begin{itemize}

\item Intel 80486

\item Motorola 68040 (old Macintosh's)

\item AMD 29050 (RISC chips used often in laser printers)

\end{itemize}\medskip

using 3 independent compilers.\bigskip\pause

\small Airbus uses C and static analysers. Recently started using CompCert.

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

\end{frame}

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

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

\begin{frame}[c]

\frametitle{POSIX Matchers}

\begin{itemize}

\item Longest match rule (``maximal munch rule''): The 

longest initial substring matched by any regular expression 

is taken as the next token.

\begin{center}

\bl{$\texttt{\Grid{iffoo\VS bla}}$}

\end{center}\medskip

\item Rule priority:

For a particular longest initial substring, the first regular

expression that can match determines the token.

\begin{center}

\bl{$\texttt{\Grid{if\VS bla}}$}

\end{center}

\end{itemize}\bigskip\pause

\small

\hfill Kuklewicz: most POSIX matchers are buggy\\

\footnotesize

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

\end{frame}

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

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

\begin{frame}[c]

\mbox{}\\[-14mm]\mbox{}

\small

\bl{

\begin{center}

\begin{tabular}{lcl}

$\textit{der}\;c\;(\ZERO)$ & $\dn$ & $\ZERO$\\

$\textit{der}\;c\;(\ONE)$  & $\dn$ & $\ZERO$\\

$\textit{der}\;c\;(d)$     & $\dn$ & $\textit{if}\; c = d\;\textit{then} \;\ONE \; \textit{else} \;\ZERO$\\

$\textit{der}\;c\;(r_1 + r_2)$ & $\dn$ & $(\textit{der}\;c\;r_1) + (\textit{der}\;c\;r_2)$\\

$\textit{der}\;c\;(r_1 \cdot r_2)$ & $\dn$ & $\textit{if}\;\textit{nullable}(r_1)$\\

      & & $\textit{then}\;((\textit{der}\;c\;r_1)\cdot r_2) + (\textit{der}\;c\;r_2)$\\

      & & $\textit{else}\;(\textit{der}\;c\;r_1)\cdot r_2$\\

$\textit{der}\;c\;(r^*)$ & $\dn$ & $(\textit{der}\;c\;r)\cdot (r^*)$\\

  $\textit{der}\;c\;(r^{\{n\}})$ & $\dn$ & \textit{if} $n=0$ \textit{then} $\ZERO$\\

  & & \textit{else if} $\textit{nullable}(r)$ \textit{then} $(\textit{der}\;c\;r)\cdot (r^{\{\uparrow n-1\}})$\\

  & & \textit{else} $(\textit{der}\;c\;r)\cdot (r^{\{n-1\}})$\\

  $\textit{der}\;c\;(r^{\{\uparrow n\}})$ & $\dn$ & \textit{if} $n=0$ \textit{then} $\ZERO$\\

  & & \textit{else}

  $(\textit{der}\;c\;r)\cdot (r^{\{\uparrow n-1\}})$\\

\end{tabular}

\end{center}}

\end{frame}

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

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

\begin{frame}[t]

\frametitle{Proofs about Rexps}

Remember their inductive definition:

  \begin{center}

  \begin{tabular}{@ {}rrl}

  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}\\

         & \bl{$\mid$} & \bl{$\ONE$}     \\

         & \bl{$\mid$} & \bl{$c$}            \\

         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\

         & \bl{$\mid$} & \bl{$r_1 + r_2$}    \\

         & \bl{$\mid$} & \bl{$r^*$}          \\

         & \bl{$\mid$} & \bl{$r^{\{n\}}$}     \\

         & \bl{$\mid$} & \bl{$r^{\{\uparrow n\}}$}     \\

  \end{tabular}

  \end{center}

If we want to prove something, say a property \bl{$P(r)$}, for all regular expressions \bl{$r$} then \ldots

\end{frame}

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

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

\begin{frame}[c]

\frametitle{Proofs about Rexp (2)}

\begin{itemize}

\item \bl{$P$} holds for \bl{$\ZERO$}, \bl{$\ONE$} and \bl{c}\bigskip

\item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already

holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip

\item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already

holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip

\item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already

  holds for \bl{$r$}.

\item \ldots

\end{itemize}

\end{frame}

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

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

\begin{frame}[c]

\frametitle{Proofs about Strings}

If we want to prove something, say a property \bl{$P(s)$}, for all

strings \bl{$s$} then \ldots\bigskip

\begin{itemize}

\item \bl{$P$} holds for the empty string, and\medskip

\item \bl{$P$} holds for the string \bl{$c\!::\!s$} under the assumption that \bl{$P$}

already holds for \bl{$s$}

\end{itemize}

\end{frame}

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

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

%\begin{frame}[c]

%

%\bl{\begin{center}

%\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}

%$zeroable(\varnothing)$      & $\dn$ & \textit{true}\\

%$zeroable(\epsilon)$         & $\dn$ &  \textit{false}\\

%$zeroable (c)$               & $\dn$ &  \textit{false}\\

%$zeroable (r_1 + r_2)$       & $\dn$ &  $zeroable(r_1) \wedge zeroable(r_2)$ \\ 

%$zeroable (r_1 \cdot r_2)$   & $\dn$ &  $zeroable(r_1) \vee zeroable(r_2)$ \\

%$zeroable (r^*)$             & $\dn$ & \textit{false}\\

%\end{tabular}

%\end{center}}

%\begin{center}

%\bl{$zeroable(r)$} if and only if \bl{$L(r) = \{\}$}

%\end{center}

%\end{frame}

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

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

\begin{frame}[c]

\frametitle{Correctness of the Matcher}

\begin{itemize}

\item We want to prove\medskip

\begin{center}

\bl{$matches\;r\;s$} if and only if \bl{$s\in L(r)$}

\end{center}\bigskip

where \bl{$matches\;r\;s \dn nullable(ders\;s\;r)$}

\bigskip\pause

\item We can do this, if we know\medskip

\begin{center}

\bl{$L(der\;c\;r) = Der\;c\;(L(r))$}

\end{center}

\end{itemize}

\end{frame}

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

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

\begin{frame}[c]

\frametitle{Some Lemmas}

\begin{itemize}

\item \bl{$Der\;c\;(A\cup B) = 

(Der\;c\;A)\cup(Der\;c\;B)$}\bigskip

\item If \bl{$[] \in A$} then

\begin{center}

\bl{$Der\;c\;(A\,@\,B) = (Der\;c\;A)\,@\,B \;\cup\; (Der\;c\;B)$}

\end{center}\bigskip

\item If \bl{$[] \not\in A$} then

\begin{center}

\bl{$Der\;c\;(A\,@\,B) = (Der\;c\;A)\,@\,B$}

\end{center}\bigskip

\item \bl{$Der\;c\;(A^*) = (Der\;c\;A)\,@\,A^*$}\\

\small\mbox{}\hfill (interesting case)\\

\end{itemize}

\end{frame}

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

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

\begin{frame}[c]

\frametitle{Why?}

Why does \bl{$Der\;c\;(A^*) = (Der\;c\;A)\,@\,A^*$} hold?

\bigskip

\begin{center}

\begin{tabular}{lcl}

\bl{$Der\;c\;(A^*)$} & \bl{$=$} &  \bl{$Der\;c\;(A^* - \{[]\})$}\medskip\\

& \bl{$=$} & \bl{$Der\;c\;((A - \{[]\})\,@\,A^*)$}\medskip\\

& \bl{$=$} & \bl{$(Der\;c\;(A - \{[]\}))\,@\,A^*$}\medskip\\

& \bl{$=$} & \bl{$(Der\;c\;A)\,@\,A^*$}\medskip\\

\end{tabular}

\end{center}\bigskip\bigskip

\small

using the facts \bl{$Der\;c\;A = Der\;c\;(A - \{[]\})$} and\\

\mbox{}\hfill\bl{$(A - \{[]\}) \,@\, A^* = A^* - \{[]\}$}

\end{frame}

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

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

\begin{frame}[c]

\frametitle{POSIX Spec}

\begin{center}

\bl{\infer{[] \in \ONE \to Empty}{}}\hspace{15mm}

\bl{\infer{c \in c \to Char(c)}{}}\bigskip\medskip

\bl{\infer{s \in r_1 + r_2 \to Left(v)}

          {s \in r_1 \to v}}\hspace{10mm}

\bl{\infer{s \in r_1 + r_2 \to Right(v)}

          {s \in r_2 \to v & s \not\in L(r_1)}}\bigskip\medskip

\bl{\infer{s_1 @ s_2 \in r_1 \cdot r_2 \to Seq(v_1, v_2)}

          {\small\begin{array}{l}

           s_1 \in r_1 \to v_1 \\

           s_2 \in r_2 \to v_2 \\

           \neg(\exists s_3\,s_4.\; s_3 \not= []

           \wedge s_3 @ s_4 = s_2 \wedge

           s_1 @ s_3 \in L(r_1) \wedge

           s_4 \in L(r_2))

           \end{array}}}

\bl{\ldots}           

\end{center}

\end{frame}

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

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

\begin{frame}[t,squeeze]

\frametitle{Sulzmann \& Lu Paper}

\begin{itemize}

\item I have no doubt the algorithm is correct --- 

  the problem is I do not believe their proof.

  \begin{center}

  \begin{bubble}[10cm]\small

  ``How could I miss this? Well, I was rather careless when 

  stating this Lemma :)\smallskip

  Great example how formal machine checked proofs (and 

  proof assistants) can help to spot flawed reasoning steps.''

  \end{bubble}

  \end{center}\pause

  %\begin{center}

  %\begin{bubble}[10cm]\small

  %``Well, I don't think there's any flaw. The issue is how to 

  %come up with a mechanical proof. In my world mathematical 

  %proof $=$ mechanical proof doesn't necessarily hold.''

  %\end{bubble}

  %\end{center}\pause

\end{itemize}

  \only<3>{%

  \begin{textblock}{11}(1,4.4)

  \begin{center}

  \begin{bubble}[10.9cm]\small\centering

  \includegraphics[scale=0.37]{../pics/msbug.png}

  \end{bubble}

  \end{center}

  \end{textblock}}

\end{frame}

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

\end{document}

%%% Local Variables:  

%%% mode: latex

%%% TeX-master: t

%%% End: 

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

\begin{frame}[t]

\frametitle{2nd CW}

Remember we showed that\\

\begin{center}

\bl{$der\;c\;(r^+) = (der\;c\;r)\cdot r^*$}

\end{center}\bigskip\pause

Does the same hold for \bl{$r^{\{n\}}$} with \bl{$n > 0$}

\begin{center}

\bl{$der\;c\;(r^{\{n\}}) = (der\;c\;r)\cdot r^{\{n-1\}}$} ?

\end{center}

\end{frame}

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

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

\begin{frame}[t]

\frametitle{2nd CW}

\begin{itemize}

\item \bl{$der$}

\begin{center}

\bl{$der\;c\;(r^{\{n\}}) \dn 

\begin{cases}

\varnothing & \text{\textcolor{black}{if}}\; n = 0\\

der\;c\;(r\cdot r^{\{n-1\}}) & \text{\textcolor{black}{o'wise}}

\end{cases}$} 

\end{center}

\item \bl{$mkeps$}

\begin{center}

\bl{$mkeps(r^{\{n\}}) \dn

[\underbrace{mkeps(r),\ldots,mkeps(r)}_{n\;times}]$} 

\end{center}

\item \bl{$inj$}

\begin{center}

\begin{tabular}{l@{\hspace{1mm}}c@{\hspace{1mm}}l}

\bl{$inj\;r^{\{n\}}\;c\;(v_1, [vs])$}     & \bl{$\dn$} &

\bl{$[inj\;r\;c\;v_1::vs]$}\\

\bl{$inj\;r^{\{n\}}\;c\;Left(v_1, [vs])$} & \bl{$\dn$} &

\bl{$[inj\;r\;c\;v_1::vs]$}\\

\bl{$inj\;r^{\{n\}}\;c\;Right([v::vs])$}  & \bl{$\dn$} &

\bl{$[mkeps(r)::inj\;r\;c\;v::vs]$}\\

\end{tabular}

\end{center}

\end{itemize}

\end{frame}

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

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

\begin{frame}[c]

\frametitle{Induction over Strings}

\begin{itemize}

\item case \bl{$[]$}:\bigskip

We need to prove 

\begin{center}

  \bl{$\forall r.\;\;nullable(ders\;[]\;r) \;\Leftrightarrow\; [] \in L(r)$}

\end{center}\bigskip  

\begin{center}

  \bl{$nullable(ders\;[]\;r) \;\dn\; nullable\;r \;\Leftrightarrow\ldots$}

\end{center} 

\end{itemize}

\end{frame}

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

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

\begin{frame}[c]

\frametitle{Induction over Strings}

\begin{itemize}

\item case \bl{$c::s$}\bigskip

We need to prove 

\begin{center}

  \bl{$\forall r.\;\;nullable(ders\;(c::s)\;r) \;\Leftrightarrow\; (c::s) \in L(r)$}

\end{center} 

We have by IH

\begin{center}

  \bl{$\forall r.\;\;nullable(ders\;s\;r) \;\Leftrightarrow\; s \in L(r)$}

\end{center}\bigskip 

\begin{center}

\bl{$ders\;(c::s)\;r \dn ders\;s\;(der\;c\;r)$}

\end{center}

\end{itemize}

\end{frame}

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

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

\begin{frame}[c]

\frametitle{Induction over Regexps}

\begin{itemize}

\item The proof hinges on the fact that we can prove\bigskip

\begin{center}

  \Large\bl{$L(der\;c\;r) = Der\;c\;(L(r))$}

\end{center} 

\end{itemize}

\end{frame}

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