Binary file coursework/cw01.pdf has changed

--- 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

Binary file coursework/cw02.pdf has changed

--- 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

Binary file coursework/cw03.pdf has changed

--- 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

Binary file coursework/cw04.pdf has changed

--- 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

Binary file coursework/cw05.pdf has changed

--- 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]

--- 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}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%