diff --git a/hw2/while-semantics.pdf b/hw2/while-semantics.pdf index ae02da6..d97dae0 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 71038ba..31c9993 100644 --- a/hw2/while-semantics.tex +++ b/hw2/while-semantics.tex @@ -20,7 +20,7 @@ \author{ CS 252: Advanced Programming Languages \\ - Prof. Thomas H. Austin \\ + Yuri Tatishchev \\ San Jos\'{e} State University \\ } \date{} @@ -113,6 +113,17 @@ 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\ @@ -288,5 +299,77 @@ Finally, implement the interpreter to match your semantics. \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''} +% } +\end{array} +\] +\end{figure} + + \end{document}