\documentclass[10pt]{article} \usepackage{611}
\usepackage{amsmath}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% CS611: Please fill in these macros as appropriate:
\newcommand{\homework}{1}      %%% Replace ? by homework number
\newcommand{\due}{09/17/01}    %%% Replace ??/??/?? by MM/DD/YY format
                               %%% due date
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\begin{document}
\hwheader

\section*{What to turn in}

Turn in the written parts of the assignment during class on the due date. For
the programming part, you should mail your version of the file
\texttt{interpretation.ml} and one interesting test case to
\texttt{nystrom@cs.cornell.edu} by 5{\sc pm} on that day.

\begin{enumerate}
\item {\sf Term equivalence}

\begin{enumerate}
\item \label{1a}
Using the large-step operational semantics of IMP, prove that the statement
$\IF~b~\THEN~c_0~\ELSE~c_1$ is equivalent to $\IF~\neg b~\THEN~c_1~\ELSE~c_0$.

\item \label{1b} Similarly, prove that command sequences in IMP can be either
left or right associative by showing that $(c_0;~c_1);~c_2$ is equivalent to
$c_0;~(c_1;~c_2)$

\end{enumerate}

\item {\sf Auto-increment expressions}

\newcommand\subst[2]{[#1/#2]}
\newcommand\inc{\mbox{\tt ++}}
\newcommand\var[1]{\mbox{\tt #1}}

Suppose we add C-like auto-increment expressions to IMP.  Given a variable $x$,
$x\inc$ will increment $x$ by 1 and evaluate to the previous value of $x$;
$\inc{}x$ will increment $x$ by 1 and evaluate to the new value of $x$.  For
example,
$$\var{ANSWER}~:=~1;~\WHILE~\var{i}\inc~\lt=~4~\DO~\var{ANSWER}~:=~\var{ANSWER}~*~\var{i}$$
stores 120 in the variable \var{ANSWER}, while
$$\var{ANSWER}~:=~1;~\WHILE~\inc\var{i}~\lt=~4~\DO~\var{ANSWER}~:=~\var{ANSWER}~*~\var{i}$$
stores 24 in the variable \var{ANSWER}.

\begin{enumerate}

\item \label{2a}
Write inference rules for the large-step operational semantics for the two
auto-increment expressions.

\item \label{2b}
Since expressions can now modify the store, the form of the evaluation
relations ($\stepsto$) for arithmetic and boolean expressions must change.
Explain how the form of the relations changes and describe how to rewrite the
inference rules for both expression types.  You do not have to write the new
inference rules.

\item \label{2c}
Another issue that arises when expressions can have side effects is that their
order of evaluation now matters.  The operational semantics for IMP presented
in class do not generally specify order of evaluation.  For example, the
inference rule in IMP for relational expressions:
$$\infer[\mbox{where } t \mbox{ is
true iff } n_0 \le n_1] {<a_0 \lt= a_1, \sigma>} {<a_0, \sigma> \stepsto n_0 &
<a_1,\sigma> \stepsto n_1}$$ does not specify which of $a_0$ and $a_1$ is
evaluated first.  Thus, if $x$ is initialized to 0, the expression
$x\inc~\lt=~x$ may evaluate to either true or false.  With these semantics, IMP
with auto-increment is non-deterministic.  Write the _small-step_ operational
semantics of IMP with auto-increment, being sure to define the language so that
it is deterministic.

\item \label{2d}
Use induction on derivations with the semantics you wrote for part~\ref{2c} to
prove that arithmetic expressions are deterministic.

\end{enumerate}

\item {\sf Adding \BREAK}
\label{break-prob}

IMP is lacking many features of a real programming language, most
notably functions and data structures, which we will study later.
In this problem you will add a mechanism like C's
\BREAK\  statement that allows a program to terminate
\WHILE\  loops early.  While this is a seemingly minor change to
the language, we will see that it radically alters the semantics of
IMP. 

As an example, the following program
(also found in \texttt{testB1.imp}) should
halt with the value 8 in location \texttt{ANSWER}:
\begin{verbatim}
                              while (true) do {
                                while (true) do {
                                  ANSWER := ANSWER + 1;
                                  if (ANSWER = 4) then {
                                    break;
                                    ANSWER := ANSWER + 10
                                  } else {
                                    skip
                                  }
                                };
                                ANSWER := ANSWER * 2;
                                break
                              }
\end{verbatim}

This example brings out several points when adding \BREAK\  to IMP.  First, if
the \BREAK\  occurs in a sequence of commands, the remainder of the sequence
(in this case \texttt{ANSWER := ANSWER + 10}) is not evaluated.  Second, there
must be a way to keep track of where the program will continue after evaluating
a \BREAK\ command.  Since \WHILE\  loops may be nested, these \BREAK\
continuations form a stack.  

A {\bf continuation} can be thought of as ``the rest of the evaluation of the
program'', and we will study them in more depth later.  For now, we can think
of continuations as ``the next command to be executed'', which, in general,
will be a sequence representing {\em all} of the commands remaining in the
program.  As we observed above, introducing \BREAK\  requires that we have the
ability to both discard the continuation of a command in a sequence and save a
continuation on a stack so we know where to pick up execution after evaluating
\BREAK.  This suggests that we modify IMP's program configurations to be the
following: \configB{c_{cur}}{c_{next}}{\rho}{\sigma}, where $c_{cur}$ is the
command currently being executed, $c_{next}$ is the continuation of $c_{cur}$,
$\rho$ is a stack of commands, written $c_{n} :: c_{n-1} :: \ldots :: c_1 ::
[]$, each $c_i$ representing the continuation of any \BREAK\  commands in the
body of a \WHILE\  loop with nesting depth $i$, and $\sigma$ is an IMP state as
usual.

\begin{figure}[t]
\hrulefill
\[
\begin{array}{rcl}
aexp_c & ::= & n \bnf \mathrm{Loc} \bnf aexp_c \;\mathtt{+}\; aexp_c
\bnf aexp_c \;\mathtt{*}\;aexp_c  \bnf aexp_c \;\mathtt{-}\; aexp_c \bnf \mathtt{(} \;aexp_c \;\mathtt{)}\\
\\
bexp_c & ::= & \mathtt{true} \bnf \mathtt{false} \bnf aexp_c \;
\mathtt{=} \; aexp_c \bnf aexp_c \; \mathtt{\lt=} \; aexp_c \bnf
\mathtt{not}\ bexp_c \\
 &  & \bnf bexp_c \; \mathtt{or} \; bexp_c \bnf bexp_c \; \mathtt{and} \;
 bexp_c \bnf \mathtt{(}\; bexp_c \;\mathtt{)}\\
\\
com_c & ::= & \mathtt{skip} \bnf \mathtt{break} \bnf \mathrm{Loc}\;
\mathtt{:=} \; aexp_c \bnf \mathtt{if\ (}\; bexp_c \;\mathtt{)\ then\ 
  \{}\; com_c \;\mathtt{\}\ else\ \{}\; com_c\; \mathtt{\}} \\
& & \bnf \mathtt{while\ (}\; bexp_c \; \mathtt{)\ do\ \{}\; com_c\;
\mathtt{\}} \bnf com_c \; \mathtt{;} \; com_c
\end{array}\]
\caption{IMP+\BREAK\ concrete syntax}
\label{imp+break}
\hrulefill
\end{figure}

There are a few subtle points to address.  The first question is this: What
happens when a \BREAK\  command is executed outside of any \WHILE\ 
-body (that is when $c_{cur} = \BREAK$ and $\rho = []$)?  This can be
considered an ill-formed program which should cause an error to
occur---our interpreter will model this by raising the exception
\texttt{BadBreak} defined in \texttt{interpretation.ml}.  A \BREAK\  command
which attempts to terminate more more loops than the current nesting level will
similarly fail.   The second question is this: What is the continuation of a
single-command program such as \texttt{X := 3}?  Since such an IMP program
should halt after executing the command, we could add a special \texttt{Halt}
continuation to the interpreter, but to make things easier, we will adopt the
convention that if the \SKIP\  command appears as $c_{next}$ then the program
is to terminate after evaluating $c_{cur}$.  (This makes the interpreter
slightly simpler to write.)

With these observations in hand, we can now specify the operational
semantics of IMP+\BREAK.  The new judgements will be of the
form $\configB{c_{cur}}{c_{next}}{\rho}{\sigma} \stepsto \sigma'$.  As
an example, consider the following inference rule specifying the
behavior of the assignment command:
\[
\Rule{\config{a}{\sigma} \stepsto n   \quad
      \configB{c_{next}}{\SKIP}{\rho}{\sigma[n/X]} \stepsto \sigma'}
     {\configB{X := a}{c_{next}}{\rho}{\sigma} \stepsto \sigma'}
\]

To evaluate the command $X := a$ followed by $c_{next}$ with \BREAK\ 
continuations $\rho$ and state $\sigma$, we first evaluate the
arithmetic expression $a$ in state $\sigma$ to obtain the number $n$.
Next we evaluate the continuation $c_{next}$ with \SKIP\  as its
continuation (indicating the program should then halt), the same $\rho$,
and a new state obtained from $\sigma$ by updating $X$ to be $n$.

Here is the axiom for specifying when a program halts:

\[
\Rule{}
     {\configB{\SKIP}{\SKIP}{[]}{\sigma} \stepsto \sigma}
\]

Here is the rule for evaluating a \SKIP\  command as part of a sequence
of other commands:

\[
\RuleSide{\configB{c_{next}}{\SKIP}{\rho}{\sigma} \stepsto \sigma'}
         {\configB{\SKIP}{c_{next}}{\rho}{\sigma} \stepsto \sigma'}
         {(c_{next} \not = \SKIP)}
\]

\begin{enumerate}
\item {\sf Operational Semantics}

Define the full set of operational semantics for IMP+\BREAK\ using the
rules above as guidelines.  You will need to define the proper
behavior for the interaction of \BREAK\ and \WHILE\ statements.  In
particular, \BREAK\ should discard $c_{next}$ and \WHILE\ should save
its continuation on the top of $\rho$.  Be careful!

\item {\sf Implementation}

The lexer and parser have already been modified to support the \BREAK\ 
command.  Implement the interpreter for IMP+\BREAK\ as the function
\texttt{interpretBreak~:~breakConfig~-\gt~state} found in the source file
\texttt{interpretation.ml}.  The stack of continuations, $\rho$, is
implemented by an \texttt{Ast.com list}.  This should be
straightforward, once you've decided what the operational semantics
should be.  Conversely, if you can implement the interpreter
correctly, you should be able to write down its operational semantics.
The only file you should modify is \texttt{interpretation.ml}.
No other file should be modified.

Note that on programs not containing the \BREAK\ command,
\texttt{test} and \texttt{testB} should agree.  Feel free to post
test cases to the newsgroup.  When you email in your source code, you should
submit one interesting test case of your own devising along with your modified
\texttt{interpretation.ml}.
\end{enumerate}

{\sf Getting started}

For problem~\ref{break-prob}, you should download the file \texttt{imp.tar.gz}
from the CS611 web page for Homework 1 and extract the contents to a
working directory.

These files contain the source code to a simple IMP interpreter (the
file \texttt{interpretation.ml}) as discussed in class.  To make it
easier for you to debug and test your code, we have written a lexer
and parser (the \texttt{lexer.mll} and \texttt{imp.mly} files).  We've
also included a pretty-printer for the abstract syntax
(\texttt{pprint.ml}).  The file \texttt{main.ml} contains two
functions, \texttt{test} and \texttt{testB}, both of type
\texttt{string~-\gt~int} that take the name of a file containing IMP code,
pretty-print it, interpret the program, and print out the result
contained in the ANSWER location.  The \texttt{testB} function will be
used to run IMP programs extended with a \texttt{break} construct
as described below.  Both of these functions can be called from the
top-loop of the ocaml system.  There are also a couple of example IMP
programs (\texttt{*.imp}).

Feel free to browse through the source code provided, but for the
purposes of this assignment, {\em the only file you should modify is}
\texttt{interpretation.ml}.  The other code makes use of OCaml's
module system, but you shouldn't need to know how it works to do this
assignment.

To compile your IMP interpreter, first untar \texttt{imp.tar.gz}.  Be sure
\texttt{ocaml} is in your path.  On the Solaris machines in the CS department,
it can be found at \texttt{/usr/u/plg/bin/sparc-solaris}. On the Windows
machines in the CS department, we have placed a copy in
\verb~\\bigbird\users\nystrom\ocaml~, or \verb~z:\nystrom\ocaml~ if
\verb~\\bigbird\users~ is mounted as usual.  You can download your own copy
of OCaml from the Caml web page at \texttt{http://caml.inria.fr}.  You make
have to adjust the \texttt{Makefile} or, on Windows, \texttt{make.bat} to point
to your installation of OCaml.  Now, run \texttt{make}.  This will run a batch
file on Windows and invoke \texttt{make} on Unix.  After the build completes,
you should have an executable named \texttt{imp}.  At this point you should be
able to run \texttt{ocamlrun imp test1.imp} at the prompt.  This will invoke
the interpreter for unmodified IMP.  Running \texttt{ocamlrun imp -break
test1.imp} will invoke your interpreter for IMP+\BREAK.  This should display
the error message ``Bad break.''

The concrete syntax of IMP is shown in Figure~\ref{imp+break}.  It is
essentially the abstract syntax discussed in class augmented with parentheses
and C-like syntax for \texttt{if} and \texttt{while} commands.  Locations are
denoted by strings containing only upper or lower case alphabetic characters.
Negative numbers are prefixed with \verb'~' as in ML.  Keywords are all in
lower case.  The arithmetic operators have the usual precedence and
associativity, and you can put parentheses in to group them.  Note that
\texttt{;} acts as a command separator not a terminator, so you will get parse
errors if you put \texttt{;} at the end of a sequence.

\end{enumerate}

\end{document}
