--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a2/ROOT.ML Tue Apr 06 16:19:45 2004 +0200
@@ -0,0 +1,1 @@
+use_thy "a2";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a2/a2.thy Tue Apr 06 16:19:45 2004 +0200
@@ -0,0 +1,66 @@
+(*<*)
+theory a2 = Main:
+(*>*)
+
+subsection {* Trees *}
+
+
+
+text{* Define a datatype @{text"'a tree"} for binary trees. Both leaf
+and internal nodes store information.
+*};
+
+datatype 'a tree(*<*)= Tip "'a" | Node "'a" "'a tree" "'a tree"(*>*)
+
+text{*
+Define the functions @{term preOrder}, @{term postOrder}, and @{term
+inOrder} that traverse an @{text"'a tree"} in the respective order.
+*}
+
+(*<*)consts(*>*)
+ preOrder :: "'a tree \<Rightarrow> 'a list"
+ postOrder :: "'a tree \<Rightarrow> 'a list"
+ inOrder :: "'a tree \<Rightarrow> 'a list"
+
+text{*
+Define a function @{term mirror} that returns the mirror image of an @{text"'a tree"}.
+*};
+(*<*)consts(*>*)
+ mirror :: "'a tree \<Rightarrow> 'a tree"
+
+text{*
+Suppose that @{term xOrder} and @{term yOrder} are tree traversal
+functions chosen from @{term preOrder}, @{term postOrder}, and @{term
+inOrder}. Formulate and prove all valid properties of the form
+\mbox{@{text "xOrder (mirror xt) = rev (yOrder xt)"}}.
+*}
+
+text{*
+Define the functions @{term root}, @{term leftmost} and @{term
+rightmost}, that return the root, leftmost, and rightmost element
+respectively.
+*}
+(*<*)consts(*>*)
+ root :: "'a tree \<Rightarrow> 'a"
+ leftmost :: "'a tree \<Rightarrow> 'a"
+ rightmost :: "'a tree \<Rightarrow> 'a"
+
+text {*
+Prove or disprove (by counter example) the theorems that follow. You may have to prove some lemmas first.
+*};
+
+theorem "last(inOrder xt) = rightmost xt"
+(*<*)oops(*>*)
+theorem "hd (inOrder xt) = leftmost xt "
+(*<*)oops(*>*)
+theorem "hd(preOrder xt) = last(postOrder xt)"
+(*<*)oops(*>*)
+theorem "hd(preOrder xt) = root xt"
+(*<*)oops(*>*)
+theorem "hd(inOrder xt) = root xt "
+(*<*)oops(*>*)
+theorem "last(postOrder xt) = root xt"
+(*<*)oops(*>*)
+
+
+(*<*)end(*>*)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a2/generated/a2.tex Tue Apr 06 16:19:45 2004 +0200
@@ -0,0 +1,75 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{a{\isadigit{2}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{Trees%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Define a datatype \isa{{\isacharprime}a\ tree} for binary trees. Both leaf
+and internal nodes store information.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\ {\isacharprime}a\ tree\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define the functions \isa{preOrder}, \isa{postOrder}, and \isa{inOrder} that traverse an \isa{{\isacharprime}a\ tree} in the respective order.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ preOrder\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
+\ \ postOrder\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isanewline
+\ \ inOrder\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ list{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define a function \isa{mirror} that returns the mirror image of an \isa{{\isacharprime}a\ tree}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ mirror\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ tree{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Suppose that \isa{xOrder} and \isa{yOrder} are tree traversal
+functions chosen from \isa{preOrder}, \isa{postOrder}, and \isa{inOrder}. Formulate and prove all valid properties of the form
+\mbox{\isa{xOrder\ {\isacharparenleft}mirror\ xt{\isacharparenright}\ {\isacharequal}\ rev\ {\isacharparenleft}yOrder\ xt{\isacharparenright}}}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Define the functions \isa{root}, \isa{leftmost} and \isa{rightmost}, that return the root, leftmost, and rightmost element
+respectively.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\ \ root\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
+\ \ leftmost\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isanewline
+\ \ rightmost\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Prove or disprove (by counter example) the theorems that follow. You may have to prove some lemmas first.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{theorem}\ {\isachardoublequote}last{\isacharparenleft}inOrder\ xt{\isacharparenright}\ {\isacharequal}\ rightmost\ xt{\isachardoublequote}\isamarkupfalse%
+\ \isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}hd\ {\isacharparenleft}inOrder\ xt{\isacharparenright}\ {\isacharequal}\ leftmost\ xt\ {\isachardoublequote}\isamarkupfalse%
+\ \isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}hd{\isacharparenleft}preOrder\ xt{\isacharparenright}\ {\isacharequal}\ last{\isacharparenleft}postOrder\ xt{\isacharparenright}{\isachardoublequote}\isamarkupfalse%
+\ \isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}hd{\isacharparenleft}preOrder\ xt{\isacharparenright}\ {\isacharequal}\ root\ xt{\isachardoublequote}\isamarkupfalse%
+\ \isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}hd{\isacharparenleft}inOrder\ xt{\isacharparenright}\ {\isacharequal}\ root\ xt\ {\isachardoublequote}\isamarkupfalse%
+\ \isanewline
+\isamarkupfalse%
+\isacommand{theorem}\ {\isachardoublequote}last{\isacharparenleft}postOrder\ xt{\isacharparenright}\ {\isacharequal}\ root\ xt{\isachardoublequote}\isamarkupfalse%
+\ \isanewline
+\isanewline
+\isamarkupfalse%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a2/generated/session.tex Tue Apr 06 16:19:45 2004 +0200
@@ -0,0 +1,6 @@
+\input{a2.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a3/ROOT.ML Tue Apr 06 16:19:45 2004 +0200
@@ -0,0 +1,1 @@
+ use_thy "a3";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a3/a3.thy Tue Apr 06 16:19:45 2004 +0200
@@ -0,0 +1,47 @@
+(*<*)
+theory a3 = Main:
+(*>*)
+
+subsection{* Computing with natural numbers - Magical Methods *}
+
+text{*
+A book about Vedic Mathematics describes three methods to make the calculation of squares of natural numbers easier:
+
+\begin{itemize}
+\item {\em MM1}: Numbers whose predecessors have squares that are known or can easily be calculated. For example:
+\\ Needed: $61^2$
+\\ Given: $60^2 = 3600$
+\\ Observe: $61^2 = 3600 + 60 + 61 = 3721$
+
+\item {\em MM2}: Numbers greater than, but near 100. For example:
+\\ Needed: $102^2$
+\\ Let $h = 102 - 100 = 2$ , $h^2 = 4$
+\\ Observe: $102^2 = (102+h)$ shifted two places to the left $ + h^2 = 10404$
+
+\item {\em MM3}: Numbers ending in $5$. For example:
+\\ Needed: $85^2$
+\\ Observe: $85^2 = (8 * 9)$ appended to $ 25 = 7225$
+\\ Needed: $995^2$
+\\ Observe: $995^2 = (99 * 100)$ appended to $ 25 = 990025 $
+\end{itemize}
+
+
+In this exercise we will show that these methods are not so magical after all!
+
+\begin{itemize}
+\item Based on {\em MM1} define a function @{term "sq"} that calculates the square of a natural number.
+\item Prove the correctness of @{term "sq"} (i.e.\ @{term "sq n = n * n"}).
+\item Formulate and prove the correctness of {\em MM2}.\\ Hints:
+ \begin{itemize}
+ \item Generalise {\em MM2} for an arbitrary constant (instead of $100$).
+ \item Universally quantify all variables other than the induction variable.
+\end{itemize}
+\item Formulate and prove the correctness of {\em MM3}.\\ Hints:
+ \begin{itemize}
+ \item Try to formulate the property `numbers ending in $5$' such that it is easy to get to the rest of the number.
+ \item Proving the binomial formula for $(a+b)^2$ can be of some help.
+ \end{itemize}
+\end{itemize}
+*}
+
+(*<*) end (*>*)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a3/generated/a3.tex Tue Apr 06 16:19:45 2004 +0200
@@ -0,0 +1,55 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{a{\isadigit{3}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{Computing with natural numbers - Magical Methods%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A book about Vedic Mathematics describes three methods to make the calculation of squares of natural numbers easier:
+
+\begin{itemize}
+\item {\em MM1}: Numbers whose predecessors have squares that are known or can easily be calculated. For example:
+\\ Needed: $61^2$
+\\ Given: $60^2 = 3600$
+\\ Observe: $61^2 = 3600 + 60 + 61 = 3721$
+
+\item {\em MM2}: Numbers greater than, but near 100. For example:
+\\ Needed: $102^2$
+\\ Let $h = 102 - 100 = 2$ , $h^2 = 4$
+\\ Observe: $102^2 = (102+h)$ shifted two places to the left $ + h^2 = 10404$
+
+\item {\em MM3}: Numbers ending in $5$. For example:
+\\ Needed: $85^2$
+\\ Observe: $85^2 = (8 * 9)$ appended to $ 25 = 7225$
+\\ Needed: $995^2$
+\\ Observe: $995^2 = (99 * 100)$ appended to $ 25 = 990025 $
+\end{itemize}
+
+
+In this exercise we will show that these methods are not so magical after all!
+
+\begin{itemize}
+\item Based on {\em MM1} define a function \isa{sq} that calculates the square of a natural number.
+\item Prove the correctness of \isa{sq} (i.e.\ \isa{sq\ n\ {\isacharequal}\ n\ {\isacharasterisk}\ n}).
+\item Formulate and prove the correctness of {\em MM2}.\\ Hints:
+ \begin{itemize}
+ \item Generalise {\em MM2} for an arbitrary constant (instead of $100$).
+ \item Universally quantify all variables other than the induction variable.
+\end{itemize}
+\item Formulate and prove the correctness of {\em MM3}.\\ Hints:
+ \begin{itemize}
+ \item Try to formulate the property `numbers ending in $5$' such that it is easy to get to the rest of the number.
+ \item Proving the binomial formula for $(a+b)^2$ can be of some help.
+ \end{itemize}
+\end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a3/generated/session.tex Tue Apr 06 16:19:45 2004 +0200
@@ -0,0 +1,6 @@
+\input{a3.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a5/ROOT.ML Tue Apr 06 16:19:45 2004 +0200
@@ -0,0 +1,1 @@
+use_thy "a5";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a5/a5.thy Tue Apr 06 16:19:45 2004 +0200
@@ -0,0 +1,66 @@
+(*<*)
+theory a5 = Main:
+(*>*)
+
+subsection {*BIGNAT - Specification and Verification*};
+
+text{*
+Hardware platforms have a limit on the largest number they can represent. This is normally fixed by the bit lengths of registers and ALUs used. In order to be able to perform calculations that require arbitrarily large numbers, the provided arithmetic operations need to be extended in order for them to work on an abstract data type representing numbers of arbitrary size.
+
+In this exercise we will build and verify an implementation for BIGNAT, an abstract data type representing natural numbers of arbitrary size.
+*}
+
+text {*\subsubsection*{Representation}*}
+
+text{*
+A BIGNAT is represented as a list of natural numbers in a range supported by the target machine. In our case, this will be all natural numbers in the range [0, BASE-1]. (Note: natural numbers in Isabelle are of arbitrary size)
+*}
+
+types
+ bigNat = "nat list"
+
+text{*
+Define a function @{term "valid"} that takes a value for BASE, and checks if the given BIGNAT is valid.
+*}
+
+consts valid :: "nat \<Rightarrow> bigNat \<Rightarrow> bool"
+
+text{*
+Define a function @{term "val"} that takes a BIGNAT and its corresponding BASE, and returns the natural number represented by it. *}
+
+consts val :: "nat \<Rightarrow> bigNat \<Rightarrow> nat"
+
+text {*\subsubsection*{Addition}*}
+
+text{*
+Define a function @{term "add"} that adds two BIGNATs with the same value for BASE. Make sure that your algorithm preserves the validity of the BIGNAT representation.
+*}
+
+consts add :: "nat \<Rightarrow> bigNat \<Rightarrow> bigNat \<Rightarrow> bigNat"
+
+text{*
+Using @{term "val"}, verify formally that your function @{term "add"} computes the sum of two BIGNATs correctly.*}
+
+text{*
+Using @{term "valid"}, verify formally that your function @{term "add"} preserves the validity of the BIGNAT representation.*}
+
+
+text {*
+\subsubsection*{Multiplication}*}
+
+text{*
+Define a function @{term "mult"} that multiplies two BIGNATs with the same value for BASE. You may use @{term "add"}, but not so often as to make the solution trivial. Make sure that your algorithm preserves the validity of the BIGNAT representation.
+*}
+consts mult :: "nat \<Rightarrow> bigNat \<Rightarrow> bigNat \<Rightarrow> bigNat"
+text{*
+Using @{term "val"}, verify formally that your function @{term "mult"} computes the product of two BIGNATs correctly.*}
+
+text{*
+Using @{term "valid"}, verify formally that your function @{term "mult"} preserves the validity of the BIGNAT representation.*}
+
+
+(*<*) end (*>*)
+
+
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a5/generated/a5.tex Tue Apr 06 16:19:45 2004 +0200
@@ -0,0 +1,91 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{a{\isadigit{5}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{BIGNAT - Specification and Verification%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Hardware platforms have a limit on the largest number they can represent. This is normally fixed by the bit lengths of registers and ALUs used. In order to be able to perform calculations that require arbitrarily large numbers, the provided arithmetic operations need to be extended in order for them to work on an abstract data type representing numbers of arbitrary size.
+
+In this exercise we will build and verify an implementation for BIGNAT, an abstract data type representing natural numbers of arbitrary size.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\subsubsection*{Representation}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+A BIGNAT is represented as a list of natural numbers in a range supported by the target machine. In our case, this will be all natural numbers in the range [0, BASE-1]. (Note: natural numbers in Isabelle are of arbitrary size)%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{types}\ \isanewline
+\ \ bigNat\ {\isacharequal}\ {\isachardoublequote}nat\ list{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define a function \isa{valid} that takes a value for BASE, and checks if the given BIGNAT is valid.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ valid\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ bigNat\ {\isasymRightarrow}\ bool{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define a function \isa{val} that takes a BIGNAT and its corresponding BASE, and returns the natural number represented by it.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ val\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ bigNat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\subsubsection*{Addition}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Define a function \isa{add} that adds two BIGNATs with the same value for BASE. Make sure that your algorithm preserves the validity of the BIGNAT representation.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ add\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ bigNat\ {\isasymRightarrow}\ bigNat\ {\isasymRightarrow}\ bigNat{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Using \isa{val}, verify formally that your function \isa{add} computes the sum of two BIGNATs correctly.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Using \isa{valid}, verify formally that your function \isa{add} preserves the validity of the BIGNAT representation.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\subsubsection*{Multiplication}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Define a function \isa{mult} that multiplies two BIGNATs with the same value for BASE. You may use \isa{add}, but not so often as to make the solution trivial. Make sure that your algorithm preserves the validity of the BIGNAT representation.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ mult\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ bigNat\ {\isasymRightarrow}\ bigNat\ {\isasymRightarrow}\ bigNat{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Using \isa{val}, verify formally that your function \isa{mult} computes the product of two BIGNATs correctly.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Using \isa{valid}, verify formally that your function \isa{mult} preserves the validity of the BIGNAT representation.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isanewline
+\isanewline
+\isanewline
+\isanewline
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a5/generated/session.tex Tue Apr 06 16:19:45 2004 +0200
@@ -0,0 +1,6 @@
+\input{a5.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a6/ROOT.ML Tue Apr 06 16:19:45 2004 +0200
@@ -0,0 +1,1 @@
+ use_thy "a6";
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a6/a6.thy Tue Apr 06 16:19:45 2004 +0200
@@ -0,0 +1,116 @@
+(*<*)
+theory a6 = Main:
+(*>*)
+
+
+subsection {* Optimising Compiler Verification *}
+
+text {*
+Section 3.3 of the Isabelle tutorial describes an expression compiler for a stack machine. In this exercise we will build and verify an optimising expression compiler for a register machine.
+*}
+
+text {*\subsubsection*{The Source Language: Expressions}*}
+
+text {*
+The arithmetic expressions we will work with consist of variables, constants, and an arbitrary binary operator @{text "oper"}.
+*}
+
+consts oper :: "nat \<Rightarrow> nat \<Rightarrow> nat";
+
+types var = string;
+
+datatype exp =
+ Const nat
+ | Var var
+ | Op exp exp
+;
+
+text {*
+The state in which an expression is evaluated is modelled by an {\em environment} function that maps variables to constants.
+*}
+
+types env = "var \<Rightarrow> nat";
+
+text {*
+Define a function @{text "value"} that evaluates an expression in a given environment.
+*}
+
+consts value :: "exp \<Rightarrow> env \<Rightarrow> nat";
+
+text {*\subsubsection*{The Register Machine}*}
+
+text {*
+As the name suggests, a register machine uses a collection of registers to store intermediate results. There exists a special register, called the accumulator, that serves as an implicit argument to each instruction. The rest of the registers make up the register file, and can be randomly accessed using an index.
+*}
+
+types regIndex = nat;
+
+datatype cell =
+ Acc
+ | Reg regIndex;
+
+
+text {*
+The state of the register machine is denoted by a function that maps storage cells to constants.
+*}
+
+types state = "cell \<Rightarrow> nat";
+
+text {*
+The instruction set for the register machine is defined as follows:
+*}
+
+datatype instr =
+ LI nat
+ -- "Load Immediate: loads a constant into the accumulator."
+| LOAD regIndex
+ -- "Loads the contents of a register into the accumulator."
+| STORE regIndex
+ -- "Saves the contents of the accumulator in a register."
+| OPER regIndex
+ -- {* Performs the binary operation @{text "oper"}.*}
+ -- "The first argument is taken from a register."
+ -- "The second argument is taken from the accumulator."
+ -- "The result of the computation is stored in the accumulator."
+;
+
+text {*
+A program is a list of such instructions. The result of running a program is a change of state of the register machine. Define a function @{text "exec"} that models this.
+*}
+
+consts exec :: "state \<Rightarrow> instr list \<Rightarrow> state"
+
+text {*\subsubsection*{Compilation}*}
+
+text {*
+The task now is to translate an expression into a sequence of instructions that computes it. At the end of execution, the result should be stored in the accumulator.
+
+Before execution, the values of each variable need to be stored somewhere in the register file. A {\it mapping} function maps variables to positions in the register file.
+*}
+
+types map = "var \<Rightarrow> regIndex";
+
+text {*
+Define a function @{text "cmp"} that compiles an expression into a sequence of instructions. The evaluation should proceed in a bottom-up depth-first manner.
+
+State and prove a theorem expressing the correctness of @{text "cmp"}.
+
+Hints:
+\begin{itemize}
+ \item The compilation function is dependent on the mapping function.
+ \item The compilation function needs some way of storing intermediate results. It should be clever enough to reuse registers it no longer needs.
+ \item It may be helpful to assume that at each recursive call, compilation is only allowed to use registers with indices greater than a given value to store intermediate results.
+\end{itemize}
+*}
+
+text {*\subsubsection*{Compiler Optimisation: Common Subexpressions}*}
+
+text {*
+In the previous section, the compiler @{text "cmp"} was allowed to evaluate a subexpression every time it occurred. In situations where arithmetic operations are costly, one may want to compute commonly occurring subexpressions only once.
+
+For example, to compute @{text "(a op b) op (a op b)"}, @{text "cmp"} was allowed three calls to @{text "oper"}, when only two were needed.
+
+Develop an optimised compiler @{text "optCmp"}, that evaluates every commonly occurring subexpression only once. Prove its correctness.
+*}
+
+(*<*) end (*>*)
\ No newline at end of file
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a6/generated/a6.tex Tue Apr 06 16:19:45 2004 +0200
@@ -0,0 +1,158 @@
+%
+\begin{isabellebody}%
+\def\isabellecontext{a{\isadigit{6}}}%
+\isamarkupfalse%
+%
+\isamarkupsubsection{Optimising Compiler Verification%
+}
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+Section 3.3 of the Isabelle tutorial describes an expression compiler for a stack machine. In this exercise we will build and verify an optimising expression compiler for a register machine.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\subsubsection*{The Source Language: Expressions}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The arithmetic expressions we will work with consist of variables, constants, and an arbitrary binary operator \isa{oper}.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ oper\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}nat\ {\isasymRightarrow}\ nat\ {\isasymRightarrow}\ nat{\isachardoublequote}\isanewline
+\isanewline
+\isamarkupfalse%
+\isacommand{types}\ var\ {\isacharequal}\ string\isanewline
+\isanewline
+\isamarkupfalse%
+\isacommand{datatype}\ exp\ {\isacharequal}\ \isanewline
+\ \ \ \ Const\ nat\ \isanewline
+\ \ {\isacharbar}\ Var\ var\isanewline
+\ \ {\isacharbar}\ Op\ exp\ exp\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+The state in which an expression is evaluated is modelled by an {\em environment} function that maps variables to constants.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{types}\ env\ {\isacharequal}\ {\isachardoublequote}var\ {\isasymRightarrow}\ nat{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define a function \isa{value} that evaluates an expression in a given environment.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ value\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}exp\ {\isasymRightarrow}\ env\ {\isasymRightarrow}\ nat{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\subsubsection*{The Register Machine}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+As the name suggests, a register machine uses a collection of registers to store intermediate results. There exists a special register, called the accumulator, that serves as an implicit argument to each instruction. The rest of the registers make up the register file, and can be randomly accessed using an index.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{types}\ regIndex\ {\isacharequal}\ nat\isanewline
+\isanewline
+\isamarkupfalse%
+\isacommand{datatype}\ cell\ {\isacharequal}\ \isanewline
+\ \ \ \ Acc\isanewline
+\ \ {\isacharbar}\ Reg\ regIndex\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+The state of the register machine is denoted by a function that maps storage cells to constants.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{types}\ state\ {\isacharequal}\ {\isachardoublequote}cell\ {\isasymRightarrow}\ nat{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+The instruction set for the register machine is defined as follows:%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{datatype}\ instr\ {\isacharequal}\ \isanewline
+\ \ LI\ nat\ \ \ \ \ \ \ \ \isanewline
+\ \ %
+\isamarkupcmt{Load Immediate: loads a constant into the accumulator.%
+}
+\ \isanewline
+{\isacharbar}\ LOAD\ regIndex\ \isanewline
+\ \ %
+\isamarkupcmt{Loads the contents of a register into the accumulator.%
+}
+\isanewline
+{\isacharbar}\ STORE\ regIndex\ \isanewline
+\ \ %
+\isamarkupcmt{Saves the contents of the accumulator in a register.%
+}
+\ \isanewline
+{\isacharbar}\ OPER\ regIndex\ \isanewline
+\ \ %
+\isamarkupcmt{Performs the binary operation \isa{oper}.%
+}
+\isanewline
+\ \ \ \ %
+\isamarkupcmt{The first argument is taken from a register.%
+}
+\isanewline
+\ \ \ \ %
+\isamarkupcmt{The second argument is taken from the accumulator.%
+}
+\ \isanewline
+\ \ \ \ %
+\isamarkupcmt{The result of the computation is stored in the accumulator.%
+}
+\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+A program is a list of such instructions. The result of running a program is a change of state of the register machine. Define a function \isa{exec} that models this.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{consts}\ exec\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}state\ {\isasymRightarrow}\ instr\ list\ {\isasymRightarrow}\ state{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+\subsubsection*{Compilation}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+The task now is to translate an expression into a sequence of instructions that computes it. At the end of execution, the result should be stored in the accumulator.
+
+Before execution, the values of each variable need to be stored somewhere in the register file. A {\it mapping} function maps variables to positions in the register file.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isacommand{types}\ map\ {\isacharequal}\ {\isachardoublequote}var\ {\isasymRightarrow}\ regIndex{\isachardoublequote}\isamarkupfalse%
+%
+\begin{isamarkuptext}%
+Define a function \isa{cmp} that compiles an expression into a sequence of instructions. The evaluation should proceed in a bottom-up depth-first manner.
+
+State and prove a theorem expressing the correctness of \isa{cmp}.
+
+Hints:
+\begin{itemize}
+ \item The compilation function is dependent on the mapping function.
+ \item The compilation function needs some way of storing intermediate results. It should be clever enough to reuse registers it no longer needs.
+ \item It may be helpful to assume that at each recursive call, compilation is only allowed to use registers with indices greater than a given value to store intermediate results.
+\end{itemize}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+\subsubsection*{Compiler Optimisation: Common Subexpressions}%
+\end{isamarkuptext}%
+\isamarkuptrue%
+%
+\begin{isamarkuptext}%
+In the previous section, the compiler \isa{cmp} was allowed to evaluate a subexpression every time it occurred. In situations where arithmetic operations are costly, one may want to compute commonly occurring subexpressions only once.
+
+For example, to compute \isa{{\isacharparenleft}a\ op\ b{\isacharparenright}\ op\ {\isacharparenleft}a\ op\ b{\isacharparenright}}, \isa{cmp} was allowed three calls to \isa{oper}, when only two were needed.
+
+Develop an optimised compiler \isa{optCmp}, that evaluates every commonly occurring subexpression only once. Prove its correctness.%
+\end{isamarkuptext}%
+\isamarkuptrue%
+\isamarkupfalse%
+\end{isabellebody}%
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End:
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/Exercises/2003/a6/generated/session.tex Tue Apr 06 16:19:45 2004 +0200
@@ -0,0 +1,6 @@
+\input{a6.tex}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "root"
+%%% End: