4 |
4 |
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 25\% and is due on 11 |
9 \noindent This coursework is worth 20\% and is due on 13 December at |
10 December at 16:00. You are asked to prove the correctness of |
10 16:00. You are asked to prove the correctness of the regular |
11 the |
11 expression matcher from the lectures using the Isabelle theorem |
12 regular expression matcher from the lectures using the |
12 prover. You need to submit a theory file containing this proof. The |
13 Isabelle theorem prover. You need to submit a theory file |
13 Isabelle theorem prover is available from |
14 containing this proof. The Isabelle theorem prover is |
|
15 available from |
|
16 |
14 |
17 \begin{center} |
15 \begin{center} |
18 \url{http://isabelle.in.tum.de} |
16 \url{http://isabelle.in.tum.de} |
19 \end{center} |
17 \end{center} |
20 |
18 |
45 \end{center} |
43 \end{center} |
46 |
44 |
47 |
45 |
48 \noindent If you need more help or you are stuck somewhere, |
46 \noindent If you need more help or you are stuck somewhere, |
49 please feel free to contact me (christian.urban@kcl.ac.uk). I |
47 please feel free to contact me (christian.urban@kcl.ac.uk). I |
50 am a main developer of Isabelle and have used it for |
48 am one of the main developers of Isabelle and have used it for |
51 approximately the 14 years. One of the success stories of |
49 approximately the 16 years. One of the success stories of |
52 Isabelle is the recent verification of a microkernel operating |
50 Isabelle is the recent verification of a microkernel operating |
53 system by an Australian group, see \url{http://sel4.systems}. |
51 system by an Australian group, see \url{http://sel4.systems}. |
54 Their operating system is the only one that has been proved |
52 Their operating system is the only one that has been proved |
55 correct according to its specification and is used for |
53 correct according to its specification and is used for |
56 application where high assurance, security and reliability is |
54 application where high assurance, security and reliability is |
84 \noindent The meaning of regular expressions is given as |
82 \noindent The meaning of regular expressions is given as |
85 usual: |
83 usual: |
86 |
84 |
87 \begin{center} |
85 \begin{center} |
88 \begin{tabular}{rcl@{\hspace{10mm}}l} |
86 \begin{tabular}{rcl@{\hspace{10mm}}l} |
89 $L(\varnothing)$ & $\dn$ & $\varnothing$ & \pcode{NULL}\\ |
87 $L(\ZERO)$ & $\dn$ & $\varnothing$ & \pcode{ZERO}\\ |
90 $L(\epsilon)$ & $\dn$ & $\{[]\}$ & \pcode{EMPTY}\\ |
88 $L(\ONE)$ & $\dn$ & $\{[]\}$ & \pcode{ONE}\\ |
91 $L(c)$ & $\dn$ & $\{[c]\}$ & \pcode{CHAR}\\ |
89 $L(c)$ & $\dn$ & $\{[c]\}$ & \pcode{CHAR}\\ |
92 $L(r_1 + r_2)$ & $\dn$ & $L(r_1) \cup L(r_2)$ & \pcode{ALT}\\ |
90 $L(r_1 + r_2)$ & $\dn$ & $L(r_1) \cup L(r_2)$ & \pcode{ALT}\\ |
93 $L(r_1 \cdot r_2)$ & $\dn$ & $L(r_1) \,@\, L(r_2)$ & \pcode{SEQ}\\ |
91 $L(r_1 \cdot r_2)$ & $\dn$ & $L(r_1) \,@\, L(r_2)$ & \pcode{SEQ}\\ |
94 $L(r^*)$ & $\dn$ & $(L(r))^*$ & \pcode{STAR}\\ |
92 $L(r^*)$ & $\dn$ & $(L(r))^*$ & \pcode{STAR}\\ |
95 \end{tabular} |
93 \end{tabular} |
134 \begin{figure}[p] |
132 \begin{figure}[p] |
135 \begin{lstlisting}[language={},keywordstyle=\color{black}\ttfamily,mathescape] |
133 \begin{lstlisting}[language={},keywordstyle=\color{black}\ttfamily,mathescape] |
136 fun |
134 fun |
137 nullable :: "rexp $\Rightarrow$ bool" |
135 nullable :: "rexp $\Rightarrow$ bool" |
138 where |
136 where |
139 "nullable NULL = False" |
137 "nullable ZERO = False" |
140 | "nullable EMPTY = True" |
138 | "nullable ONE = True" |
141 | "nullable (CHAR _) = False" |
139 | "nullable (CHAR _) = False" |
142 | "nullable (ALT r1 r2) = (nullable(r1) $\vee$ nullable(r2))" |
140 | "nullable (ALT r1 r2) = (nullable(r1) $\vee$ nullable(r2))" |
143 | "nullable (SEQ r1 r2) = (nullable(r1) $\wedge$ nullable(r2))" |
141 | "nullable (SEQ r1 r2) = (nullable(r1) $\wedge$ nullable(r2))" |
144 | "nullable (STAR _) = True" |
142 | "nullable (STAR _) = True" |
145 |
143 |
146 fun |
144 fun |
147 der :: "char $\Rightarrow$ rexp $\Rightarrow$ rexp" |
145 der :: "char $\Rightarrow$ rexp $\Rightarrow$ rexp" |
148 where |
146 where |
149 "der c NULL = NULL" |
147 "der c ZERO = ZERO" |
150 | "der c EMPTY = NULL" |
148 | "der c ONE = ZERO" |
151 | "der c (CHAR d) = (if c = d then EMPTY else NULL)" |
149 | "der c (CHAR d) = (if c = d then ONE else ZERO)" |
152 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
150 | "der c (ALT r1 r2) = ALT (der c r1) (der c r2)" |
153 | "der c (SEQ r1 r2) = |
151 | "der c (SEQ r1 r2) = |
154 (if (nullable r1) then ALT (SEQ (der c r1) r2) (der c r2) |
152 (if (nullable r1) then ALT (SEQ (der c r1) r2) (der c r2) |
155 else SEQ (der c r1) r2)" |
153 else SEQ (der c r1) r2)" |
156 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
154 | "der c (STAR r) = SEQ (der c r) (STAR r)" |
173 \begin{figure}[p] |
171 \begin{figure}[p] |
174 \begin{lstlisting}[language={},keywordstyle=\color{black}\ttfamily,mathescape] |
172 \begin{lstlisting}[language={},keywordstyle=\color{black}\ttfamily,mathescape] |
175 fun |
173 fun |
176 zeroable :: "rexp $\Rightarrow$ bool" |
174 zeroable :: "rexp $\Rightarrow$ bool" |
177 where |
175 where |
178 "zeroable NULL = True" |
176 "zeroable ZERO = True" |
179 | "zeroable EMPTY = False" |
177 | "zeroable ONE = False" |
180 | "zeroable (CHAR _) = False" |
178 | "zeroable (CHAR _) = False" |
181 | "zeroable (ALT r1 r2) = (zeroable(r1) $\wedge$ zeroable(r2))" |
179 | "zeroable (ALT r1 r2) = (zeroable(r1) $\wedge$ zeroable(r2))" |
182 | "zeroable (SEQ r1 r2) = (zeroable(r1) $\vee$ zeroable(r2))" |
180 | "zeroable (SEQ r1 r2) = (zeroable(r1) $\vee$ zeroable(r2))" |
183 | "zeroable (STAR _) = False" |
181 | "zeroable (STAR _) = False" |
184 |
182 |
185 lemma |
183 lemma |
186 "zeroable r $\longleftrightarrow$ L r = {}" |
184 "zeroable r $\longleftrightarrow$ L r = {}" |
187 proof (induct) |
185 proof (induct) |
188 case (NULL) |
186 case (ZERO) |
189 have "zeroable NULL" "L NULL = {}" by simp_all |
187 have "zeroable ZERO" "L ZERO = {}" by simp_all |
190 then show "zeroable NULL $\longleftrightarrow$ (L NULL = {})" by simp |
188 then show "zeroable ZERO $\longleftrightarrow$ (L ZERO = {})" by simp |
191 next |
189 next |
192 case (EMPTY) |
190 case (ONE) |
193 have "$\neg$ zeroable EMPTY" "L EMPTY = {[]}" by simp_all |
191 have "$\neg$ zeroable ONE" "L ONE = {[]}" by simp_all |
194 then show "zeroable EMPTY $\longleftrightarrow$ (L EMPTY = {})" by simp |
192 then show "zeroable ONE $\longleftrightarrow$ (L ONE = {})" by simp |
195 next |
193 next |
196 case (CHAR c) |
194 case (CHAR c) |
197 have "$\neg$ zeroable (CHAR c)" "L (CHAR c) = {[c]}" by simp_all |
195 have "$\neg$ zeroable (CHAR c)" "L (CHAR c) = {[c]}" by simp_all |
198 then show "zeroable (CHAR c) $\longleftrightarrow$ (L (CHAR c) = {})" by simp |
196 then show "zeroable (CHAR c) $\longleftrightarrow$ (L (CHAR c) = {})" by simp |
199 next |
197 next |