# HG changeset patch # User Christian Urban # Date 1598972275 -3600 # Node ID 4b208d81e002cb0e5e573954f71fed4d8993b92b # Parent e93a9e74ca8ed3851a72a22e24fd36718be3c892 updated diff -r e93a9e74ca8e -r 4b208d81e002 coursework/cw04.pdf Binary file coursework/cw04.pdf has changed diff -r e93a9e74ca8e -r 4b208d81e002 coursework/cw04.tex --- 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} diff -r e93a9e74ca8e -r 4b208d81e002 coursework/cw05.pdf Binary file coursework/cw05.pdf has changed diff -r e93a9e74ca8e -r 4b208d81e002 coursework/cw05.tex --- 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} diff -r e93a9e74ca8e -r 4b208d81e002 coursework/cw0A.tex --- /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: diff -r e93a9e74ca8e -r 4b208d81e002 style.sty --- 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}