|
13841
|
1 |
%
|
|
|
2 |
\begin{isabellebody}%
|
|
|
3 |
\def\isabellecontext{a{\isadigit{3}}}%
|
|
|
4 |
\isamarkupfalse%
|
|
|
5 |
%
|
|
|
6 |
\isamarkupsubsection{Compilation%
|
|
|
7 |
}
|
|
|
8 |
\isamarkuptrue%
|
|
|
9 |
%
|
|
|
10 |
\begin{isamarkuptext}%
|
|
|
11 |
This exercise deals with the compiler example in section~3.3
|
|
|
12 |
of \cite{isabelle-tutorial}. The simple side effect free expressions
|
|
|
13 |
are extended with side effects.
|
|
|
14 |
\begin{enumerate}
|
|
|
15 |
|
|
|
16 |
\item Read sections 3.3 and 8.2 of \cite{isabelle-tutorial}. Study
|
|
|
17 |
the section about \isa{fun{\isacharunderscore}upd} in theory \isa{Fun} of HOL:
|
|
|
18 |
\isa{fun{\isacharunderscore}upd\ f\ x\ y}, written \isa{f{\isacharparenleft}x{\isacharcolon}{\isacharequal}y{\isacharparenright}}, is \isa{f}
|
|
|
19 |
updated at \isa{x} with new value \isa{y}.
|
|
|
20 |
|
|
|
21 |
\item Extend data type \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ expr} with a new alternative
|
|
|
22 |
\isa{Assign\ x\ e} that shall represent an assignment \isa{x\ {\isacharequal}\ e} of the value of the expression \isa{e} to the variable \isa{x}.
|
|
|
23 |
The value of an assignment shall be the value of \isa{e}.
|
|
|
24 |
|
|
|
25 |
\item Modify the evaluation function \isa{value} such that it can
|
|
|
26 |
deal with assignments. Note that since the evaluation of an expression
|
|
|
27 |
may now change the environment, it no longer suffices to return only
|
|
|
28 |
the value from the evaluation of an expression.
|
|
|
29 |
|
|
|
30 |
Define a function \isa{se{\isacharunderscore}free\ {\isacharcolon}{\isacharcolon}\ expr\ {\isasymRightarrow}\ bool} that
|
|
|
31 |
identifies side effect free expressions. Show that \isa{se{\isacharunderscore}free\ e}
|
|
|
32 |
implies that evaluation of \isa{e} does not change the environment.
|
|
|
33 |
|
|
|
34 |
\item Extend data type \isa{{\isacharparenleft}{\isacharprime}a{\isacharcomma}\ {\isacharprime}v{\isacharparenright}\ instr} with a new instruction
|
|
|
35 |
\isa{Store\ x} that stores the topmost element on the stack in
|
|
|
36 |
address/variable \isa{x}, without removing it from the stack.
|
|
|
37 |
Update the machine semantics \isa{exec} accordingly. You will face
|
|
|
38 |
the same problem as in the extension of \isa{value}.
|
|
|
39 |
|
|
|
40 |
\item Modify the compiler \isa{comp} and its correctness proof to
|
|
|
41 |
accommodate the above changes.
|
|
|
42 |
\end{enumerate}%
|
|
|
43 |
\end{isamarkuptext}%
|
|
|
44 |
\isamarkuptrue%
|
|
|
45 |
\isamarkupfalse%
|
|
|
46 |
\end{isabellebody}%
|
|
|
47 |
%%% Local Variables:
|
|
|
48 |
%%% mode: latex
|
|
|
49 |
%%% TeX-master: "root"
|
|
|
50 |
%%% End:
|