diff --git a/hw2/while-semantics.pdf b/hw2/while-semantics.pdf index fb59f46..a7d9bf8 100644 Binary files a/hw2/while-semantics.pdf and b/hw2/while-semantics.pdf differ diff --git a/hw2/while-semantics.tex b/hw2/while-semantics.tex index fe6f600..2f35dcc 100644 --- a/hw2/while-semantics.tex +++ b/hw2/while-semantics.tex @@ -45,8 +45,9 @@ you will implement the semantics for a small imperative language, named WHILE. \newcommand{\false}{\mbox{\tt false}} \newcommand{\note}[1]{\mbox{\tt not}~{#1}} -\begin{figure}\label{fig:lang} +\begin{figure}[H] \caption{The WHILE language} +\label{fig:lang} \[ \begin{array}{llr} \mydefhead{e ::=\qquad\qquad\qquad\qquad}{Expressions} @@ -58,7 +59,7 @@ you will implement the semantics for a small imperative language, named WHILE. \mydefcase{\ife e e e}{conditional expressions} \mydefcase{\whilee e e}{while expressions} \mydefcase{e ~boolop~ e}{boolean binary operations} - \mydefcase{\not e}{negation} + \mydefcase{\note e}{negation} \\ \mydefhead{v ::=\qquad\qquad\qquad\qquad}{Values} \mydefcase{i}{integer values} @@ -81,41 +82,8 @@ 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} +\section{Semantics} \newcommand{\bstep}[4]{{#1},{#2} \Downarrow {#3},{#4}} % Format for a big-step evaluation rule. @@ -129,183 +97,9 @@ Both choices, however, would complicate our language needlessly. \\~\\ } -\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} +\begin{figure}[H] \caption{Big-step semantics for WHILE} +\label{fig:bigstep} {\bf Runtime Syntax:} \[ \begin{array}{rclcl}