70 expressions. They can be used for a very simple regular expression |
70 expressions. They can be used for a very simple regular expression |
71 matching algorithm. Sulzmann and Lu cleverly extended this algorithm |
71 matching algorithm. Sulzmann and Lu cleverly extended this algorithm |
72 in order to deal with POSIX matching, which is the underlying |
72 in order to deal with POSIX matching, which is the underlying |
73 disambiguation strategy for regular expressions needed in lexers. |
73 disambiguation strategy for regular expressions needed in lexers. |
74 Their algorithm generates POSIX values which encode the information of |
74 Their algorithm generates POSIX values which encode the information of |
75 \emph{how} a regular expression matched a string---that is which part |
75 \emph{how} a regular expression matched a string---that is, which part |
76 of the string is matched by which part of the regular expression. In |
76 of the string is matched by which part of the regular expression. In |
77 the first part of this paper we give our inductive definition of what |
77 this paper we give our inductive definition of what a POSIX value is |
78 a POSIX value is and show $(i)$ that such a value is unique (for given |
78 and show $(i)$ that such a value is unique (for given regular |
79 regular expression and string being matched) and $(ii)$ that Sulzmann |
79 expression and string being matched) and $(ii)$ that Sulzmann and Lu's |
80 and Lu's algorithm always generates such a value (provided that the |
80 algorithm always generates such a value (provided that the regular |
81 regular expression matches the string). We also prove the correctness |
81 expression matches the string). We show that $(iii)$ our inductive |
82 of an optimised version of the POSIX matching algorithm. In the |
82 definition of a POSIX value is equivalent to an alternative definition |
83 second part we show that $(iii)$ our inductive definition of a POSIX |
83 by Okui and Suzuki which identifies POSIX values as least elements |
84 value is equivalent to an alternative definition by Okui and Suzuki |
84 according to an ordering of values. We also prove the correctness of |
85 which identifies POSIX values as least elements according to an |
85 an optimised version of the POSIX matching algorithm. \smallskip |
86 ordering of values. \smallskip |
|
87 |
86 |
88 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions, |
87 {\bf Keywords:} POSIX matching, Derivatives of Regular Expressions, |
89 Isabelle/HOL |
88 Isabelle/HOL |
90 \end{abstract} |
89 \end{abstract} |
91 |
90 |