\documentclass{article}

\usepackage{fullpage}
\usepackage{listings}
\usepackage{amsmath}
\usepackage{amsthm}
\usepackage{amssymb}
%\usepackagen{url}
\usepackage{float}
\usepackage{paralist}

\floatstyle{boxed}
\restylefloat{figure}



\newcommand{\rel}[1]{ \mbox{\sc [#1]} }

\title{Homework 2: Operational Semantics for WHILE}

\author{
  CS 252: Advanced Programming Languages \\
  Yuri Tatishchev \\
  San Jos\'{e} State University \\
  }
\date{}

\begin{document}
\maketitle

\section{Introduction}

For this assignment,
you will implement the semantics for a small imperative language, named WHILE.

% Commands for formatting figure
\newcommand{\mydefhead}[2]{\multicolumn{2}{l}{{#1}}&\mbox{\emph{#2}}\\}
\newcommand{\mydefcase}[2]{\qquad\qquad& #1 &\mbox{#2}\\}

% Commands for language format
\newcommand{\assign}[2]{#1~{:=}~#2}
\newcommand{\ife}[3]{\mbox{\tt if}~{#1}~\mbox{\tt then}~{#2}~\mbox{\tt else}~{#3}}
\newcommand{\whilee}[2]{\mbox{\tt while}~(#1)~#2}
\newcommand{\true}{\mbox{\tt true}}
\newcommand{\false}{\mbox{\tt false}}
\newcommand{\note}[1]{\mbox{\tt not}~{#1}}

\begin{figure}[H]
\caption{The WHILE language}
\label{fig:lang}
\[
\begin{array}{llr}
  \mydefhead{e ::=\qquad\qquad\qquad\qquad}{Expressions}
  \mydefcase{x}{variables/addresses}
  \mydefcase{v}{values}
  \mydefcase{\assign x e}{assignment}
  \mydefcase{e; e}{sequential expressions}
  \mydefcase{e ~op~ e}{binary operations}
  \mydefcase{\ife e e e}{conditional expressions}
  \mydefcase{\whilee e e}{while expressions}
  \mydefcase{e ~boolop~ e}{boolean binary operations}
  \mydefcase{\note e}{negation}
  \\
  \mydefhead{v ::=\qquad\qquad\qquad\qquad}{Values}
  \mydefcase{i}{integer values}
  \mydefcase{b}{boolean values}
  \\
  op ::= & + ~|~ - ~|~ * ~|~ / ~|~ > ~|~ >= ~|~ < ~|~ <=  & \mbox{\emph{Binary operators}} \\
  \\
  boolop ::= & and ~|~ or  & \mbox{\emph{Boolean binary operators}} \\
\end{array}
\]
\end{figure}

The language for WHILE is given in Figure~\ref{fig:lang}.
Unlike the Bool* language we discussed previously,
WHILE supports \emph{mutable references}.
The state of these references is maintained in a \emph{store},
a mapping of references to values.
(``Store'' can be thought of as a synonym for heap.)
Once we have mutable references, other language constructs become more useful,
such as sequencing operations ($e_1;e_2$).


%--------------
\section{Semantics}
\newcommand{\bstep}[4]{{#1},{#2} \Downarrow {#3},{#4}}

% Format for a big-step evaluation rule.
% #1 is the name of the rule.
% #2 are the premises.  Leave blank if there are none.
% #3 is the conclusion.
\newcommand{\bsrule}[3]{
  \rel{#1} &
  \frac{\strut\begin{array}{@{}c@{}} #2 \end{array}}
       {\strut\begin{array}{@{}c@{}} #3 \end{array}}
   \\~\\
}

\begin{figure}[H]
\caption{Big-step semantics for WHILE}
\label{fig:bigstep}
{\bf Runtime Syntax:}
\[
\begin{array}{rclcl}
  \sigma & \in & {Store} \quad  & = & \quad {variable} ~\rightarrow ~v \\
  \\
\end{array}
\]
{\bf Evaluation Rules:~~~ \fbox{$\bstep{e}{\sigma}{e'}{\sigma'}$}} \\
\[
\begin{array}{r@{\qquad\qquad}c}
\bsrule{B-Value}{}{
  \bstep{v}{\sigma}{v}{\sigma}
}
\bsrule{B-Var}{
  x \in domain(\sigma) \qquad \sigma(x)=v
}{
  \bstep{x}{\sigma}{v}{\sigma}
}
\bsrule{B-Assign}{
  \bstep{e}{\sigma}{v}{\sigma'}
}{
  \bstep{\assign{x}{e}}{\sigma}{v}{\sigma'[x:=v]}
}
\bsrule{B-Seq}{
  \bstep{e_1}{\sigma}{v_1}{\sigma'} \\
  \bstep{e_2}{\sigma'}{v_2}{\sigma''}
}{
  \bstep{e_1;e_2}{\sigma}{v_2}{\sigma''}
}
\bsrule{B-Op}{
  \bstep{e_1}{\sigma}{v_1}{\sigma'} \\
  \bstep{e_2}{\sigma'}{v_2}{\sigma''} \\
  v = apply(op, v_1, v_2)
}{
  \bstep{e_1~op~e_2}{\sigma}{v}{\sigma''}
}
\bsrule{B-IfTrue}{
  \bstep{e_1}{\sigma}{\true}{\sigma'} \\
  \bstep{e_2}{\sigma'}{v}{\sigma''}
}{
  \bstep{\ife{e_1}{e_2}{e_3}}{\sigma}{v}{\sigma''}
}
\bsrule{B-IfFalse}{
  \bstep{e_1}{\sigma}{\false}{\sigma'} \\
  \bstep{e_3}{\sigma'}{v}{\sigma''}
}{
  \bstep{\ife{e_1}{e_2}{e_3}}{\sigma}{v}{\sigma''}
}
\bsrule{B-WhileTrue}{
  \bstep{e_1}{\sigma}{\true}{\sigma'} \\
  \bstep{e_2}{\sigma'}{v_1}{\sigma''} \\
  \bstep{\whilee{e_1}{e_2}}{\sigma''}{v}{\sigma'''}
}{
  \bstep{\whilee{e_1}{e_2}}{\sigma}{v}{\sigma'''}
}
\bsrule{B-WhileFalse}{
  \bstep{e_1}{\sigma}{\false}{\sigma'}
}{
  \bstep{\whilee{e_1}{e_2}}{\sigma}{\false}{\sigma'}
}
% \bsrule{B-While}{
%   \bstep{e_1}{\sigma}{v_1}{\sigma'} \\
%   \bstep{e_2}{\sigma'}{v_2}{\sigma''}
% }{
%   \bstep{\whilee{e_1}{e_2}}{\sigma}{\ife{v_1}{e_2;\whilee{e_1}{e_2}}{\false}}{\sigma''}
% }
\bsrule{B-Not}{
  \bstep{e}{\sigma}{b}{\sigma'}
}{
  \bstep{\note{e}}{\sigma}{\neg b}{\sigma'}
}
\bsrule{B-BoolOp}{
  \bstep{e_1}{\sigma}{b_1}{\sigma'} \\
  \bstep{e_2}{\sigma'}{b_2}{\sigma''} \\
  b = apply(boolop, b_1, b_2)
}{
  \bstep{e_1~boolop~e_2}{\sigma}{b}{\sigma''}
}
\end{array}
\]
\end{figure}


\end{document}