\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: & S1.27 (1st floor Strand Building)\\ 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 hardwarefaults.\bigskipThey 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}\medskipusing 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 regularexpression 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$} alreadyholds 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$} alreadyholds 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 allstrings \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}\bigskipwhere \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\smallusing 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]{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\pauseDoes 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{$[]$}:\bigskipWe 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$}\bigskipWe 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}%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%