23 \newcommand{\sflataux}[1]{\llparenthesis #1 \rrparenthesis'} |
23 \newcommand{\sflataux}[1]{\llparenthesis #1 \rrparenthesis'} |
24 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% |
24 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% |
25 \newcommand{\ZERO}{\mbox{\bf 0}} |
25 \newcommand{\ZERO}{\mbox{\bf 0}} |
26 \newcommand{\ONE}{\mbox{\bf 1}} |
26 \newcommand{\ONE}{\mbox{\bf 1}} |
27 \newcommand{\AALTS}[2]{\oplus {\scriptstyle #1}\, #2} |
27 \newcommand{\AALTS}[2]{\oplus {\scriptstyle #1}\, #2} |
|
28 \newcommand{\rdistinct}[2]{\textit{distinct} \; \textit{#1} \; #2} |
|
29 \newcommand\hflat[1]{\llparenthesis #1 \rrparenthesis_*} |
|
30 \newcommand\hflataux[1]{\llparenthesis #1 \rrparenthesis_*'} |
|
31 \newcommand\createdByStar[1]{\textit{\textit{createdByStar}(#1)}} |
28 |
32 |
29 \newcommand\myequiv{\mathrel{\stackrel{\makebox[0pt]{\mbox{\normalfont\tiny equiv}}}{=}}} |
33 \newcommand\myequiv{\mathrel{\stackrel{\makebox[0pt]{\mbox{\normalfont\tiny equiv}}}{=}}} |
30 |
34 |
31 \def\lexer{\mathit{lexer}} |
35 \def\lexer{\mathit{lexer}} |
32 \def\mkeps{\mathit{mkeps}} |
36 \def\mkeps{\mathit{mkeps}} |
|
37 \newcommand{\rder}[2]{#2 \backslash #1} |
33 |
38 |
34 \def\AZERO{\textit{AZERO}} |
39 \def\AZERO{\textit{AZERO}} |
35 \def\AONE{\textit{AONE}} |
40 \def\AONE{\textit{AONE}} |
36 \def\ACHAR{\textit{ACHAR}} |
41 \def\ACHAR{\textit{ACHAR}} |
37 |
42 |
83 \newcommand\RCHAR[1]{\mathbf{#1}_r} |
88 \newcommand\RCHAR[1]{\mathbf{#1}_r} |
84 \newcommand\RSEQ[2]{#1 \cdot #2} |
89 \newcommand\RSEQ[2]{#1 \cdot #2} |
85 \newcommand\RALTS[1]{\oplus #1} |
90 \newcommand\RALTS[1]{\oplus #1} |
86 \newcommand\RSTAR[1]{#1^*} |
91 \newcommand\RSTAR[1]{#1^*} |
87 \newcommand\vsuf[2]{\textit{vsuf} \;#1\;#2} |
92 \newcommand\vsuf[2]{\textit{vsuf} \;#1\;#2} |
|
93 |
88 %---------------------------------------------------------------------------------------- |
94 %---------------------------------------------------------------------------------------- |
89 %This part is about regular expressions, Brzozowski derivatives, |
95 %This part is about regular expressions, Brzozowski derivatives, |
90 %and a bit-coded lexing algorithm with proven correctness and time bounds. |
96 %and a bit-coded lexing algorithm with proven correctness and time bounds. |
91 |
97 |
92 %TODO: look up snort rules to use here--give readers idea of what regexes look like |
98 %TODO: look up snort rules to use here--give readers idea of what regexes look like |
876 POSIX matching as a ternary relation recursively defined in a |
882 POSIX matching as a ternary relation recursively defined in a |
877 natural deduction style. |
883 natural deduction style. |
878 With the formally-specified rules for what a POSIX matching is, |
884 With the formally-specified rules for what a POSIX matching is, |
879 they proved in Isabelle/HOL that the algorithm gives correct results. |
885 they proved in Isabelle/HOL that the algorithm gives correct results. |
880 |
886 |
881 But having a correct result is still not enough, we want $\mathbf{efficiency}$. |
887 But having a correct result is still not enough, |
|
888 we want at least some degree of $\mathbf{efficiency}$. |
882 |
889 |
883 |
890 |
884 |
891 |
885 One regular expression can have multiple lexical values. For example |
892 One regular expression can have multiple lexical values. For example |
886 for the regular expression $(a+b)^*$, it has a infinite list of |
893 for the regular expression $(a+b)^*$, it has a infinite list of |