7 \section*{Coursework Alternative}

     7 \section*{Coursework (Strand 2)}

     8 

     8 

     9 \noindent

     9 \noindent This coursework is worth 25\% and is due on 12

    10 This coursework is worth 25\% and is due on 12 December at 16:00. You are 

    10 December at 16:00. You are asked to prove the correctness of a

    11 asked to prove the correctness of a regular expression matcher with the 

    11 regular expression matcher from the lectures using the

    12 Isabelle theorem prover. This theorem prover is available from 

    12 Isabelle theorem prover. You need to submit a theory file

    13 containing this proof. The Isabelle theorem prover is

    14 available from 

    18 \noindent

    20 \noindent This is an interactive theorem prover, meaning that

    19 There is a shorte user guide for Isabelle called 

    21 you can make definitions and state properties, and then help

    20 ``Programming and Proving in Isabelle/HOL'' at

    22 the system with proving these properties. Sometimes the proofs

    23 are also automatic. There is a shortish user guide for

    24 Isabelle, called ``Programming and Proving in Isabelle/HOL''

    25 at

    33 \noindent

    38 \noindent The Isabelle theorem prover is operated through the

    34 If you need more help or you are stuck somewhere, please feel free

    39 jEdit IDE, which might not be an editor that is widely known.

    35 to contact me (christian.urban@kcl.ac.uk). I am a main developer of

    40 JEdit is documented in

    36 Isabelle and have used it for approximately the last 14 years.

    41 

    37 

    42 \begin{center}

    38 

    43 \url{http://isabelle.in.tum.de/dist/Isabelle2014/doc/jedit.pdf}

    39 \subsection*{Problem}

    44 \end{center}

    45 

    46 

    47 \noindent If you need more help or you are stuck somewhere,

    48 please feel free to contact me (christian.urban@kcl.ac.uk). I

    49 am a main developer of Isabelle and have used it for

    50 approximately the 14 years. One of the success stories of

    51 Isabelle is the recent verification of a microkernel operating

    52 system by an Australian group, see \url{http://sel4.systems}.

    53 Their operating system is the only one that has been proved

    54 correct according to its specification and is used for

    55 application where high assurance, security and reliability is

    56 needed. 

    57 

    58 

    59 \subsection*{The Task}

    60 

    61 In this coursework you are asked to prove the correctness of

    62 the regular expression matcher from the lectures in Isabelle.

    63 For this you need to first specify what the matcher is

    64 supposed to do and then to implement the algorithm. Finally

    65 you need to prove that the algorithm meets the specification.

    66 The first two parts are relatively easy, because the

    67 definitions in Isabelle will look very similar to the

    68 mathematical definitions from the lectures or the Scala code

    69 that is supplied at KEATS. For example very similar to Scala,

    70 regular expressions are defined in Isabelle as an inductive

    71 datatype:

    72 

    73 \begin{lstlisting}[language={},numbers=none]

    74 datatype rexp =

    75   NULL

    76 | EMPTY

    77 | CHAR char

    78 | SEQ rexp rexp

    79 | ALT rexp rexp

    80 | STAR rexp

    81 \end{lstlisting}

    82 

    83 \noindent The meaning of regular expressions is given as 

    84 usual:

    85 

    86 \begin{center}

    87 \begin{tabular}{rcl@{\hspace{10mm}}l}

    88 $L(\varnothing)$  & $\dn$ & $\varnothing$   & \pcode{NULL}\\

    89 $L(\epsilon)$     & $\dn$ & $\{[]\}$        & \pcode{EMPTY}\\ 

    90 $L(c)$            & $\dn$ & $\{[c]\}$       & \pcode{CHAR}\\

    91 $L(r_1 + r_2)$     & $\dn$ & $L(r_1) \cup L(r_2)$ & \pcode{ALT}\\

    92 $L(r_1 \cdot r_2)$ & $\dn$ & $L(r_1) \,@\, L(r_2)$ & \pcode{SEQ}\\

    93 $L(r^*)$           & $\dn$ & $(L(r))^*$ & \pcode{STAR}\\

    94 \end{tabular}

    95 \end{center}

    96 

    97 \noindent You would need to implement this function in order

    98 to state the theorem about the correctness of the algorithm.

    99 The function $L$ should in Isabelle take a \pcode{rexp} as

   100 input and return a set of strings. Its type is

   101 therefore 

   102 

   103 \begin{center}

   104 \pcode{L} \pcode{::} \pcode{rexp} $\Rightarrow$ \pcode{string set}

   105 \end{center}

   106 

   107 \noindent Isabelle treats strings as an abbreviation for lists

   108 of characters. This means you can pattern-match strings like

   109 lists. The union operation on sets (for the \pcode{ALT}-case)

   110 is a standard definition in Isabelle, but not the

   111 concatenation operation on sets and also not the

   112 star-operation. You would have to supply these definitions.

   113 The concatenation operation can be defined in terms of the

   114 append function, written \code{_ @ _} in Isabelle, for lists.

   115 The star-operation can be defined as a ``big-union'' of 

   116 powers, like in the lectures, or directly as an inductive set.

   117 

   118 The functions for the matcher are shown in

   119 Figure~\ref{matcher}. The theorem that needs to be proved is

   120 

   121 \begin{lstlisting}[numbers=none,language={},keywordstyle=\color{black}\ttfamily,mathescape]

   122 theorem 

   123   "matches r s $\longleftrightarrow$ s $\in$ L r"

   124 \end{lstlisting}

   125 

   126 \noindent which states that the function \emph{matches} is

   127 true if and only if the string is in the language of the

   128 regular expression. A proof for this lemma will need

   129 side-lemmas about \pcode{nullable} and \pcode{der}. An example

   130 proof in Isabelle that will not be relevant for the theorem

   131 above is given in Figure~\ref{proof}.

   132 

   133 \begin{figure}[p]

   134 \begin{lstlisting}[language={},keywordstyle=\color{black}\ttfamily,mathescape]

   135 fun 

   136   nullable :: "rexp $\Rightarrow$ bool"

   137 where

   138   "nullable NULL = False"

   139 | "nullable EMPTY = True"

   140 | "nullable (CHAR _) = False"

   141 | "nullable (ALT r1 r2) = (nullable(r1) $\vee$ nullable(r2))"

   142 | "nullable (SEQ r1 r2) = (nullable(r1) $\wedge$ nullable(r2))"

   143 | "nullable (STAR _) = True"

   144 

   145 fun 

   146   der :: "char $\Rightarrow$ rexp $\Rightarrow$ rexp"

   147 where

   148   "der c NULL = NULL"

   149 | "der c EMPTY = NULL"

   150 | "der c (CHAR d) = (if c = d then EMPTY else NULL)"

   151 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"

   152 | "der c (SEQ r1 r2) = 

   153      (if (nullable r1) then ALT (SEQ (der c r1) r2) (der c r2)

   154                        else SEQ (der c r1) r2)"

   155 | "der c (STAR r) = SEQ (der c r) (STAR r)"

   156 

   157 fun 

   158   ders :: "rexp $\Rightarrow$ string $\Rightarrow$ rexp"

   159 where

   160   "ders r [] = r"

   161 | "ders r (c # s) = ders (der c r) s"

   162 

   163 fun 

   164   matches :: "rexp $\Rightarrow$ string $\Rightarrow$ bool"

   165 where

   166   "matches r s = nullable (ders r s)" 

   167 \end{lstlisting}

   168 \caption{The definition of the matcher algorithm in 

   169 Isabelle.\label{matcher}}

   170 \end{figure}

   171 

   172 \begin{figure}[p]

   173 \begin{lstlisting}[language={},keywordstyle=\color{black}\ttfamily,mathescape]

   174 fun 

   175   zeroable :: "rexp $\Rightarrow$ bool"

   176 where

   177   "zeroable NULL = True"

   178 | "zeroable EMPTY = False"

   179 | "zeroable (CHAR _) = False"

   180 | "zeroable (ALT r1 r2) = (zeroable(r1) $\wedge$ zeroable(r2))"

   181 | "zeroable (SEQ r1 r2) = (zeroable(r1) $\vee$ zeroable(r2))"

   182 | "zeroable (STAR _) = False"

   183 

   184 lemma

   185   "zeroable r $\longleftrightarrow$ L r = {}"

   186 proof (induct)

   187   case (NULL)

   188   have "zeroable NULL" "L NULL = {}" by simp_all

   189   then show "zeroable NULL $\longleftrightarrow$ (L NULL = {})" by simp

   190 next

   191   case (EMPTY)

   192   have "$\neg$ zeroable EMPTY" "L EMPTY = {[]}" by simp_all

   193   then show "zeroable EMPTY $\longleftrightarrow$ (L EMPTY = {})" by simp

   194 next

   195   case (CHAR c)

   196   have "$\neg$ zeroable (CHAR c)" "L (CHAR c) = {[c]}" by simp_all

   197   then show "zeroable (CHAR c) $\longleftrightarrow$ (L (CHAR c) = {})" by simp

   198 next 

   199   case (ALT r1 r2)

   200   have ih1: "zeroable r1 $\longleftrightarrow$ L r1 = {}" by fact

   201   have ih2: "zeroable r2 $\longleftrightarrow$ L r2 = {}" by fact

   202   show "zeroable (ALT r1 r2) $\longleftrightarrow$ (L (ALT r1 r2) = {})" 

   203     using ih1 ih2 by simp

   204 next

   205   case (SEQ r1 r2)

   206   have ih1: "zeroable r1 $\longleftrightarrow$ L r1 = {}" by fact

   207   have ih2: "zeroable r2 $\longleftrightarrow$ L r2 = {}" by fact

   208   show "zeroable (SEQ r1 r2) $\longleftrightarrow$ (L (SEQ r1 r2) = {})" 

   209     using ih1 ih2 by (auto simp add: Conc_def)

   210 next

   211   case (STAR r)

   212   have "$\neg$ zeroable (STAR r)" "[] $\in$ L (r) ^ 0" by simp_all

   213   then show "zeroable (STAR r) $\longleftrightarrow$ (L (STAR r) = {})" 

   214     by (simp (no_asm) add: Star_def) blast

   215 qed

   216 \end{lstlisting}

   217 \caption{An Isabelle proof about the function \pcode{zeroable}.\label{proof}}

   218 \end{figure}