393 lines
9.8 KiB
TeX
393 lines
9.8 KiB
TeX
\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}\label{fig:lang}
|
|
\caption{The WHILE language}
|
|
\[
|
|
\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{\not 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{Small-step semantics}
|
|
|
|
\newcommand{\ssrule}[3]{
|
|
\rel{#1} &
|
|
\frac{\strut\begin{array}{@{}c@{}} #2 \end{array}}
|
|
{\strut\begin{array}{@{}c@{}} #3 \end{array}}
|
|
\\~\\
|
|
}
|
|
%\newcommand{\sstep}[4]{\ctxt[{#1}],{#2} \rightarrow \ctxt[{#3}],{#4}}
|
|
%\newcommand{\sstepraw}[4]{{#1},{#2} \rightarrow {#3},{#4}}
|
|
\newcommand{\sstep}[4]{{#1},{#2} \rightarrow {#3},{#4}}
|
|
\newcommand{\ctxt}{C}
|
|
|
|
The small-step semantics for WHILE are given in Figure~\ref{fig:smallstep}.
|
|
%For the sake of brevity, these rules use \emph{evaluation contexts} ($\ctxt$),
|
|
%which specify which \emph{redex} will be evaluated next.
|
|
%The evaluation rules then apply to the ``hole'' ($\bullet$) in this context.
|
|
%
|
|
Most of these rules are fairly straightforward, but there are a couple of points
|
|
to note with the $\rel{ss-while}$ rule.
|
|
First of all, this is the only rule that makes a more complex expression
|
|
when it has finished.
|
|
(This rule is much cleaner when specified with the big-step operational semantics.)
|
|
|
|
Secondly, note the final value of this expression once the while loop completes.
|
|
It will \emph{always} be {\false} when it completes.
|
|
We could have created a special value, such as {\tt null},
|
|
or we could have made the while loop a statement that returns no value.
|
|
Both choices, however, would complicate our language needlessly.
|
|
|
|
|
|
%--------------
|
|
\section{YOUR ASSIGNMENT}
|
|
\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}}
|
|
\\~\\
|
|
}
|
|
|
|
\noindent
|
|
{\bf Part 1:}
|
|
Rewrite the operational semantic rules for WHILE in \LaTeX\
|
|
to use big-step operational semantics instead.
|
|
Submit both your \LaTeX\ source and the generated PDF file.
|
|
|
|
Extend your semantics with features to handle boolean values.
|
|
{\bf Do not treat these a binary operators.}
|
|
Specifically, add support for:
|
|
\begin{compactitem}
|
|
\item {\tt and}
|
|
\item {\tt or}
|
|
\item {\tt not}
|
|
\end{compactitem}
|
|
|
|
The exact behavior of these new features is up to you,
|
|
but should seem reasonable to most programmers.
|
|
|
|
\bigskip
|
|
\noindent
|
|
{\bf Part 2:}
|
|
Once you have your semantics defined,
|
|
download {\tt WhileInterp.hs} and implement the {\tt evaluate} function,
|
|
as well as any additional functions you need.
|
|
Your implementation must be consistent with your operational semantics,
|
|
{\it including your extensions for {\tt and}, {\tt or}, and {\tt not}}.
|
|
Also, you may not change any type signatures provided in the file.
|
|
|
|
Finally, implement the interpreter to match your semantics.
|
|
|
|
\bigskip
|
|
\noindent
|
|
{\bf Zip all files together into {\tt hw2.zip} and submit to Canvas.}
|
|
|
|
|
|
|
|
|
|
|
|
%\begin{figure}[H]\label{fig:smallstep}
|
|
%\caption{Small-step semantics for WHILE}
|
|
%{\bf Runtime Syntax:}
|
|
%\[
|
|
%\begin{array}{rclcl}
|
|
% \ctxt & \in & {Context} \quad & ::= & \quad \ctxt; e
|
|
% ~|~ \ctxt ~op~ e
|
|
% ~|~ v ~op~ \ctxt
|
|
% ~|~ \assign{x}{\ctxt}
|
|
% ~|~ \ife{\ctxt}{e_1}{e_2}
|
|
% ~|~ \bullet \\
|
|
% \sigma & \in & {Store} \quad & = & \quad {variable} ~\rightarrow ~v \\
|
|
% \\
|
|
%\end{array}
|
|
%\]
|
|
%{\bf Evaluation Rules:~~~ \fbox{$\sstepraw{e}{\sigma}{e'}{\sigma'}$}} \\
|
|
%\[
|
|
%\begin{array}{cc}
|
|
%\begin{array}{r@{\qquad}l}
|
|
%\ssrule{ss-var}{
|
|
% x \in domain(\sigma) \qquad \sigma(x)=v
|
|
%}{
|
|
% \sstep{x}{\sigma}{v}{\sigma}
|
|
%}
|
|
%\ssrule{ss-assign}{
|
|
%}{
|
|
% \sstep{\assign{x}{v}}{\sigma}{v}{\sigma[x:=v]}
|
|
%}
|
|
%\ssrule{ss-op}{
|
|
% v = v_1 ~op~ v_2
|
|
%}{
|
|
% \sstep{v_1~op~v_2}{\sigma}{v}{\sigma}
|
|
%}
|
|
%\end{array}
|
|
% &
|
|
%\begin{array}{r@{\qquad}l}
|
|
%\ssrule{ss-seq}{
|
|
%}{
|
|
% \sstep{v;e}{\sigma}{e}{\sigma}
|
|
%}
|
|
%\ssrule{ss-iftrue}{
|
|
%}{
|
|
% \sstep{\ife{\true}{e_1}{e_2}}{\sigma}{e_1}{\sigma}
|
|
%}
|
|
%\ssrule{ss-iffalse}{
|
|
%}{
|
|
% \sstep{\ife{\false}{e_1}{e_2}}{\sigma}{e_2}{\sigma}
|
|
%}
|
|
%\ssrule{ss-while}{
|
|
%}{
|
|
% \sstep{\whilee{e_1}{e_2}}{\sigma}{\ife{e_1}{e_2;\whilee{e_1}{e_2}}{\false}}{\sigma}
|
|
%}
|
|
%\end{array}
|
|
%\end{array}
|
|
%\]
|
|
%\end{figure}
|
|
%
|
|
|
|
\begin{figure}[H]\label{fig:smallstep}
|
|
\caption{Small-step semantics for WHILE}
|
|
{\bf Runtime Syntax:}
|
|
\[
|
|
\begin{array}{rclcl}
|
|
\sigma & \in & {Store} \quad & = & \quad {variable} ~\rightarrow ~v \\
|
|
\\
|
|
\end{array}
|
|
\]
|
|
{\bf Evaluation Rules:~~~ \fbox{$\sstep{e}{\sigma}{e'}{\sigma'}$}} \\
|
|
\[
|
|
%\begin{array}{cc}
|
|
\begin{array}{r@{\qquad}l}
|
|
\ssrule{ss-seqctx}{
|
|
\sstep{e_1}{\sigma}{e_1'}{\sigma'}
|
|
}{
|
|
\sstep{e_1;e_2}{\sigma}{e_1';e_2}{\sigma'}
|
|
}
|
|
\ssrule{ss-seq}{
|
|
}{
|
|
\sstep{v;e}{\sigma}{e}{\sigma}
|
|
}
|
|
\ssrule{ss-opctx1}{
|
|
\sstep{e_1}{\sigma}{e_1'}{\sigma'}
|
|
}{
|
|
\sstep{e_1~op~e_2}{\sigma}{e_1'~op~e_2}{\sigma'}
|
|
}
|
|
\ssrule{ss-opctx2}{
|
|
\sstep{e_2}{\sigma}{e_2'}{\sigma'}
|
|
}{
|
|
\sstep{v_1~op~e_2}{\sigma}{v_1~op~e_2'}{\sigma'}
|
|
}
|
|
\ssrule{ss-op}{
|
|
v = v_1 ~op~ v_2
|
|
}{
|
|
\sstep{v_1~op~v_2}{\sigma}{v}{\sigma}
|
|
}
|
|
\end{array}
|
|
\begin{array}{r@{\qquad}l}
|
|
\ssrule{ss-var}{
|
|
x \in domain(\sigma) \qquad \sigma(x)=v
|
|
}{
|
|
\sstep{x}{\sigma}{v}{\sigma}
|
|
}
|
|
\ssrule{ss-assignctx}{
|
|
\sstep{e_1}{\sigma}{e_1'}{\sigma'}
|
|
}{
|
|
\sstep{\assign{x}{e}}{\sigma}{\assign{x}{e'}}{\sigma'}
|
|
}
|
|
\ssrule{ss-assign}{
|
|
}{
|
|
\sstep{\assign{x}{v}}{\sigma}{v}{\sigma[x:=v]}
|
|
}
|
|
\ssrule{ss-iftrue}{
|
|
}{
|
|
\sstep{\ife{\true}{e_1}{e_2}}{\sigma}{e_1}{\sigma}
|
|
}
|
|
\ssrule{ss-iffalse}{
|
|
}{
|
|
\sstep{\ife{\false}{e_1}{e_2}}{\sigma}{e_2}{\sigma}
|
|
}
|
|
\end{array}
|
|
\]
|
|
\[
|
|
\begin{array}{r@{\qquad}l}
|
|
\ssrule{ss-ifctx}{
|
|
\sstep{e_1}{\sigma}{e_1'}{\sigma'}
|
|
}{
|
|
\sstep{\ife{e_1}{e_2}{e_3}}{\sigma}{\ife{e_1'}{e_2}{e_3}}{\sigma'}
|
|
}
|
|
\ssrule{ss-while}{
|
|
}{
|
|
\sstep{\whilee{e_1}{e_2}}{\sigma}{\ife{e_1}{e_2;\whilee{e_1}{e_2}}{\false}}{\sigma}
|
|
}
|
|
\end{array}
|
|
\]
|
|
\end{figure}
|
|
|
|
|
|
\begin{figure}[H]\label{fig:bigstep}
|
|
\caption{Big-step semantics for WHILE}
|
|
{\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}{\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}
|
|
|