# HG changeset patch # User Christian Urban # Date 1473868264 -3600 # Node ID 4110ab35e5d8e2ef20f71cd6d50f6df27b56fd0e # Parent 010c5a03dca22abcb7e83d9e2a8ce41faae0b84e updated courseworks diff -r 010c5a03dca2 -r 4110ab35e5d8 coursework/cw02.pdf Binary file coursework/cw02.pdf has changed diff -r 010c5a03dca2 -r 4110ab35e5d8 coursework/cw02.tex --- a/coursework/cw02.tex Wed Sep 14 11:02:44 2016 +0100 +++ b/coursework/cw02.tex Wed Sep 14 16:51:04 2016 +0100 @@ -6,25 +6,26 @@ \section*{Coursework 2 (Strand 1)} -\noindent This coursework is worth 5\% and is due on 6 +\noindent This coursework is worth 4\% and is due on 3 November at 16:00. You are asked to implement the Sulzmann \& -Lu tokeniser for the WHILE language. You can do the +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 questions, otherwise a mark of 0\% will be awarded. You can -submit your answers in a txt-file or as pdf. +submit your answers in a txt-file or as pdf. Code submit as +code. \subsection*{Disclaimer} 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 from KEATS and the code I showed -during the lectures, which you can both use. You can also use -your own code from the CW~1. +during the lectures, which you can both freely use. You can +also use your own code from the CW~1. -\subsection*{Question 1 (marked with 1\%)} +\subsection*{Question 1} -To implement a tokeniser for the WHILE language, you first +To implement a lexer for the WHILE language, you first need to design the appropriate regular expressions for the following eight syntactic entities: @@ -78,7 +79,7 @@ You can use the basic regular expressions \[ -\varnothing, \epsilon, c, r_1 + r_2, r_1 \cdot r_2, r^* +\ZERO,\; \ONE,\; c,\; r_1 + r_2,\; r_1 \cdot r_2,\; r^* \] \noindent @@ -97,9 +98,9 @@ small as possible. For example you should use character ranges for identifiers and numbers. -\subsection*{Question 2 (marked with 3\%)} +\subsection*{Question 2} -Implement the Sulzmann \& Lu tokeniser from the lectures. For +Implement the Sulzmann \& Lu lexer from the lectures. For this you need to implement the functions $nullable$ and $der$ (you can use your code from CW~1), as well as $mkeps$ and $inj$. These functions need to be appropriately extended for @@ -138,7 +139,7 @@ Also add the record regular expression from the -lectures to your tokeniser and implement a function, say +lectures to your lexer and implement a function, say \pcode{env}, that returns all assignments from a value (such that you can extract easily the tokens from a value).\medskip @@ -154,11 +155,11 @@ and use your \pcode{env} function to give the token sequence. -\subsection*{Question 3 (marked with 1\%)} +\subsection*{Question 3} -Extend your tokenizer from Q2 to also simplify regular expressions +Extend your lexer from Q2 to also simplify regular expressions after each derivation step and rectify the computed values after each -injection. Use this tokenizer to tokenize the programs in +injection. Use this lexer to tokenize the programs in Figure~\ref{fib} and \ref{loop}. Give the tokens of these programs where whitespaces are filtered out. diff -r 010c5a03dca2 -r 4110ab35e5d8 coursework/cw03.pdf Binary file coursework/cw03.pdf has changed diff -r 010c5a03dca2 -r 4110ab35e5d8 coursework/cw03.tex --- a/coursework/cw03.tex Wed Sep 14 11:02:44 2016 +0100 +++ b/coursework/cw03.tex Wed Sep 14 16:51:04 2016 +0100 @@ -4,9 +4,9 @@ \begin{document} -\section*{Coursework 3 (Strand 1)} +\section*{Coursework 3} -\noindent This coursework is worth 5\% and is due on 27 +\noindent This coursework is worth 5\% and is due on 24 November at 16: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 @@ -23,9 +23,9 @@ CW~1 and CW~2. -\subsection*{Question 1 (marked with 1\%)} +\subsection*{Question 1} -Design a grammar for the WHILE language and give the grammar +Design a grammar for the WHILE language and give the grammar rules. The main categories of non-terminal should be: \begin{itemize} @@ -39,12 +39,12 @@ \item blocks which are enclosed in curly parentheses \end{itemize} -\subsection*{Question 2 (marked with 2\%)} +\subsection*{Question 2} You should implement a parser for the WHILE language using parser combinators. Be careful that the parser takes as input a stream, or list, of tokens generated by the tokenizer from -the previous coursework. For this you might filter out +the previous coursework. For this you might want to filter out whitespaces and comments. Your parser should be able to handle the WHILE programs in Figures~\ref{fib} and \ref{loop}. In addition give the parse tree for the statement: @@ -81,11 +81,11 @@ \caption{The datatype for parse trees in Scala.\label{trees}} \end{figure} -\subsection*{Question 3 (marked with 2\%)} +\subsection*{Question 3} Implement an interpreter for the WHILE language you designed and parsed in Question 1 and 2. This interpreter should take -as input a parse tree. However be careful because programs +as input a parse tree. However be careful because, programs contain variables and variable assignments. This means you need to maintain a kind of memory, or environment, where you can look up a value of a variable and also diff -r 010c5a03dca2 -r 4110ab35e5d8 coursework/cw04.pdf Binary file coursework/cw04.pdf has changed diff -r 010c5a03dca2 -r 4110ab35e5d8 coursework/cw04.tex --- a/coursework/cw04.tex Wed Sep 14 11:02:44 2016 +0100 +++ b/coursework/cw04.tex Wed Sep 14 16:51:04 2016 +0100 @@ -9,7 +9,7 @@ \section*{Coursework 4 (Strand 1)} -\noindent This coursework is worth 10\% and is due on 11 +\noindent This coursework is worth 5\% and is due on 13 December at 16: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 @@ -124,7 +124,7 @@ %submit your answers in a txt-file or as pdf.\bigskip -\subsection*{Question 1 (marked with 5\%)} +\subsection*{Question 1} You need to lex and parse WHILE programs, and then generate Java Byte Code instructions for the Jasmin assembler (or @@ -141,7 +141,7 @@ \caption{The Fibonacci program in the WHILE language.\label{fibs}} \end{figure} -\subsection*{Question 2 (marked with 4\%)} +\subsection*{Question 2} Extend the syntax of your language so that it contains also \texttt{for}-loops, like diff -r 010c5a03dca2 -r 4110ab35e5d8 coursework/cw05.pdf Binary file coursework/cw05.pdf has changed diff -r 010c5a03dca2 -r 4110ab35e5d8 coursework/cw05.tex --- a/coursework/cw05.tex Wed Sep 14 11:02:44 2016 +0100 +++ b/coursework/cw05.tex Wed Sep 14 16:51:04 2016 +0100 @@ -6,13 +6,11 @@ \section*{Coursework (Strand 2)} -\noindent This coursework is worth 25\% and is due on 11 -December at 16: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 +\noindent This coursework is worth 20\% and is due on 13 December at +16: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 \begin{center} \url{http://isabelle.in.tum.de} @@ -47,8 +45,8 @@ \noindent If you need more help or you are stuck somewhere, please feel free to contact me (christian.urban@kcl.ac.uk). I -am a main developer of Isabelle and have used it for -approximately the 14 years. One of the success stories of +am one of the main developers of Isabelle and have used it for +approximately the 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 @@ -73,8 +71,8 @@ \begin{lstlisting}[language={},numbers=none] datatype rexp = - NULL -| EMPTY + ZERO +| ONE | CHAR char | SEQ rexp rexp | ALT rexp rexp @@ -86,8 +84,8 @@ \begin{center} \begin{tabular}{rcl@{\hspace{10mm}}l} -$L(\varnothing)$ & $\dn$ & $\varnothing$ & \pcode{NULL}\\ -$L(\epsilon)$ & $\dn$ & $\{[]\}$ & \pcode{EMPTY}\\ +$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}\\ @@ -136,8 +134,8 @@ fun nullable :: "rexp $\Rightarrow$ bool" where - "nullable NULL = False" -| "nullable EMPTY = True" + "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))" @@ -146,9 +144,9 @@ fun der :: "char $\Rightarrow$ rexp $\Rightarrow$ rexp" where - "der c NULL = NULL" -| "der c EMPTY = NULL" -| "der c (CHAR d) = (if c = d then EMPTY else NULL)" + "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) @@ -175,8 +173,8 @@ fun zeroable :: "rexp $\Rightarrow$ bool" where - "zeroable NULL = True" -| "zeroable EMPTY = False" + "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))" @@ -185,13 +183,13 @@ lemma "zeroable r $\longleftrightarrow$ L r = {}" proof (induct) - case (NULL) - have "zeroable NULL" "L NULL = {}" by simp_all - then show "zeroable NULL $\longleftrightarrow$ (L NULL = {})" by simp + case (ZERO) + have "zeroable ZERO" "L ZERO = {}" by simp_all + then show "zeroable ZERO $\longleftrightarrow$ (L ZERO = {})" by simp next - case (EMPTY) - have "$\neg$ zeroable EMPTY" "L EMPTY = {[]}" by simp_all - then show "zeroable EMPTY $\longleftrightarrow$ (L EMPTY = {})" by simp + 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