588 

   588 You might not like doing proofs. But they serve a very

   589 important purpose in Computer Science: When can we be sure

   590 that our algorithms match their specification. We can try to

   591 test the algorithms, but that often overlooks corner cases and

   592 also often an exhaustive testing is impossible (since there

   593 are often infinitely many inputs). Proofs allow us to ensure

   594 that an algorithm meets its specification. 

   595 

   596 For the programs we look at in this module, the proofs will

   597 mostly by some form of induction. Remember that regular

   598 expressions are defined as 

   599 

   600 \begin{center}

   601 \begin{tabular}{r@{\hspace{1mm}}r@{\hspace{1mm}}l@{\hspace{13mm}}l}

   602   $r$ & $::=$ &   $\varnothing$         & null\\

   603         & $\mid$ & $\epsilon$           & empty string / \texttt{""} / []\\

   604         & $\mid$ & $c$                  & single character\\

   605         & $\mid$ & $r_1 + r_2$          & alternative / choice\\

   606         & $\mid$ & $r_1 \cdot r_2$      & sequence\\

   607         & $\mid$ & $r^*$                & star (zero or more)\\

   608   \end{tabular}

   609 \end{center}

   610 

   611 \noindent If you want to show a property $P(r)$ for all 

   612 regular expressions $r$, then you have to follow essentially 

   613 the recipe:

   614 

   615 \begin{itemize}

   616 \item $P$ has to hold for $\varnothing$, $\epsilon$ and $c$

   617  (these are the base cases).

   618 \item $P$ has to hold for $r_1 + r_2$ under the assumption 

   619    that $P$ already holds for $r_1$ and $r_2$.

   620 \item $P$ has to hold for $r_1 \cdot r_2$ under the 

   621   assumption that $P$ already holds for $r_1$ and $r_2$.

   622 \item $P$ has to hold for $r^*$ under the assumption 

   623   that $P$ already holds for $r$.

   624 \end{itemize}

   625 

   626 \noindent 

   627 A simple proof is for example showing the following 

   628 property:

   629 

   630 \[

   631 nullable(r) \;\;\text{if and only if}\;\; []\in L(r)

   632 \]

   633 

   634 \noindent

   635 Let us say that this property is $P(r)$, then the first case

   636 we need to check is whether $P(\varnothing)$ (see recipe 

   637 above). So we have to show that

   638 

   639 \[

   640 nullable(\varnothing) \;\;\text{if and only if}\;\; 

   641 []\in L(\varnothing)

   642 \]

   643 

   644 \noindent whereby $nullable(\varnothing)$ is by definition of

   645 the function $nullable$ always $\textit{false}$. We also

   646 have that $L(\varnothing)$ is by definition $\{\}$. It is 

   647 impossible that the empty string $[]$ is in the empty set. 

   648 Therefore also the right-hand side is false. Consequently we

   649 verified this case. We would still need to do this for 

   650 $P(\varepsilon)$ and $P(c)$. I leave this to you.