37 \institute{King's College London, United Kingdom \and |
37 \institute{King's College London, United Kingdom \and |
38 St Andrews} |
38 St Andrews} |
39 \maketitle |
39 \maketitle |
40 |
40 |
41 \begin{abstract} |
41 \begin{abstract} |
42 \Brz{} introduced the notion of derivatives of regular expressions |
|
43 that can be used for very simple regular expression matching algorithms. |
|
44 |
42 |
45 BLA BLA Sulzmann and Lu \cite{Sulzmann2014} |
43 \Brz{} introduced the notion of derivatives for regular |
|
44 expressions. They can be used for a very simple regular expression |
|
45 matching algorithm. Sulzmann and Lu cleverly extended this algorithm |
|
46 in order to deal with POSIX matching, which is the underlying |
|
47 disambiguation strategy for regular expressions needed in |
|
48 lexers. 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 |
|
50 specification; regrettably, it appears to us to have unfillable gaps. |
|
51 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 |
|
53 given regular expression and string being matched) and $(ii)$ that |
|
54 Sulzmann and Lu's algorithm always generates such a value (provided |
|
55 that the regular expression matches the string). We also prove the |
|
56 correctness of an optimised version of the POSIX matching |
|
57 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 |
|
59 second part we analyse the correctness argument by Sulzmann and Lu in |
|
60 more detail and explain why it seems hard to turn it into a proof |
|
61 rigorous enough to be accepted by a system such as Isabelle/HOL. |
46 |
62 |
47 {\bf Keywords:} |
63 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions, |
|
64 Isabelle/HOL |
48 \end{abstract} |
65 \end{abstract} |
49 |
66 |
50 \input{session} |
67 \input{session} |
51 |
68 |
52 \end{document} |
69 \end{document} |