39 |
39 |
40 \begin{document} |
40 \begin{document} |
41 \renewcommand{\thefootnote}{$\star$} \footnotetext[1]{This paper is a |
41 \renewcommand{\thefootnote}{$\star$} \footnotetext[1]{This paper is a |
42 revised and expanded version of \cite{AusafDyckhoffUrban2016}. |
42 revised and expanded version of \cite{AusafDyckhoffUrban2016}. |
43 Compared with that paper we give a second definition for POSIX |
43 Compared with that paper we give a second definition for POSIX |
44 values introduced by Okui Suzuki \cite{OkuiSuzuki2013} and prove that it is |
44 values introduced by Okui Suzuki \cite{OkuiSuzuki2010,OkuiSuzukiTech} |
|
45 and prove that it is |
45 equivalent to our original one. This |
46 equivalent to our original one. This |
46 second definition is based on an ordering of values and very similar to, |
47 second definition is based on an ordering of values and very similar to, |
47 but not equivalent with, the |
48 but not equivalent with, the |
48 definition given by Sulzmann and Lu~\cite{Sulzmann2014}. We also |
49 definition given by Sulzmann and Lu~\cite{Sulzmann2014}. |
|
50 The advantage of the definition based on the |
|
51 ordering is that it implements more directly the informal rules from the |
|
52 POSIX standard. |
|
53 We also |
49 extend our results to additional constructors of regular |
54 extend our results to additional constructors of regular |
50 expressions.} \renewcommand{\thefootnote}{\arabic{footnote}} |
55 expressions.} \renewcommand{\thefootnote}{\arabic{footnote}} |
51 |
56 |
52 |
57 |
53 \title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions} |
58 \title{POSIX {L}exing with {D}erivatives of {R}egular {E}xpressions} |
73 regular expression matches the string). We also prove the correctness |
78 regular expression matches the string). We also prove the correctness |
74 of an optimised version of the POSIX matching algorithm. In the |
79 of an optimised version of the POSIX matching algorithm. In the |
75 second part we show that $(iii)$ our inductive definition of a POSIX |
80 second part we show that $(iii)$ our inductive definition of a POSIX |
76 value is equivalent to an alternative definition by Okui and Suzuki |
81 value is equivalent to an alternative definition by Okui and Suzuki |
77 which identifies POSIX values as least elements according to an |
82 which identifies POSIX values as least elements according to an |
78 ordering of values. The advantage of the definition based on the |
83 ordering of values. \smallskip |
79 ordering is that it implements more directly the informal rules from the |
|
80 POSIX standard.\smallskip |
|
81 |
84 |
82 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions, |
85 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions, |
83 Isabelle/HOL |
86 Isabelle/HOL |
84 \end{abstract} |
87 \end{abstract} |
85 |
88 |