172 lines
4.8 KiB
TeX
172 lines
4.8 KiB
TeX
\documentclass{article}
|
|
|
|
\usepackage{fullpage}
|
|
%\usepackage{citesort}
|
|
%\usepackage{url}
|
|
%\usepackage{listings}
|
|
\usepackage{color}
|
|
|
|
|
|
% Commands for formatting figures
|
|
\newcommand{\mydefhead}[2]{\multicolumn{2}{l}{{#1}}&\mbox{\emph{#2}}\\}
|
|
\newcommand{\mydefcase}[2]{\qquad\qquad& #1 &\mbox{#2}\\}
|
|
|
|
% Commands for language expressions and values
|
|
\newcommand{\true}{\mbox{\tt true}}
|
|
\newcommand{\false}{\mbox{\tt false}}\title{Operational Semantics for BoolInt* Language}
|
|
\newcommand{\ife}[3]{\mbox{\tt if}~{#1}~\mbox{\tt then}~{#2}~\mbox{\tt else}~{#3}}
|
|
\newcommand{\suc}[1]{\mbox{\tt succ}~{#1}}
|
|
\newcommand{\prd}[1]{\mbox{\tt pred}~{#1}}
|
|
|
|
% Big-step evaluation relation.
|
|
% #1 is the expression.
|
|
% #2 is the resulting value.
|
|
\newcommand{\bstep}[2]{{#1} \Downarrow {#2}}
|
|
|
|
% Command for formatting the name of the evaluation relation.
|
|
\newcommand{\rel}[1]{ \mbox{\sc [#1]} }
|
|
|
|
% 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}}
|
|
\\~\\
|
|
}
|
|
|
|
\author{
|
|
Yuri Tatishchev \\
|
|
San Jos\'{e} State University \\
|
|
iurii.tatishchev@sjsu.edu
|
|
}
|
|
|
|
\begin{document}
|
|
\maketitle
|
|
|
|
\begin{abstract}
|
|
In this paper, we will provide a review of the big-step operational semantics
|
|
for the BoolInt* language we discussed in class.
|
|
\end{abstract}
|
|
|
|
%%%%
|
|
%\section{Introduction}
|
|
|
|
BoolInt* is a very minimal language that allows us to experiment with operational semantics.
|
|
|
|
First, we define the valid expressions in our language.
|
|
These expressions dictate the possibilities of what expressions
|
|
we may have in our source programs.
|
|
(Note that other language might also have {\em statements}.
|
|
Statements might not evaluate to a value;
|
|
expressions always will.)
|
|
|
|
\begin{figure}
|
|
\caption{The BoolInt* language}
|
|
\label{fig:lang}
|
|
\[
|
|
\begin{array}{ll@{\qquad\qquad}l}
|
|
\mydefhead{e ::=\qquad\qquad\qquad\qquad}{Expressions}
|
|
\mydefcase{\true}{true value}
|
|
\mydefcase{\false}{false value}
|
|
\mydefcase{i}{integers}
|
|
\mydefcase{\ife e e e}{conditional expressions}
|
|
\mydefcase{\suc e}{successor}
|
|
\mydefcase{\prd e}{predecessor}
|
|
\\
|
|
\mydefhead{v ::=\qquad\qquad\qquad\qquad}{Values}
|
|
\mydefcase{\true}{true value}
|
|
\mydefcase{\false}{false value}
|
|
\mydefcase{i}{integers}
|
|
\end{array}
|
|
\]
|
|
\end{figure}
|
|
|
|
Figure~\ref{fig:lang} shows the list of expressions and values for the BoolInt* language.
|
|
Expressions can be the value $\true$, the value $\false$,
|
|
or the conditional expression $\ife e e e$.
|
|
Note that conditional expressions have a recursive structure,
|
|
with 3 sub-expressions.
|
|
|
|
After evaluating a program, we should be able to produce a value in this language.
|
|
(In other languages, we might hit a bad situation and need to crash instead;
|
|
that won't happen in this language.)
|
|
The valid values for BoolInt* are $\true$, $\false$, and $i$.
|
|
|
|
With our expressions and values defined,
|
|
we can now specify the semantics for our language.
|
|
To do so, we will use the following big-step evaluation relation:
|
|
|
|
\[
|
|
\bstep{e}{v}
|
|
\]
|
|
|
|
The above line should be read as ``the expression $e$ evaluates to the value $v$''.
|
|
|
|
\begin{figure}
|
|
\caption{Big-step semantics for BoolInt*}
|
|
\label{fig:bigstep}
|
|
{\bf Evaluation Rules:~~~ \fbox{$\bstep{e}{v}$}} \\
|
|
\[
|
|
\begin{array}{r@{\qquad\qquad}c}
|
|
\bsrule{B-Value}{}{
|
|
\bstep{v}{v}
|
|
}
|
|
\bsrule{B-IfTrue}{
|
|
\bstep{e_1}{\true} \\
|
|
\bstep{e_2}{v}
|
|
}{
|
|
\bstep{\ife{e_1}{e_2}{e_3}}{v}
|
|
}
|
|
\bsrule{B-IfFalse}{
|
|
\bstep{e_1}{\false} \\
|
|
\bstep{e_3}{v}
|
|
}{
|
|
\bstep{\ife{e_1}{e_2}{e_3}}{v}
|
|
}
|
|
\bsrule{B-Succ}{
|
|
\bstep{e}{i}
|
|
}{
|
|
\bstep{\suc{e}}{i+1}
|
|
}
|
|
\bsrule{B-Pred}{
|
|
\bstep{e}{i}
|
|
}{
|
|
\bstep{\prd{e}}{i-1}
|
|
}
|
|
\end{array}
|
|
\]
|
|
\end{figure}
|
|
|
|
|
|
|
|
Figure~\ref{fig:bigstep} shows the big-step evaluation rules for the BoolInt* language.
|
|
Of course, there are additional possible rules.
|
|
|
|
The \rel{B-Value} rule applies when the expression (to the left of ``$\Downarrow$'')
|
|
is also a value, as defined in Figure~\ref{fig:lang}.
|
|
There are no premises for this rule (above the line),
|
|
meaning that it is an {\em axiom}.
|
|
This rule states that a value evaluates to itself,
|
|
so that \true{} evaluates to \true{} and \false{} evaluates to \false{}.
|
|
|
|
Two different rules are needed for handling conditional expressions.
|
|
Which rule applies depends on the premises.
|
|
|
|
For the \rel{B-IfTrue} rule,
|
|
the premise states that $e_1$ evaluates to \true{}
|
|
and $e_2$ evaluates to some value $v$.
|
|
If the premise holds, then the result of evaluating the expression is the value $v$.
|
|
The structure of \rel{B-IfFalse} is similar.
|
|
|
|
We also have rules for handling the integer operations.
|
|
The \rel{B-Succ} rule states that if the operand $e$ evaluates to an integer $i$,
|
|
then the expression $\suc e$ evaluates to $i+1$.
|
|
Similarly, \rel{B-Pred} evaluates $\prd e$ to $i-1$ if $e$ evaluates to $i$.
|
|
|
|
|
|
\end{document}
|
|
|