Binary file coursework/cw04.pdf has changed
--- a/coursework/cw04.tex Tue Sep 01 12:44:07 2020 +0100
+++ b/coursework/cw04.tex Tue Sep 01 15:57:55 2020 +0100
@@ -11,9 +11,9 @@
% Jasmin Tutorial
%http://saksagan.ceng.metu.edu.tr/courses/ceng444/link/jvm-cpm.html
-\section*{Coursework 4 (Strand 1)}
+\section*{Coursework 4}
-\noindent This coursework is worth 6\% and is due on \cwFOUR{}
+\noindent This coursework is worth 10\% and is due on \cwFOUR{}
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
@@ -25,7 +25,7 @@
a zip-file that creates a directory with the name
\texttt{YournameYourFamilyname} on my end.
-\subsection*{Disclaimer}
+\subsection*{Disclaimer\alert}
It should be understood that the work you submit represents
your own effort. You have not copied from anyone else. An
@@ -146,7 +146,7 @@
a file that can be run, not as PDF-text.
\begin{figure}[t]
-\lstinputlisting[language=while]{../progs/fib.while}
+\lstinputlisting[language=while]{../progs/while-tests/fib.while}
\caption{The Fibonacci program in the WHILE language.\label{fibs}}
\end{figure}
Binary file coursework/cw05.pdf has changed
--- a/coursework/cw05.tex Tue Sep 01 12:44:07 2020 +0100
+++ b/coursework/cw05.tex Tue Sep 01 15:57:55 2020 +0100
@@ -5,237 +5,33 @@
\begin{document}
-\section*{Coursework (Strand 2)}
-
-\noindent This coursework is worth 20\% and is due on \cwISABELLE{} at
-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 and also a document
-describing your proof. The Isabelle theorem prover is available from
-
-\begin{center}
-\url{http://isabelle.in.tum.de}
-\end{center}
-
-\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 completely automatic. There is a shortish user guide for
-Isabelle, called ``Programming and Proving in Isabelle/HOL''
-at
-
-\begin{center}
-\url{http://isabelle.in.tum.de/documentation.html}
-\end{center}
-
-\noindent
-and also a longer (free) book at
-
-\begin{center}
-\url{http://www.concrete-semantics.org}
-\end{center}
-
-\noindent The Isabelle theorem prover is operated through the
-jEdit IDE, which might not be an editor that is widely known.
-JEdit is documented in
+\section*{Coursework 5}
-\begin{center}
-\url{http://isabelle.in.tum.de/dist/Isabelle2014/doc/jedit.pdf}
-\end{center}
-
-
-\noindent If you need more help or you are stuck somewhere,
-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 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 (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. 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]
-datatype rexp =
- ZERO
-| ONE
-| CHAR char
-| SEQ rexp rexp
-| ALT rexp rexp
-| STAR rexp
-\end{lstlisting}
-
-\noindent The meaning of regular expressions is given as
-usual:
-
-\begin{center}
-\begin{tabular}{rcl@{\hspace{10mm}}l}
-$L(\ZERO)$ & $\dn$ & $\varnothing$ & \pcode{ZERO}\\
-$L(\ONE)$ & $\dn$ & $\{[]\}$ & \pcode{ONE}\\
-$L(c)$ & $\dn$ & $\{[c]\}$ & \pcode{CHAR}\\
-$L(r_1 + r_2)$ & $\dn$ & $L(r_1) \cup L(r_2)$ & \pcode{ALT}\\
-$L(r_1 \cdot r_2)$ & $\dn$ & $L(r_1) \,@\, L(r_2)$ & \pcode{SEQ}\\
-$L(r^*)$ & $\dn$ & $(L(r))^*$ & \pcode{STAR}\\
-\end{tabular}
-\end{center}
+\noindent This coursework is worth 12\% and is due on \cwFIVE{} at
+18:00. You are asked to implement a compiler targetting the LLVM-IR.
+You can do the implementation in any programming
+language you like, but you need to submit the source code with which
+you answered the questions, otherwise a mark of 0\% will be
+awarded. You should use the lexer from the previous coursework for the
+parser. Please package everything(!) in a zip-file that creates a
+directory with the name \texttt{YournameYourFamilyname} on my end.
-\noindent You would need to implement this function in order
-to state the theorem about the correctness of the algorithm.
-The function $L$ should in Isabelle take a \pcode{rexp} as
-input and return a set of strings. Its type is
-therefore
-
-\begin{center}
-\pcode{L} \pcode{::} \pcode{rexp} $\Rightarrow$ \pcode{string set}
-\end{center}
-
-\noindent Isabelle treats strings as an abbreviation for lists
-of characters. This means you can pattern-match strings like
-lists. The union operation on sets (for the \pcode{ALT}-case)
-is a standard definition in Isabelle, but not the
-concatenation operation on sets and also not the
-star-operation. You would have to supply these definitions.
-The concatenation operation can be defined in terms of the
-append function, written \code{_ @ _} in Isabelle, for lists.
-The star-operation can be defined as a ``big-union'' of
-powers, like in the lectures, or directly as an inductive set.
-
-The functions for the matcher are shown in
-Figure~\ref{matcher}. The theorem that needs to be proved is
-
-\begin{lstlisting}[numbers=none,language={},keywordstyle=\color{black}\ttfamily,mathescape]
-theorem
- "matches r s $\longleftrightarrow$ s $\in$ L r"
-\end{lstlisting}
-
-\noindent which states that the function \emph{matches} is
-true if and only if the string is in the language of the
-regular expression. A proof for this lemma will need
-side-lemmas about \pcode{nullable} and \pcode{der}. An example
-proof in Isabelle that will not be relevant for the theorem
-above is given in Figure~\ref{proof}.
+\subsection*{Disclaimer\alert}
-\begin{figure}[p]
-\begin{lstlisting}[language={},keywordstyle=\color{black}\ttfamily,mathescape]
-fun
- nullable :: "rexp $\Rightarrow$ bool"
-where
- "nullable ZERO = False"
-| "nullable ONE = True"
-| "nullable (CHAR _) = False"
-| "nullable (ALT r1 r2) = (nullable(r1) $\vee$ nullable(r2))"
-| "nullable (SEQ r1 r2) = (nullable(r1) $\wedge$ nullable(r2))"
-| "nullable (STAR _) = True"
-
-fun
- der :: "char $\Rightarrow$ rexp $\Rightarrow$ rexp"
-where
- "der c ZERO = ZERO"
-| "der c ONE = ZERO"
-| "der c (CHAR d) = (if c = d then ONE else ZERO)"
-| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
-| "der c (SEQ r1 r2) =
- (if (nullable r1) then ALT (SEQ (der c r1) r2) (der c r2)
- else SEQ (der c r1) r2)"
-| "der c (STAR r) = SEQ (der c r) (STAR r)"
-
-fun
- ders :: "rexp $\Rightarrow$ string $\Rightarrow$ rexp"
-where
- "ders r [] = r"
-| "ders r (c # s) = ders (der c r) s"
-
-fun
- matches :: "rexp $\Rightarrow$ string $\Rightarrow$ bool"
-where
- "matches r s = nullable (ders r s)"
-\end{lstlisting}
-\caption{The definition of the matcher algorithm in
-Isabelle.\label{matcher}}
-\end{figure}
+It should be understood that the work you submit represents your own
+effort. You have not copied from anyone else. An exception is the
+Scala code I showed during the lectures or uploaded to KEATS, which
+you can both use. You can also use your own code from the CW~1 --
+CW~4.
-\begin{figure}[p]
-\begin{lstlisting}[language={},keywordstyle=\color{black}\ttfamily,mathescape]
-fun
- zeroable :: "rexp $\Rightarrow$ bool"
-where
- "zeroable ZERO = True"
-| "zeroable ONE = False"
-| "zeroable (CHAR _) = False"
-| "zeroable (ALT r1 r2) = (zeroable(r1) $\wedge$ zeroable(r2))"
-| "zeroable (SEQ r1 r2) = (zeroable(r1) $\vee$ zeroable(r2))"
-| "zeroable (STAR _) = False"
+
+\subsection*{Question 1}
-lemma
- "zeroable r $\longleftrightarrow$ L r = {}"
-proof (induct)
- case (ZERO)
- have "zeroable ZERO" "L ZERO = {}" by simp_all
- then show "zeroable ZERO $\longleftrightarrow$ (L ZERO = {})" by simp
-next
- case (ONE)
- have "$\neg$ zeroable ONE" "L ONE = {[]}" by simp_all
- then show "zeroable ONE $\longleftrightarrow$ (L ONE = {})" by simp
-next
- case (CHAR c)
- have "$\neg$ zeroable (CHAR c)" "L (CHAR c) = {[c]}" by simp_all
- then show "zeroable (CHAR c) $\longleftrightarrow$ (L (CHAR c) = {})" by simp
-next
- case (ALT r1 r2)
- have ih1: "zeroable r1 $\longleftrightarrow$ L r1 = {}" by fact
- have ih2: "zeroable r2 $\longleftrightarrow$ L r2 = {}" by fact
- show "zeroable (ALT r1 r2) $\longleftrightarrow$ (L (ALT r1 r2) = {})"
- using ih1 ih2 by simp
-next
- case (SEQ r1 r2)
- have ih1: "zeroable r1 $\longleftrightarrow$ L r1 = {}" by fact
- have ih2: "zeroable r2 $\longleftrightarrow$ L r2 = {}" by fact
- show "zeroable (SEQ r1 r2) $\longleftrightarrow$ (L (SEQ r1 r2) = {})"
- using ih1 ih2 by (auto simp add: Conc_def)
-next
- case (STAR r)
- have "$\neg$ zeroable (STAR r)" "[] $\in$ L (r) ^ 0" by simp_all
- then show "zeroable (STAR r) $\longleftrightarrow$ (L (STAR r) = {})"
- by (simp (no_asm) add: Star_def) blast
-qed
-\end{lstlisting}
-\caption{An Isabelle proof about the function \texttt{zeroable}.\label{proof}}
-\end{figure}
+\subsection*{Question 2}
+
+\subsection*{Question 3}
\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/coursework/cw0A.tex Tue Sep 01 15:57:55 2020 +0100
@@ -0,0 +1,245 @@
+% !TEX program = xelatex
+\documentclass{article}
+\usepackage{../style}
+\usepackage{../langs}
+
+\begin{document}
+
+\section*{Coursework (Strand 2)}
+
+\noindent This coursework is worth 20\% and is due on \cwISABELLE{} at
+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 and also a document
+describing your proof. The Isabelle theorem prover is available from
+
+\begin{center}
+\url{http://isabelle.in.tum.de}
+\end{center}
+
+\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 completely automatic. There is a shortish user guide for
+Isabelle, called ``Programming and Proving in Isabelle/HOL''
+at
+
+\begin{center}
+\url{http://isabelle.in.tum.de/documentation.html}
+\end{center}
+
+\noindent
+and also a longer (free) book at
+
+\begin{center}
+\url{http://www.concrete-semantics.org}
+\end{center}
+
+\noindent The Isabelle theorem prover is operated through the
+jEdit IDE, which might not be an editor that is widely known.
+JEdit is documented in
+
+\begin{center}
+\url{http://isabelle.in.tum.de/dist/Isabelle2014/doc/jedit.pdf}
+\end{center}
+
+
+\noindent If you need more help or you are stuck somewhere,
+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 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 (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. 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]
+datatype rexp =
+ ZERO
+| ONE
+| CHAR char
+| SEQ rexp rexp
+| ALT rexp rexp
+| STAR rexp
+\end{lstlisting}
+
+\noindent The meaning of regular expressions is given as
+usual:
+
+\begin{center}
+\begin{tabular}{rcl@{\hspace{10mm}}l}
+$L(\ZERO)$ & $\dn$ & $\varnothing$ & \pcode{ZERO}\\
+$L(\ONE)$ & $\dn$ & $\{[]\}$ & \pcode{ONE}\\
+$L(c)$ & $\dn$ & $\{[c]\}$ & \pcode{CHAR}\\
+$L(r_1 + r_2)$ & $\dn$ & $L(r_1) \cup L(r_2)$ & \pcode{ALT}\\
+$L(r_1 \cdot r_2)$ & $\dn$ & $L(r_1) \,@\, L(r_2)$ & \pcode{SEQ}\\
+$L(r^*)$ & $\dn$ & $(L(r))^*$ & \pcode{STAR}\\
+\end{tabular}
+\end{center}
+
+\noindent You would need to implement this function in order
+to state the theorem about the correctness of the algorithm.
+The function $L$ should in Isabelle take a \pcode{rexp} as
+input and return a set of strings. Its type is
+therefore
+
+\begin{center}
+\pcode{L} \pcode{::} \pcode{rexp} $\Rightarrow$ \pcode{string set}
+\end{center}
+
+\noindent Isabelle treats strings as an abbreviation for lists
+of characters. This means you can pattern-match strings like
+lists. The union operation on sets (for the \pcode{ALT}-case)
+is a standard definition in Isabelle, but not the
+concatenation operation on sets and also not the
+star-operation. You would have to supply these definitions.
+The concatenation operation can be defined in terms of the
+append function, written \code{_ @ _} in Isabelle, for lists.
+The star-operation can be defined as a ``big-union'' of
+powers, like in the lectures, or directly as an inductive set.
+
+The functions for the matcher are shown in
+Figure~\ref{matcher}. The theorem that needs to be proved is
+
+\begin{lstlisting}[numbers=none,language={},keywordstyle=\color{black}\ttfamily,mathescape]
+theorem
+ "matches r s $\longleftrightarrow$ s $\in$ L r"
+\end{lstlisting}
+
+\noindent which states that the function \emph{matches} is
+true if and only if the string is in the language of the
+regular expression. A proof for this lemma will need
+side-lemmas about \pcode{nullable} and \pcode{der}. An example
+proof in Isabelle that will not be relevant for the theorem
+above is given in Figure~\ref{proof}.
+
+\begin{figure}[p]
+\begin{lstlisting}[language={},keywordstyle=\color{black}\ttfamily,mathescape]
+fun
+ nullable :: "rexp $\Rightarrow$ bool"
+where
+ "nullable ZERO = False"
+| "nullable ONE = True"
+| "nullable (CHAR _) = False"
+| "nullable (ALT r1 r2) = (nullable(r1) $\vee$ nullable(r2))"
+| "nullable (SEQ r1 r2) = (nullable(r1) $\wedge$ nullable(r2))"
+| "nullable (STAR _) = True"
+
+fun
+ der :: "char $\Rightarrow$ rexp $\Rightarrow$ rexp"
+where
+ "der c ZERO = ZERO"
+| "der c ONE = ZERO"
+| "der c (CHAR d) = (if c = d then ONE else ZERO)"
+| "der c (ALT r1 r2) = ALT (der c r1) (der c r2)"
+| "der c (SEQ r1 r2) =
+ (if (nullable r1) then ALT (SEQ (der c r1) r2) (der c r2)
+ else SEQ (der c r1) r2)"
+| "der c (STAR r) = SEQ (der c r) (STAR r)"
+
+fun
+ ders :: "rexp $\Rightarrow$ string $\Rightarrow$ rexp"
+where
+ "ders r [] = r"
+| "ders r (c # s) = ders (der c r) s"
+
+fun
+ matches :: "rexp $\Rightarrow$ string $\Rightarrow$ bool"
+where
+ "matches r s = nullable (ders r s)"
+\end{lstlisting}
+\caption{The definition of the matcher algorithm in
+Isabelle.\label{matcher}}
+\end{figure}
+
+\begin{figure}[p]
+\begin{lstlisting}[language={},keywordstyle=\color{black}\ttfamily,mathescape]
+fun
+ zeroable :: "rexp $\Rightarrow$ bool"
+where
+ "zeroable ZERO = True"
+| "zeroable ONE = False"
+| "zeroable (CHAR _) = False"
+| "zeroable (ALT r1 r2) = (zeroable(r1) $\wedge$ zeroable(r2))"
+| "zeroable (SEQ r1 r2) = (zeroable(r1) $\vee$ zeroable(r2))"
+| "zeroable (STAR _) = False"
+
+lemma
+ "zeroable r $\longleftrightarrow$ L r = {}"
+proof (induct)
+ case (ZERO)
+ have "zeroable ZERO" "L ZERO = {}" by simp_all
+ then show "zeroable ZERO $\longleftrightarrow$ (L ZERO = {})" by simp
+next
+ case (ONE)
+ have "$\neg$ zeroable ONE" "L ONE = {[]}" by simp_all
+ then show "zeroable ONE $\longleftrightarrow$ (L ONE = {})" by simp
+next
+ case (CHAR c)
+ have "$\neg$ zeroable (CHAR c)" "L (CHAR c) = {[c]}" by simp_all
+ then show "zeroable (CHAR c) $\longleftrightarrow$ (L (CHAR c) = {})" by simp
+next
+ case (ALT r1 r2)
+ have ih1: "zeroable r1 $\longleftrightarrow$ L r1 = {}" by fact
+ have ih2: "zeroable r2 $\longleftrightarrow$ L r2 = {}" by fact
+ show "zeroable (ALT r1 r2) $\longleftrightarrow$ (L (ALT r1 r2) = {})"
+ using ih1 ih2 by simp
+next
+ case (SEQ r1 r2)
+ have ih1: "zeroable r1 $\longleftrightarrow$ L r1 = {}" by fact
+ have ih2: "zeroable r2 $\longleftrightarrow$ L r2 = {}" by fact
+ show "zeroable (SEQ r1 r2) $\longleftrightarrow$ (L (SEQ r1 r2) = {})"
+ using ih1 ih2 by (auto simp add: Conc_def)
+next
+ case (STAR r)
+ have "$\neg$ zeroable (STAR r)" "[] $\in$ L (r) ^ 0" by simp_all
+ then show "zeroable (STAR r) $\longleftrightarrow$ (L (STAR r) = {})"
+ by (simp (no_asm) add: Star_def) blast
+qed
+\end{lstlisting}
+\caption{An Isabelle proof about the function \texttt{zeroable}.\label{proof}}
+\end{figure}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
--- a/style.sty Tue Sep 01 12:44:07 2020 +0100
+++ b/style.sty Tue Sep 01 15:57:55 2020 +0100
@@ -101,5 +101,6 @@
\def\cwTWO{4 November}
\def\cwTHREE{22 November}
\def\cwFOUR{11 December}
+\def\cwFIVE{15 January}
\def\cwISABELLE{11 December}