# HG changeset patch # User Christian Urban # Date 1538399088 -3600 # Node ID 4573d36d0b2f057370639e750dfd4df8639c3544 # Parent b153c04834ebfb1a0e6b8347ed60de0dc2082575 updated diff -r b153c04834eb -r 4573d36d0b2f coursework/cw01.pdf Binary file coursework/cw01.pdf has changed diff -r b153c04834eb -r 4573d36d0b2f coursework/cw01.tex --- a/coursework/cw01.tex Mon Oct 01 01:11:42 2018 +0100 +++ b/coursework/cw01.tex Mon Oct 01 14:04:48 2018 +0100 @@ -11,7 +11,7 @@ \section*{Coursework 1 (Strand 1)} This coursework is worth 4\% and is due on 12 October at -16:00. You are asked to implement a regular expression matcher +18:00. You are asked to implement a regular expression matcher and submit a document containing the answers for the questions below. You can do the implementation in any programming language you like, but you need to submit the source code with @@ -62,12 +62,15 @@ $0$. In the case of $r^{\{n,m\}}$ you can also assume $0 \le n \le m$.\bigskip \noindent {\bf Important!} Your implementation should have explicit -cases for the basic regular expressions, but also for explicit cases for -the extended regular expressions. That means do not treat the extended -regular expressions by just translating them into the basic ones. See -also Question 3, where you are asked to explicitly give the rules for -\textit{nullable} and \textit{der} for the extended regular -expressions.\newpage +case classes for the basic regular expressions, but also explicit case +classes for +the extended regular expressions.\footnote{Please call them + \code{RANGE}, \code{PLUS}, \code{OPTIONAL}, \code{NTIMES}, + \code{UPTO}, \code{FROM}, \code{BETWEEN}, \code{NOT} or something + like that.} That means do not treat the extended regular expressions +by just translating them into the basic ones. See also Question 3, +where you are asked to explicitly give the rules for \textit{nullable} +and \textit{der} for the extended regular expressions.\medskip \noindent The meanings of the extended regular expressions are @@ -110,16 +113,18 @@ \subsection*{Question 2 (Unmarked)} -In which programming languages have you written a program (like spent -at least a day working on the program)? +Can you please list all programming languages in which you have +already written programs (like spent at least a good working day +working on the program)? This is just for my curiosity to estimate +what your background is. \subsection*{Question 3} From the lectures you have seen the definitions for the functions \textit{nullable} and \textit{der} for the basic regular -expressions. Implement the rules for the extended regular -expressions: +expressions. Implement and write down rules for the extended +regular expressions: \begin{center} \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}} @@ -192,11 +197,11 @@ \end{center} \noindent -the latter is useful for matching any string (for example +The latter is useful for matching any string (for example by using $\textit{ALL}^*$). In order to avoid having an explicit constructor for each case, we can generalise all these cases and introduce a single constructor $\textit{CFUN}(f)$ where $f$ is a function from characters -to a boolean. The idea is that the function $f$ determines which character(s) +to booleans. The idea is that the function $f$ determines which character(s) are matched, namely those where $f$ returns \texttt{true}. In this question implement \textit{CFUN} and define @@ -217,6 +222,11 @@ \end{tabular} \end{center} +\noindent +You can either add the constructor $CFUN$ to your implementation in +Question 3, or you can implement this questions first +and then use $CFUN$ instead of \code{RANGE} and \code{CHAR} in Question 3. + \subsection*{Question 5} @@ -231,7 +241,7 @@ ([a\mbox{-}z0\mbox{-}9\_\,.-]^+)\cdot @\cdot ([a\mbox{-}z0\mbox{-}9\,.-]^+)\cdot .\cdot ([a\mbox{-}z\,.]^{\{2,6\}}) \] -\noindent and calculate the derivative according to your email +\noindent and calculate the derivative according to your own email address. When calculating the derivative, simplify all regular expressions as much as possible by applying the following 7 simplification rules: @@ -251,9 +261,11 @@ \noindent Write down your simplified derivative in a readable notation using parentheses where necessary. That means you should use the infix notation $+$, $\cdot$, $^*$ and so on, -instead of code.\bigskip - -\noindent +instead of raw code.\bigskip + + +\subsection*{Question 6} + Implement the simplification rules in your regular expression matcher. Consider the regular expression $/ \cdot * \cdot (\sim{}(\textit{ALL}^* \cdot * \cdot / \cdot \textit{ALL}^*)) \cdot * @@ -267,7 +279,7 @@ \item \texttt{"/*test/*test*/"} \end{enumerate} -\subsection*{Question 6} +\subsection*{Question 7} Let $r_1$ be the regular expression $a\cdot a\cdot a$ and $r_2$ be $(a^{\{19,19\}}) \cdot (a^?)$. Decide whether the following three diff -r b153c04834eb -r 4573d36d0b2f coursework/cw02.pdf Binary file coursework/cw02.pdf has changed diff -r b153c04834eb -r 4573d36d0b2f coursework/cw02.tex --- a/coursework/cw02.tex Mon Oct 01 01:11:42 2018 +0100 +++ b/coursework/cw02.tex Mon Oct 01 14:04:48 2018 +0100 @@ -7,7 +7,7 @@ \section*{Coursework 2 (Strand 1)} \noindent This coursework is worth 5\% and is due on 2 -November at 16:00. You are asked to implement the Sulzmann \& +November at 18:00. You are asked to implement the Sulzmann \& Lu lexer for the WHILE language. You can do the implementation in any programming language you like, but you need to submit the source code with which you answered the diff -r b153c04834eb -r 4573d36d0b2f coursework/cw03.pdf Binary file coursework/cw03.pdf has changed diff -r b153c04834eb -r 4573d36d0b2f coursework/cw03.tex --- a/coursework/cw03.tex Mon Oct 01 01:11:42 2018 +0100 +++ b/coursework/cw03.tex Mon Oct 01 14:04:48 2018 +0100 @@ -7,7 +7,7 @@ \section*{Coursework 3} \noindent This coursework is worth 5\% and is due on 23 -November at 16:00. You are asked to implement a parser for the +November at 18:00. You are asked to implement a parser for the WHILE language and also an interpreter. You can do the implementation in any programming language you like, but you need to submit the source code with which you answered the diff -r b153c04834eb -r 4573d36d0b2f coursework/cw04.pdf Binary file coursework/cw04.pdf has changed diff -r b153c04834eb -r 4573d36d0b2f coursework/cw04.tex --- a/coursework/cw04.tex Mon Oct 01 01:11:42 2018 +0100 +++ b/coursework/cw04.tex Mon Oct 01 14:04:48 2018 +0100 @@ -10,7 +10,7 @@ \section*{Coursework 4 (Strand 1)} \noindent This coursework is worth 6\% and is due on 14 -December at 16:00. You are asked to implement a compiler for +December at 18:00. You are asked to implement a compiler for the WHILE language that targets the assembler language provided by Jasmin or Krakatau (both have very similar syntax). You can do the implementation in any programming diff -r b153c04834eb -r 4573d36d0b2f coursework/cw05.pdf Binary file coursework/cw05.pdf has changed diff -r b153c04834eb -r 4573d36d0b2f coursework/cw05.tex --- a/coursework/cw05.tex Mon Oct 01 01:11:42 2018 +0100 +++ b/coursework/cw05.tex Mon Oct 01 14:04:48 2018 +0100 @@ -7,7 +7,7 @@ \section*{Coursework (Strand 2)} \noindent This coursework is worth 20\% and is due on 14 December at -16:00. You are asked to prove the correctness of the regular +18:00. You are asked to prove the correctness of the regular expression matcher from the lectures using the Isabelle theorem prover. You need to submit a theory file containing this proof. The Isabelle theorem prover is available from @@ -19,7 +19,7 @@ \noindent This is an interactive theorem prover, meaning that you can make definitions and state properties, and then help the system with proving these properties. Sometimes the proofs -are also automatic. There is a shortish user guide for +are also completely automatic. There is a shortish user guide for Isabelle, called ``Programming and Proving in Isabelle/HOL'' at @@ -44,29 +44,49 @@ \noindent If you need more help or you are stuck somewhere, -please feel free to contact me (christian.urban@kcl.ac.uk). I +please feel free to contact me (christian.urban at kcl.ac.uk). I am one of the main developers of Isabelle and have used it for -approximately the 16 years. One of the success stories of +approximately 16 years. One of the success stories of Isabelle is the recent verification of a microkernel operating system by an Australian group, see \url{http://sel4.systems}. Their operating system is the only one that has been proved correct according to its specification and is used for application where high assurance, security and reliability is -needed. +needed (like in helicopters which fly over enemy territory). \subsection*{The Task} -In this coursework you are asked to prove the correctness of -the regular expression matcher from the lectures in Isabelle. -For this you need to first specify what the matcher is -supposed to do and then to implement the algorithm. Finally -you need to prove that the algorithm meets the specification. -The first two parts are relatively easy, because the -definitions in Isabelle will look very similar to the -mathematical definitions from the lectures or the Scala code -that is supplied at KEATS. For example very similar to Scala, -regular expressions are defined in Isabelle as an inductive +In this coursework you are asked to prove the correctness of the +regular expression matcher from the lectures in Isabelle. The matcher +should be able to deal with the usual (basic) regular expressions + +\[ +\ZERO,\; \ONE,\; c,\; r_1 + r_2,\; r_1 \cdot r_2,\; r^* +\] + +\noindent +but also with the following extended regular expressions: + +\begin{center} +\begin{tabular}{ll} + $r^{\{n\}}$ & exactly $n$-times\\ + $r^{\{..m\}}$ & zero or more times $r$ but no more than $m$-times\\ + $r^{\{n..\}}$ & at least $n$-times $r$\\ + $r^{\{n..m\}}$ & at least $n$-times $r$ but no more than $m$-times\\ + $\sim{}r$ & not-regular-expression of $r$\\ +\end{tabular} +\end{center} + + +\noindent +You need to first specify what the matcher is +supposed to do and then to implement the algorithm. Finally you need +to prove that the algorithm meets the specification. The first two +parts are relatively easy, because the definitions in Isabelle will +look very similar to the mathematical definitions from the lectures or +the Scala code that is supplied at KEATS. For example very similar to +Scala, regular expressions are defined in Isabelle as an inductive datatype: \begin{lstlisting}[language={},numbers=none] diff -r b153c04834eb -r 4573d36d0b2f slides/slides02.tex --- a/slides/slides02.tex Mon Oct 01 01:11:42 2018 +0100 +++ b/slides/slides02.tex Mon Oct 01 14:04:48 2018 +0100 @@ -277,7 +277,7 @@ \bigskip homework (written exam 80\%)\\ coursework (20\%; first one today)\\ -submission Fridays @ 18:00 -- accepted Mondays +submission Fridays @ 18:00 -- accepted until Mondays \mbox{} \end{frame} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%