1 \documentclass[runningheads]{llncs} |
1 \documentclass[runningheads]{llncs} |
|
2 \usepackage{times} |
2 \usepackage{isabelle} |
3 \usepackage{isabelle} |
3 \usepackage{isabellesym} |
4 \usepackage{isabellesym} |
4 \usepackage{amsmath} |
5 \usepackage{amsmath} |
5 \usepackage{amssymb} |
6 \usepackage{amssymb} |
6 \usepackage{mathpartir} |
7 \usepackage{mathpartir} |
7 \usepackage{tikz} |
8 \usepackage{tikz} |
8 \usepackage{pgf} |
9 \usepackage{pgf} |
9 \usepackage{pdfsetup} |
10 \usepackage{pdfsetup} |
10 \usepackage{ot1patch} |
11 \usepackage{ot1patch} |
11 \usepackage{times} |
|
12 \usepackage{stmaryrd} |
12 \usepackage{stmaryrd} |
13 \usepackage{url} |
13 \usepackage{url} |
14 \usepackage{color} |
14 \usepackage{color} |
15 |
15 |
16 \titlerunning{BLA BLA} |
16 \titlerunning{POSIX Lexing with Derivatives} |
17 |
17 |
18 \urlstyle{rm} |
18 \urlstyle{rm} |
19 \isabellestyle{it} |
19 \isabellestyle{it} |
20 \renewcommand{\isastyleminor}{\it}% |
20 \renewcommand{\isastyleminor}{\it}% |
21 \renewcommand{\isastyle}{\normalsize\it}% |
21 \renewcommand{\isastyle}{\normalsize\it}% |
22 |
22 |
23 |
23 |
24 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
24 \def\dn{\,\stackrel{\mbox{\scriptsize def}}{=}\,} |
25 \renewcommand{\isasymequiv}{$\dn$} |
25 \renewcommand{\isasymequiv}{$\dn$} |
26 \renewcommand{\isasymemptyset}{$\varnothing$} |
26 \renewcommand{\isasymemptyset}{$\varnothing$} |
27 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
27 \renewcommand{\isacharunderscore}{\mbox{$\_\!\_$}} |
28 |
28 |
29 \definecolor{mygrey}{rgb}{.80,.80,.80} |
29 \definecolor{mygrey}{rgb}{.80,.80,.80} |
30 \def\Brz{Brzozowski} |
30 \def\Brz{Brzozowski} |
31 |
31 \def\der{\backslash} |
|
32 \newcommand{\eps}{\varepsilon} |
|
33 \newcommand{\mts}{\eps} |
32 |
34 |
33 \begin{document} |
35 \begin{document} |
34 |
36 |
35 \title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions (Proof Pearl)} |
37 \title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions (Proof Pearl)} |
36 \author{Fahad Ausaf\inst{1} \and Roy Dyckhoff\inst{2} \and Christian Urban\inst{1}} |
38 \author{Fahad Ausaf\inst{1} \and Roy Dyckhoff\inst{2} \and Christian Urban\inst{3}} |
37 \institute{King's College London, United Kingdom \and |
39 \institute{King's College London\\ |
38 St Andrews} |
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}} |
39 \maketitle |
45 \maketitle |
40 |
46 |
41 \begin{abstract} |
47 \begin{abstract} |
42 |
48 |
43 \Brz{} introduced the notion of derivatives for regular |
49 Brzozowski introduced the notion of derivatives for regular |
44 expressions. They can be used for a very simple regular expression |
50 expressions. They can be used for a very simple regular expression |
45 matching algorithm. Sulzmann and Lu cleverly extended this algorithm |
51 matching algorithm. Sulzmann and Lu cleverly extended this algorithm |
46 in order to deal with POSIX matching, which is the underlying |
52 in order to deal with POSIX matching, which is the underlying |
47 disambiguation strategy for regular expressions needed in |
53 disambiguation strategy for regular expressions needed in lexers. |
48 lexers. Sulzmann and Lu have made available on-line what they call a |
54 Sulzmann and Lu have made available on-line what they call a |
49 ``rigorous proof'' of the correctness of their algorithm w.r.t.~their |
55 ``rigorous proof'' of the correctness of their algorithm w.r.t.\ their |
50 specification; regrettably, it appears to us to have unfillable gaps. |
56 specification; regrettably, it appears to us to have unfillable gaps. |
51 In the first part of this paper we give our inductive definition of |
57 In the first part of this paper we give our inductive definition of |
52 what a POSIX value is and show $(i)$ that such a value is unique (for |
58 what a POSIX value is and show $(i)$ that such a value is unique (for |
53 given regular expression and string being matched) and $(ii)$ that |
59 given regular expression and string being matched) and $(ii)$ that |
54 Sulzmann and Lu's algorithm always generates such a value (provided |
60 Sulzmann and Lu's algorithm always generates such a value (provided |
55 that the regular expression matches the string). We also prove the |
61 that the regular expression matches the string). We also prove the |
56 correctness of an optimised version of the POSIX matching |
62 correctness of an optimised version of the POSIX matching |
57 algorithm. Our definitions and proof are much simpler than those by |
63 algorithm. Our definitions and proof are much simpler than those by |
58 Sulzmann and Lu and can be easily formalised in Isabelle/HOL. In the |
64 Sulzmann and Lu and can be easily formalised in Isabelle/HOL. In the |
59 second part we analyse the correctness argument by Sulzmann and Lu in |
65 second part we analyse the correctness argument by Sulzmann and Lu and |
60 more detail and explain why it seems hard to turn it into a proof |
66 explain why it seems hard to turn it into a proof rigorous enough to |
61 rigorous enough to be accepted by a system such as Isabelle/HOL. |
67 be accepted by a system such as Isabelle/HOL.\smallskip |
62 |
68 |
63 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions, |
69 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions, |
64 Isabelle/HOL |
70 Isabelle/HOL |
65 \end{abstract} |
71 \end{abstract} |
66 |
72 |