1 \documentclass[runningheads]{llncs}

     2 \usepackage{times}

     3 \usepackage{isabelle}

     4 \usepackage{isabellesym}

     5 \usepackage{amsmath}

     6 \usepackage{amssymb}

     7 \usepackage{mathpartir}

     8 \usepackage{tikz}

     9 \usepackage{pgf}

    10 \usetikzlibrary{positioning}

    11 \usepackage{pdfsetup}

    12 %%\usepackage{stmaryrd}

    13 \usepackage{url}

    14 \usepackage{color}

    15 

    16 \titlerunning{POSIX Lexing with Derivatives of Regular Expressions}

    17 

    18 \urlstyle{rm}

    19 \isabellestyle{it}

    20 \renewcommand{\isastyleminor}{\it}% 

    21 \renewcommand{\isastyle}{\normalsize\it}%

    22 

    23 

    24 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,}

    25 \renewcommand{\isasymequiv}{$\dn$}

    26 \renewcommand{\isasymemptyset}{$\varnothing$}

    27 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}}

    28 \renewcommand{\isasymiota}{\makebox[0mm]{${}^{\prime}$}}

    29 

    30 \def\Brz{Brzozowski}

    31 \def\der{\backslash}

    32 \newtheorem{falsehood}{Falsehood}

    33 \newtheorem{conject}{Conjecture}

    34 

    35 \begin{document}

    36 

    37 \title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions (Proof Pearl)}

    38 \author{Fahad Ausaf\inst{1} \and Roy Dyckhoff\inst{2} \and Christian Urban\inst{3}}

    39 \institute{King's College London\\

    40 		\email{fahad.ausaf@icloud.com}

    41 \and University of St Andrews\\

    42 		\email{roy.dyckhoff@st-andrews.ac.uk}

    43 \and King's College London\\

    44 		\email{christian.urban@kcl.ac.uk}}

    45 \maketitle

    46 

    47 \begin{abstract}

    48 

    49 Brzozowski introduced the notion of derivatives for regular

    50 expressions. They can be used for a very simple regular expression

    51 matching algorithm.  Sulzmann and Lu cleverly extended this algorithm

    52 in order to deal with POSIX matching, which is the underlying

    53 disambiguation strategy for regular expressions needed in lexers.

    54 Sulzmann and Lu have made available on-line what they call a

    55 ``rigorous proof'' of the correctness of their algorithm w.r.t.\ their

    56 specification; regrettably, it appears to us to have unfillable gaps.

    57 In the first part of this paper we give our inductive definition of

    58 what a POSIX value is and show $(i)$ that such a value is unique (for

    59 given regular expression and string being matched) and $(ii)$ that

    60 Sulzmann and Lu's algorithm always generates such a value (provided

    61 that the regular expression matches the string).  We also prove the

    62 correctness of an optimised version of the POSIX matching

    63 algorithm. Our definitions and proof are much simpler than those by

    64 Sulzmann and Lu and can be easily formalised in Isabelle/HOL. In the

    65 second part we analyse the correctness argument by Sulzmann and Lu and

    66 explain why the gaps in this argument cannot be filled easily.\smallskip

    67 

    68 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions,

    69 Isabelle/HOL

    70 \end{abstract}

    71 

    72 \input{session}

    73 

    74 \end{document}

    75 

    76 %%% Local Variables:

    77 %%% mode: latex

    78 %%% TeX-master: t

    79 %%% End: