5 \begin{document} |
5 \begin{document} |
6 |
6 |
7 \section*{Coursework (Strand 2)} |
7 \section*{Coursework (Strand 2)} |
8 |
8 |
9 \noindent This coursework is worth 20\% and is due on 14 December at |
9 \noindent This coursework is worth 20\% and is due on 14 December at |
10 16:00. You are asked to prove the correctness of the regular |
10 18:00. You are asked to prove the correctness of the regular |
11 expression matcher from the lectures using the Isabelle theorem |
11 expression matcher from the lectures using the Isabelle theorem |
12 prover. You need to submit a theory file containing this proof. The |
12 prover. You need to submit a theory file containing this proof. The |
13 Isabelle theorem prover is available from |
13 Isabelle theorem prover is available from |
14 |
14 |
15 \begin{center} |
15 \begin{center} |
17 \end{center} |
17 \end{center} |
18 |
18 |
19 \noindent This is an interactive theorem prover, meaning that |
19 \noindent This is an interactive theorem prover, meaning that |
20 you can make definitions and state properties, and then help |
20 you can make definitions and state properties, and then help |
21 the system with proving these properties. Sometimes the proofs |
21 the system with proving these properties. Sometimes the proofs |
22 are also automatic. There is a shortish user guide for |
22 are also completely automatic. There is a shortish user guide for |
23 Isabelle, called ``Programming and Proving in Isabelle/HOL'' |
23 Isabelle, called ``Programming and Proving in Isabelle/HOL'' |
24 at |
24 at |
25 |
25 |
26 \begin{center} |
26 \begin{center} |
27 \url{http://isabelle.in.tum.de/documentation.html} |
27 \url{http://isabelle.in.tum.de/documentation.html} |
42 \url{http://isabelle.in.tum.de/dist/Isabelle2014/doc/jedit.pdf} |
42 \url{http://isabelle.in.tum.de/dist/Isabelle2014/doc/jedit.pdf} |
43 \end{center} |
43 \end{center} |
44 |
44 |
45 |
45 |
46 \noindent If you need more help or you are stuck somewhere, |
46 \noindent If you need more help or you are stuck somewhere, |
47 please feel free to contact me (christian.urban@kcl.ac.uk). I |
47 please feel free to contact me (christian.urban at kcl.ac.uk). I |
48 am one of the main developers of Isabelle and have used it for |
48 am one of the main developers of Isabelle and have used it for |
49 approximately the 16 years. One of the success stories of |
49 approximately 16 years. One of the success stories of |
50 Isabelle is the recent verification of a microkernel operating |
50 Isabelle is the recent verification of a microkernel operating |
51 system by an Australian group, see \url{http://sel4.systems}. |
51 system by an Australian group, see \url{http://sel4.systems}. |
52 Their operating system is the only one that has been proved |
52 Their operating system is the only one that has been proved |
53 correct according to its specification and is used for |
53 correct according to its specification and is used for |
54 application where high assurance, security and reliability is |
54 application where high assurance, security and reliability is |
55 needed. |
55 needed (like in helicopters which fly over enemy territory). |
56 |
56 |
57 |
57 |
58 \subsection*{The Task} |
58 \subsection*{The Task} |
59 |
59 |
60 In this coursework you are asked to prove the correctness of |
60 In this coursework you are asked to prove the correctness of the |
61 the regular expression matcher from the lectures in Isabelle. |
61 regular expression matcher from the lectures in Isabelle. The matcher |
62 For this you need to first specify what the matcher is |
62 should be able to deal with the usual (basic) regular expressions |
63 supposed to do and then to implement the algorithm. Finally |
63 |
64 you need to prove that the algorithm meets the specification. |
64 \[ |
65 The first two parts are relatively easy, because the |
65 \ZERO,\; \ONE,\; c,\; r_1 + r_2,\; r_1 \cdot r_2,\; r^* |
66 definitions in Isabelle will look very similar to the |
66 \] |
67 mathematical definitions from the lectures or the Scala code |
67 |
68 that is supplied at KEATS. For example very similar to Scala, |
68 \noindent |
69 regular expressions are defined in Isabelle as an inductive |
69 but also with the following extended regular expressions: |
|
70 |
|
71 \begin{center} |
|
72 \begin{tabular}{ll} |
|
73 $r^{\{n\}}$ & exactly $n$-times\\ |
|
74 $r^{\{..m\}}$ & zero or more times $r$ but no more than $m$-times\\ |
|
75 $r^{\{n..\}}$ & at least $n$-times $r$\\ |
|
76 $r^{\{n..m\}}$ & at least $n$-times $r$ but no more than $m$-times\\ |
|
77 $\sim{}r$ & not-regular-expression of $r$\\ |
|
78 \end{tabular} |
|
79 \end{center} |
|
80 |
|
81 |
|
82 \noindent |
|
83 You need to first specify what the matcher is |
|
84 supposed to do and then to implement the algorithm. Finally you need |
|
85 to prove that the algorithm meets the specification. The first two |
|
86 parts are relatively easy, because the definitions in Isabelle will |
|
87 look very similar to the mathematical definitions from the lectures or |
|
88 the Scala code that is supplied at KEATS. For example very similar to |
|
89 Scala, regular expressions are defined in Isabelle as an inductive |
70 datatype: |
90 datatype: |
71 |
91 |
72 \begin{lstlisting}[language={},numbers=none] |
92 \begin{lstlisting}[language={},numbers=none] |
73 datatype rexp = |
93 datatype rexp = |
74 ZERO |
94 ZERO |