afl-material: comparison handouts/ho01.tex

equal deleted inserted replaced

-:4ae59fd3b174
+:357c395ae838
 Also often we face the problem that we are given a string (for
 example some user input) and want to know whether it matches a
 particular pattern---be it an email address, for example. In
 this way we can exclude user input that would otherwise have
 nasty effects on our program (crashing it or making it go into
-an infinite loop, if not worse).
+an infinite loop, if not worse).\smallskip
 \defn{Regular expressions} help with conveniently specifying
 such patterns. The idea behind regular expressions is that
 they are a simple method for describing languages (or sets of
 strings)\ldots at least languages we are interested in in
 ``8 Regular Expressions You Should Know''
 \url{http://goo.gl/5LoVX7}} Consider the following regular
 expression
 \begin{equation}\label{email}
-\texttt{[a-z0-9\_.-]+ @ [a-z0-9.-]+ . [a-z.]\{2,6\}}
+\texttt{[a-z0-9\_.-]+} \;\;\texttt{@}\;\; \texttt{[a-z0-9.-]+} \;\;\texttt{.}\;\; \texttt{[a-z.]\{2,6\}}
 \end{equation}
-\noindent where the first part matches one or more lowercase
+\noindent where the first part, the user name, matches one or more lowercase
 letters (\pcode{a-z}), digits (\pcode{0-9}), underscores, dots
 and hyphens. The \pcode{+} at the end of the brackets ensures
 the ``one or more''. Then comes the \pcode{@}-sign, followed
 by the domain name which must be one or more lowercase
 letters, digits, underscores, dots or hyphens. Note there
 \end{center}
 \noindent With this table you can figure out the purpose of
 the regular expressions in the web-crawlers shown Figures
 \ref{crawler1}, \ref{crawler2} and
-\ref{crawler3}.\footnote{There is an interesting twist in the
+\ref{crawler3}. Note, however, the regular expression for
-web-scraper where \pcode{re*?} is used instead of
-\pcode{re*}.} Note, however, the regular expression for
 http-addresses in web-pages in Figure~\ref{crawler1}, Line 15,
 is intended to be
 \[
 \pcode{"https?://[^"]*"}
 then is there any interest in studying them again in depth in
 this module? Well, one answer is in the following two graphs about
 regular expression matching in Python, Ruby and Java.
 \begin{center}
-\begin{tabular}{@{}cc@{}}
+\begin{tabular}{@{\hspace{-1mm}}c@{\hspace{-1mm}}c@{}}
 \begin{tikzpicture}
 \begin{axis}[
 title={Graph: $\texttt{a?\{n\}\,a{\{n\}}}$ and strings
 $\underbrace{\texttt{a}\ldots \texttt{a}}_{n}$},
 xlabel={$n$},
 \begin{center}
 \url{http://stackstatus.net/post/147710624694/outage-postmortem-july-20-2016}
 \end{center}
 \noindent
+It was also a problem in the Atom editor
+\begin{center}
+\url{http://davidvgalbraith.com/how-i-fixed-atom/}
+\end{center}
+\noindent
 Such troublesome regular expressions are sometimes called \emph{evil
 regular expressions} because they have the potential to make regular
 expression matching engines to topple over, like in Python, Ruby and
-Java. This `toopling over' is also sometimes called \emph{catastrophic
+Java. This ``toppling over'' is also sometimes called \emph{catastrophic
 backtracking}.  The problem with evil regular expressions is that
 they can have some serious consequences, for example, if you use them
 in your web-application. The reason is that hackers can look for these
 instances where the matching engine behaves badly and then mount a
 nice DoS-attack against your application. These attacks are already
 have their own name: \emph{Regular Expression Denial of Service
 Attacks (ReDoS)}.
 It will be instructive to look behind the ``scenes'' to find
 out why Python and Ruby (and others) behave so badly when
-matching with evil regular expressions. But we will also look
+matching strings with evil regular expressions. But we will also look
 at a relatively simple algorithm that solves this problem much
 better than Python and Ruby do\ldots actually it will be two
 versions of the algorithm: the first one will be able to
 process strings of approximately 1,000 \texttt{a}s in 30
 seconds, while the second version will even be able to process
 \[
 A\star\dn \bigcup_{0\le n} A^n
 \]
-\noindent
-Note that this expands to
-\[
-A\star \dn A^0 \cup A^1 \cup A^2 \cup A^3 \cup A^4 \cup \ldots
-\]
-\noindent which is equivalent to
-\[
-A\star \dn \{[]\} \cup A \cup A@A \cup A@A@A \cup A@A@A@A \cup \ldots
-\]
-\noindent
-Remember that $A^0$ is always the set containing the empty
-string.
 We will use parentheses to disambiguate regular expressions.
 Parentheses are not really part of a regular expression, and
 indeed we do not need them in our code because there the tree
 structure of regular expressions is always clear. But for
 for the last 14 years has been with theorem provers. I am a
 core developer of one of
 them.\footnote{\url{http://isabelle.in.tum.de}} Theorem
 provers are systems in which you can formally reason about
 mathematical concepts, but also about programs. In this way
-they can help with writing bug-free code. Theorem provers have
+theorem prover can help with the manacing problem of writing bug-free code. Theorem provers have
-proved already their value in a number of systems (even in
+proved already their value in a number of cases (even in
 terms of hard cash), but they are still clunky and difficult
 to use by average programmers.
 Anyway, in about 2011 I came across the notion of
 \defn{derivatives of regular expressions}. This notion allows
 one to do almost all calculations in regular language theory
-on the level of regular expressions, not needing any automata.
+on the level of regular expressions, not needing any automata (you will
-This is important because automata are graphs and it is rather
+see we only touch briefly on automata in lecture 3).
+This is crucial because automata are graphs and it is rather
 difficult to reason about graphs in theorem provers. In
-contrast, to reason about regular expressions is easy-peasy in
+contrast, reasoning about regular expressions is easy-peasy in
 theorem provers. Is this important? I think yes, because
 according to Kuklewicz nearly all POSIX-based regular
 expression matchers are
 buggy.\footnote{\url{http://www.haskell.org/haskellwiki/Regex_Posix}}
-With my PhD student Fahad Ausaf I am currently working on
+With my PhD student Fahad Ausaf I proved
-proving the correctness for one such matcher that was
+the correctness for one such matcher that was
 proposed by Sulzmann and Lu in
-2014.\footnote{\url{http://goo.gl/bz0eHp}} This would be an
+2014.\footnote{\url{http://goo.gl/bz0eHp}} Hopefully we can
-attractive results since we will be able to prove that the
+prove that the machine code(!)
-algorithm is really correct, but also that the machine code(!)
 that implements this code efficiently is correct. Writing
 programs in this way does not leave any room for potential
 errors or bugs. How nice!
 What also helped with my fascination with regular expressions
 is that we could indeed find out new things about them that
-have surprised some experts in the field of regular
+have surprised some experts. Together with two colleagues from China, I was
-expressions. Together with two colleagues from China, I was
 able to prove the Myhill-Nerode theorem by only using regular
 expressions and the notion of derivatives. Earlier versions of
 this theorem used always automata in the proof. Using this
 theorem we can show that regular languages are closed under
 complementation, something which Gasarch in his
 What a feeling if you are an outsider to the subject!
 To conclude: Despite my early ignorance about regular
 expressions, I find them now very interesting. They have a
 beautiful mathematical theory behind them, which can be
-sometimes quite deep and contain hidden snares. They have
+sometimes quite deep and which contains hidden snares. They have
 practical importance (remember the shocking runtime of the
-regular expression matchers in Python and Ruby in some
+regular expression matchers in Python, Ruby and Java in some
-instances). People who are not very familiar with the
+instances) and the problems in Stack Exchange and the Atom editor.
+People who are not very familiar with the
 mathematical background of regular expressions get them
 consistently wrong. The hope is that we can do better in the
 future---for example by proving that the algorithms actually
 satisfy their specification and that the corresponding
 implementations do not contain any bugs. We are close, but not
 the syntax of email addresses. With their proposed regular
 expression they are too strict in some cases and too lax in
 others. Not a good situation to be in. A regular expression
 that is claimed to be closer to the standard is shown in
 Figure~\ref{monster}. Whether this claim is true or not, I
-would not know---the only thing I can say to this regular
+would not know---the only thing I can say about this regular
 expression is it is a monstrosity. However, this might
 actually be an argument against the RFC standard, rather than
 against regular expressions. A similar argument is made in
 \begin{center}
 \lstinputlisting[language={},keywordstyle=\color{black},numbers=none]{../progs/email-rexp}
 \end{minipage}
 \end{center}
 \caption{Nothing that can be said about this regular
-expression\ldots\label{monster}}
+expression\ldots{}except it is a monstrosity.\label{monster}}
 \end{figure}
 \end{document}

changeset 416	357c395ae838
parent 415	4ae59fd3b174
child 417	e74c696821a2