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