\documentclass[runningheads]{llncs}+
−
\usepackage{isabelle}+
−
\usepackage{isabellesym}+
−
\usepackage{amsmath}+
−
\usepackage{amssymb}+
−
\usepackage{mathpartir}+
−
\usepackage{tikz}+
−
\usepackage{pgf}+
−
\usepackage{pdfsetup}+
−
\usepackage{ot1patch}+
−
\usepackage{times}+
−
\usepackage{stmaryrd}+
−
\usepackage{url}+
−
\usepackage{color}+
−
+
−
\titlerunning{BLA BLA}+
−
+
−
\urlstyle{rm}+
−
\isabellestyle{it}+
−
\renewcommand{\isastyleminor}{\it}%+
−
\renewcommand{\isastyle}{\normalsize\it}%+
−
+
−
+
−
\def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}+
−
\renewcommand{\isasymequiv}{$\dn$}+
−
\renewcommand{\isasymemptyset}{$\varnothing$}+
−
\renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}+
−
+
−
\definecolor{mygrey}{rgb}{.80,.80,.80}+
−
\def\Brz{Brzozowski}+
−
+
−
+
−
\begin{document}+
−
+
−
\title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions (Proof Pearl)}+
−
\author{Fahad Ausaf\inst{1} \and Roy Dyckhoff\inst{2} \and Christian Urban\inst{1}}+
−
\institute{King's College London, United Kingdom \and +
−
           St Andrews}+
−
\maketitle+
−
+
−
\begin{abstract}+
−
+
−
\Brz{} introduced the notion of derivatives for regular+
−
expressions. They can be used for a very simple regular expression+
−
matching algorithm.  Sulzmann and Lu cleverly extended this algorithm+
−
in order to deal with POSIX matching, which is the underlying+
−
disambiguation strategy for regular expressions needed in+
−
lexers. Sulzmann and Lu have made available on-line what they call a+
−
``rigorous proof'' of the correctness of their algorithm w.r.t.~their+
−
specification; regrettably, it appears to us to have unfillable gaps.+
−
In the first part of this paper we give our inductive definition of+
−
what a POSIX value is and show $(i)$ that such a value is unique (for+
−
given regular expression and string being matched) and $(ii)$ that+
−
Sulzmann and Lu's algorithm always generates such a value (provided+
−
that the regular expression matches the string).  We also prove the+
−
correctness of an optimised version of the POSIX matching+
−
algorithm. Our definitions and proof are much simpler than those by+
−
Sulzmann and Lu and can be easily formalised in Isabelle/HOL.  In the+
−
second part we analyse the correctness argument by Sulzmann and Lu in+
−
more detail and explain why it seems hard to turn it into a proof+
−
rigorous enough to be accepted by a system such as Isabelle/HOL.+
−
+
−
{\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,+
−
Isabelle/HOL+
−
\end{abstract}+
−
+
−
\input{session}+
−
+
−
\end{document}+
−
+
−
%%% Local Variables:+
−
%%% mode: latex+
−
%%% TeX-master: t+
−
%%% End:+
−