mirror of
https://github.com/ProgramSnail/Lama.git
synced 2025-12-06 06:48:48 +00:00
Lectures
This commit is contained in:
Dmitry Boulytchev
parent
29efb45353
commit
ef8ea21216
5 changed files with 140 additions and 103 deletions
34
doc/04.tex
34
doc/04.tex
|
|
@ -24,25 +24,35 @@ In the concrete syntax for the constructs we add the closing keywords ``\llang{i
|
|||
\]
|
||||
|
||||
\begin{figure}[t]
|
||||
|
||||
\[\trans{c}{\llang{skip}}{c}\ruleno{Skip$_{bs}$}\]
|
||||
\arraycolsep=10pt
|
||||
%\def\arraystretch{2.9}
|
||||
\[\trans{c}{\llang{skip}}{c}\ruleno{Skip$_{bs}$}\]\vskip2mm
|
||||
\[
|
||||
\crule{\trans{c}{\mbox{$S_1$}}{c^\prime}}
|
||||
\trule{\begin{array}{cc}
|
||||
\sembr{e}\;s\ne 0 & \trans{c}{\mbox{$S_1$}}{c^\prime}
|
||||
\end{array}}
|
||||
{\trans{c=\inbr{s, \_, \_}}{\llang{if $\;e\;$ then $\;S_1\;$ else $\;S_2\;$}}{c^\prime}}
|
||||
{\sembr{e}\;s\ne 0}\ruleno{If-True$_{bs}$}
|
||||
\]
|
||||
\ruleno{If-True$_{bs}$}
|
||||
\]\vskip2mm
|
||||
\[
|
||||
\crule{\trans{c}{\mbox{$S_2$}}{c^\prime}}
|
||||
\trule{\begin{array}{cc}
|
||||
\sembr{e}\;s=0 & \trans{c}{\mbox{$S_1$}}{c^\prime}
|
||||
\end{array}}
|
||||
{\trans{c=\inbr{s, \_, \_}}{\llang{if $\;e\;$ then $\;S_1\;$ else $\;S_2\;$}}{c^\prime}}
|
||||
{\sembr{e}\;s=0}\ruleno{If-False$_{bs}$}
|
||||
\]
|
||||
\ruleno{If-False$_{bs}$}
|
||||
\]\vskip3mm
|
||||
\[
|
||||
\crule{\trans{c}{\llang{$S$}}{c^\prime},\;\trans{c^\prime}{\llang{while $\;e\;$ do $\;S\;$}}{c^{\prime\prime}}}
|
||||
\trule{\begin{array}{ccc}
|
||||
{\sembr{e}\;s\ne 0} & \trans{c}{\llang{$S$}}{c^\prime} & \trans{c^\prime}{\llang{while $\;e\;$ do $\;S\;$}}{c^{\prime\prime}}\\
|
||||
\end{array}
|
||||
}
|
||||
{\trans{c=\inbr{s, \_, \_}}{\llang{while $\;e\;$ do $\;S\;$}}{c^{\prime\prime}}}
|
||||
{\sembr{e}\;s\ne 0}\ruleno{While-True$_{bs}$}
|
||||
\]
|
||||
\ruleno{While-True$_{bs}$}
|
||||
\]\vskip3mm
|
||||
\[
|
||||
\ctrans{c=\inbr{s, \_, \_}}{\llang{while $\;e\;$ do $\;S\;$}}{c}{\sembr{e}\;s=0}\ruleno{While-False$_{bs}$}
|
||||
\trule{\sembr{e}\;s=0}
|
||||
{\trans{c=\inbr{s, \_, \_}}{\llang{while $\;e\;$ do $\;S\;$}}{c}}
|
||||
\ruleno{While-False$_{bs}$}
|
||||
\]
|
||||
\caption{Big-step operational semantics for control flow statements}
|
||||
\label{bs_stmt_cf}
|
||||
|
|
|
|||
12
doc/05.tex
12
doc/05.tex
|
|
@ -94,8 +94,8 @@ Finally, we need two transformations for states:
|
|||
|
||||
\[
|
||||
\begin{array}{rcl}
|
||||
\mbox{\textbf{enter}}\,\inbr{\sigma_g,\,\_,\,\_}\,S & = & \inbr{\sigma_g,\,S,\,\bot}\\
|
||||
\mbox{\textbf{leave}}\,\inbr{\sigma_g,\,\_,\,\_}\,\inbr{\_,\,S,\,\sigma_l}& = & \inbr{\sigma_g,\,S,\,\sigma_l}
|
||||
\primi{enter}{\inbr{\sigma_g,\,\_,\,\_}\,S} & = & \inbr{\sigma_g,\,S,\,\bot}\\
|
||||
\primi{leave}{\inbr{\sigma_g,\,\_,\,\_}\,\inbr{\_,\,S,\,\sigma_l}}& = & \inbr{\sigma_g,\,S,\,\sigma_l}
|
||||
\end{array}
|
||||
\]
|
||||
|
||||
|
|
@ -110,8 +110,8 @@ propagate this environment, adding $\withenv{\Gamma}{...}$ for each transition `
|
|||
need now is to describe the rule for procedure calls:
|
||||
|
||||
\[
|
||||
\trule{\withenv{\Gamma}{\trans{\inbr{\mbox{\textbf{enter}}\;\sigma\,(\bar{a}@\bar{l})[\overline{a\gets\sembr{e}\sigma}],\,i,\,o}}{S}{\inbr{\sigma^\prime,\,i^\prime,\,o^\prime}}}}
|
||||
{\withenv{\Gamma}{\trans{\inbr{\sigma,\,i,\,o}}{f (\bar{e})}{\inbr{\mbox{\textbf{leave}}\;\sigma^\prime\,\sigma,\,i^\prime,o^\prime}}}}
|
||||
\trule{\withenv{\Gamma}{\trans{\inbr{\primi{enter}{\sigma\,(\bar{a}@\bar{l})[\overline{a\gets\sembr{e}\sigma}]},\,i,\,o}}{S}{\inbr{\sigma^\prime,\,i^\prime,\,o^\prime}}}}
|
||||
{\withenv{\Gamma}{\trans{\inbr{\sigma,\,i,\,o}}{f (\bar{e})}{\inbr{\primi{leave}{\sigma^\prime\,\sigma},\,i^\prime,o^\prime}}}}
|
||||
\ruleno{Call$_{bs}$}
|
||||
\]
|
||||
|
||||
|
|
@ -146,7 +146,7 @@ affect the control stack, it gets threaded through all rules of operational sema
|
|||
Now we specify additional rules for the new instructions:
|
||||
|
||||
\[
|
||||
\trule{\withenv{P}{\trans{\inbr{cs,\,st,\,\inbr{\mbox{\textbf{enter}}\;\sigma\,(\bar{a}@\bar{l})\overline{[a\gets z]},\,i,\,o}}}{p}{c^\prime}}}
|
||||
\trule{\withenv{P}{\trans{\inbr{cs,\,st,\,\inbr{\primi{enter}{\sigma\,(\bar{a}@\bar{l})\overline{[a\gets z]}},\,i,\,o}}}{p}{c^\prime}}}
|
||||
{\withenv{P}{\trans{\inbr{cs,\,\bar{z}@st,\,\inbr{\sigma,\,i,\,o}}}{(\llang{BEGIN $\;\bar{a}\,\bar{l}$})p}{c^\prime}}}
|
||||
\ruleno{Begin$_{SM}$}
|
||||
\]
|
||||
|
|
@ -158,7 +158,7 @@ Now we specify additional rules for the new instructions:
|
|||
\]
|
||||
|
||||
\[
|
||||
\trule{\withenv{P}{\trans{\inbr{cs,\,st,\,\inbr{\mbox{\textbf{leave}}\;\sigma\,\sigma^\prime,\,i,\,o}}}{p^\prime}{c^\prime}}}
|
||||
\trule{\withenv{P}{\trans{\inbr{cs,\,st,\,\inbr{\primi{leave}{\sigma\,\sigma^\prime},\,i,\,o}}}{p^\prime}{c^\prime}}}
|
||||
{\withenv{P}{\trans{\inbr{(p^\prime,\,\sigma^\prime)::cs,\,st,\,\inbr{\sigma,\,i,\,o}}}{\llang{END}p}{c^\prime}}}
|
||||
\ruleno{EndRet$_{SM}$}
|
||||
\]
|
||||
|
|
|
|||
87
doc/06.tex
87
doc/06.tex
|
|
@ -30,29 +30,41 @@ We extend the configuration, used in the semantic description for statements, wi
|
|||
|
||||
This component will correspond to an optional return value for function/procedure calls (either integer value $n$ or ``$\hbox{---}$'', nothing).
|
||||
|
||||
The rules inself are summarized in the Fig.~\ref{bs_expr}. Note the use of double environment for evaluating the body of function in the rule
|
||||
We introduce two primitives to make the semantic description shorter:
|
||||
|
||||
\[
|
||||
\begin{array}{c}
|
||||
\primi{val}{\inbr{s,\,i,\,o,\,v}}=v\\
|
||||
\primi{ret}{\inbr{s,\,i,\,o,\,\_}\,v}=\inbr{s,\,i,\,o,\,v}
|
||||
\end{array}
|
||||
\]
|
||||
|
||||
|
||||
The rules themselves are summarized in the Fig.~\ref{bs_expr}. Note the use of double environment for evaluating the body of a function in the rule
|
||||
\rulename{Call}; note also, that now semantics of expressions and statements are mutually recursive.
|
||||
|
||||
\setarrow{\xRightarrow}
|
||||
\setsubarrow{_{\mathscr E}}
|
||||
|
||||
\begin{figure}
|
||||
\[\withenv{\Phi}{\trans{\inbr{\sigma, i, o, \hbox{---}}}{n}{\inbr{\sigma, i, o, n}}} \ruleno{Const} \]
|
||||
\[\withenv{\Phi}{\trans{\inbr{\sigma, i, o, \hbox{---}}}{x}{\inbr{\sigma, i, o, \sigma\;x}}} \ruleno{Var} \]
|
||||
\[\trule{\withenv{\Phi}{\trans{c}{A}{c^\prime=\inbr{\_,\, \_,\, \_,\, a}}},\;
|
||||
\withenv{\Phi}{\trans{c^\prime}{B}{\inbr{\sigma^{\prime\prime}, i^{\prime\prime}, o^{\prime\prime}, b}}}
|
||||
}
|
||||
{\withenv{\Phi}{\trans{c}{A\otimes B}{\inbr{\sigma^{\prime\prime}, i^{\prime\prime}, o^{\prime\prime}, a\oplus b}}}}
|
||||
\ruleno{Binop}
|
||||
\]
|
||||
\[\trule{\begin{array}{c}
|
||||
\withenv{\Phi}{\trans{c_{j-1}}{e_j}{c_j=\inbr{\sigma_j,\,i_j,\,o_j,\,v_j}}},\\
|
||||
\Phi\;f = \llang{fun $\;f\;$ ($\overline{a}$) local $\;\overline{l}\;$ \{$s$\}},\\
|
||||
{\setsubarrow{}
|
||||
\withenv{\llang{skip},\,\Phi}{\trans{\inbr{\mbox{\textbf{enter}}\;\sigma_k\; (\overline{a}@\overline{l})\; [\overline{a_j\gets v_j}],i_k,o_k,\hbox{---}}}{s}{\inbr{\sigma^\prime, i^\prime, o^\prime, n}}}}
|
||||
\arraycolsep=10pt
|
||||
\[\withenv{\Phi}{\trans{\inbr{\sigma,\, i,\, o,\, \_}}{n}{\inbr{\sigma,\, i,\, o,\, n}}} \ruleno{Const} \]\vskip2mm
|
||||
\[\withenv{\Phi}{\trans{\inbr{\sigma,\, i,\, o,\, \_}}{x}{\inbr{\sigma,\, i,\, o,\, \sigma\;x}}} \ruleno{Var} \]\vskip2mm
|
||||
\[\trule{\begin{array}{cc}
|
||||
\withenv{\Phi}{\trans{c}{A}{c^\prime}} & \withenv{\Phi}{\trans{c^\prime}{B}{c^{\prime\prime}}}
|
||||
\end{array}
|
||||
}
|
||||
{\withenv{\Phi}{\trans{c_0=\inbr{\sigma_0,\,\_,\,\_,\,\_}}{f (\overline{e_k})}{\inbr{\mbox{\textbf{leave}}\;\sigma^\prime\;\sigma_0, i^\prime, o^\prime, n}}}}
|
||||
{\withenv{\Phi}{\trans{c}{A\otimes B}{\primi{ret}{(\primi{val}{c^\prime}\oplus\primi{val}{c^{\prime\prime}})}}}}
|
||||
\ruleno{Binop}
|
||||
\]\vskip2mm
|
||||
\[\trule{\begin{array}{c}
|
||||
\withenv{\Phi}{\trans{c_{j-1}}{e_j}{c_j=\inbr{\sigma_j,\,i_j,\,o_j,\,v_j}}}\\
|
||||
\Phi\;f = \llang{fun $\;f\;$ ($\overline{a}$) local $\;\overline{l}\;$ \{$s$\}}\\
|
||||
{\setsubarrow{}
|
||||
\withenv{\llang{skip},\,\Phi}{\trans{\inbr{\primi{enter}{\sigma_k\; (\overline{a}@\overline{l})\; [\overline{a_j\gets v_j}]},\,i_k,o_k,\hbox{---}}}{s}{\inbr{\sigma^\prime, i^\prime, o^\prime, n}}}}
|
||||
\end{array}
|
||||
}
|
||||
{\withenv{\Phi}{\trans{c_0=\inbr{\sigma_0,\,\_,\,\_,\,\_}}{f (\overline{e_k})}{\inbr{\primi{leave}{\sigma^\prime\;\sigma_0}, i^\prime, o^\prime, n}}}}
|
||||
\ruleno{Call}
|
||||
\]
|
||||
\caption{Big-step Operational Semantics for Expressions}
|
||||
|
|
@ -96,14 +108,16 @@ The rules themselves are shown on Fig.~\ref{bs_cps}. Note, the rule for the call
|
|||
{\withenv{K,\,\Phi}{\trans{c}{\llang{skip}}{c^\prime}}}
|
||||
\ruleno{Skip}
|
||||
\]
|
||||
\[\trule{{\setsubarrow{_{\mathscr E}}\withenv{\Phi}{\trans{c}{e}{\inbr{\sigma,\,i,\,o,\,n}}}};\;
|
||||
\withenv{\llang{skip},\,\Phi}{\trans{\inbr{\sigma[x\gets n],\,i,\,o,\,\hbox{---}}}{K}{c^\prime}}
|
||||
}
|
||||
\[\trule{
|
||||
\begin{array}{cc}
|
||||
{\setsubarrow{_{\mathscr E}}\withenv{\Phi}{\trans{c}{e}{\inbr{\sigma,\,i,\,o,\,n}}}} & \withenv{\llang{skip},\,\Phi}{\trans{\inbr{\sigma[x\gets n],\,i,\,o,\,\hbox{---}}}{K}{c^\prime}}
|
||||
\end{array}}
|
||||
{\withenv{K,\,\Phi}{\trans{c}{\llang{$x\,$:=$\,e$}}{c^\prime}}}
|
||||
\ruleno{Assign}
|
||||
\]
|
||||
\[\trule{{\setsubarrow{_{\mathscr E}}\withenv{\Phi}{\trans{c}{e}{\inbr{\sigma,\,i,\,o,\,n}}}};\;
|
||||
\withenv{\llang{skip},\,\Phi}{\trans{\inbr{\sigma,\,i,\,o@[n],\,\hbox{---}}}{K}{c^\prime}}
|
||||
\[\trule{\begin{array}{cc}
|
||||
{\setsubarrow{_{\mathscr E}}\withenv{\Phi}{\trans{c}{e}{\inbr{\sigma,\,i,\,o,\,n}}}} & \withenv{\llang{skip},\,\Phi}{\trans{\inbr{\sigma,\,i,\,o@[n],\,\hbox{---}}}{K}{c^\prime}}
|
||||
\end{array}
|
||||
}
|
||||
{\withenv{K,\,\Phi}{\trans{c}{\llang{write ($e$)}}{c^\prime}}}
|
||||
\ruleno{Write}
|
||||
|
|
@ -120,41 +134,44 @@ The rules themselves are shown on Fig.~\ref{bs_cps}. Note, the rule for the call
|
|||
\ruleno{Seq}
|
||||
\]
|
||||
|
||||
\[\crule{{\setsubarrow{_{\mathscr E}} \withenv{\Phi}{\trans{c}{e}{\inbr{\sigma,\,i,\,o,\,n}}}};\;
|
||||
\withenv{K,\,\Phi}{\trans{\inbr{\sigma,\,i,\,o,\,\hbox{---}}}{\llang{$s_1$}}{c^\prime}}}
|
||||
\[\trule{\begin{array}{cc}
|
||||
{\setsubarrow{_{\mathscr E}}\withenv{\Phi}{\trans{c}{e}{\inbr{\sigma,\,i,\,o,\,n}}}} & \withenv{K,\,\Phi}{\trans{\inbr{\sigma,\,i,\,o,\,\hbox{---}}}{\llang{$s_1$}}{c^\prime}}\\
|
||||
n\ne 0 &
|
||||
\end{array}
|
||||
}
|
||||
{\withenv{K,\,\Phi}{\trans{c}{\llang{if $\;e\;$ then $\;s_1\;$ else $\;s_2$}}{c^\prime}}}
|
||||
{n\ne 0}
|
||||
\ruleno{IfTrue}
|
||||
\]
|
||||
|
||||
\[\crule{{\setsubarrow{_{\mathscr E}} \withenv{\Phi}{\trans{c}{e}{\inbr{\sigma,\,i,\,o,\,n}}}};\;
|
||||
\withenv{K,\,\Phi}{\trans{\inbr{\sigma,\,i,\,o,\,\hbox{---}}}{\llang{$s_2$}}{c^\prime}}}
|
||||
\[\trule{\begin{array}{cc}
|
||||
{\setsubarrow{_{\mathscr E}} \withenv{\Phi}{\trans{c}{e}{\inbr{\sigma,\,i,\,o,\,0}}}} & \withenv{K,\,\Phi}{\trans{\inbr{\sigma,\,i,\,o,\,\hbox{---}}}{\llang{$s_2$}}{c^\prime}}
|
||||
\end{array}
|
||||
}
|
||||
{\withenv{K,\,\Phi}{\trans{c}{\llang{if $\;e\;$ then $\;s_1\;$ else $\;s_2$}}{c^\prime}}}
|
||||
{n= 0}
|
||||
\ruleno{IfFalse}
|
||||
\]
|
||||
|
||||
\[\crule{\begin{array}{c}
|
||||
{\setsubarrow{_{\mathscr E}} \withenv{\Phi}{\trans{c}{e}{\inbr{\sigma,\,i,\,o,\,n}}}}\\
|
||||
\withenv{\llang{while $\;e\;$ do $\;s$}\diamond K,\,\Phi}{\trans{\inbr{\sigma,\,i,\,o,\,\hbox{---}}}{\llang{$s$}}{c^\prime}}
|
||||
\[\trule{\begin{array}{cc}
|
||||
{\setsubarrow{_{\mathscr E}} \withenv{\Phi}{\trans{c}{e}{\inbr{\sigma,\,i,\,o,\,n}}}} &
|
||||
\withenv{\llang{while $\;e\;$ do $\;s$}\diamond K,\,\Phi}{\trans{\inbr{\sigma,\,i,\,o,\,\hbox{---}}}{\llang{$s$}}{c^\prime}}\\
|
||||
n \ne 0 &
|
||||
\end{array}}
|
||||
{\withenv{K,\,\Phi}{\trans{c}{\llang{while $\;e\;$ do $\;s$}}{c^\prime}}}
|
||||
{n\ne 0}
|
||||
\ruleno{WhileTrue}
|
||||
\]
|
||||
|
||||
\[\crule{{\setsubarrow{_{\mathscr E}} \withenv{\Phi}{\trans{c}{e}{\inbr{\sigma,\,i,\,o,\,n}}}};\;
|
||||
\withenv{\llang{skip},\,\Phi}{\trans{\inbr{\sigma,\,i,\,o,\,\hbox{---}}}{K}{c^\prime}}}
|
||||
\[\trule{\begin{array}{cc}
|
||||
{\setsubarrow{_{\mathscr E}} \withenv{\Phi}{\trans{c}{e}{\inbr{\sigma,\,i,\,o,\,0}}}} & \withenv{\llang{skip},\,\Phi}{\trans{\inbr{\sigma,\,i,\,o,\,\hbox{---}}}{K}{c^\prime}}
|
||||
\end{array}}
|
||||
{\withenv{K,\,\Phi}{\trans{c}{\llang{while $\;e\;$ do $\;s$}}{c^\prime}}}
|
||||
{n = 0}
|
||||
\ruleno{WhileFalse}
|
||||
\]
|
||||
|
||||
\[\trule{\begin{array}{c}
|
||||
{\setsubarrow{_{\mathscr E}}\withenv{\Phi}{\trans{c_{j-1}}{e_j}{c_j=\inbr{\sigma_j,\,i_j,\,o_j,\,v_j}}}}\\
|
||||
\Phi\;f = \llang{fun $\;f\;$ ($\overline{a}$) local $\;\overline{l}\;$ \{$s$\}} \\
|
||||
\withenv{\llang{skip},\,\Phi}{\trans{\inbr{\mbox{\textbf{enter}}\;\sigma_k\; (\overline{a}@\overline{l})\; [\overline{a_j\gets v_j}],i_k,o_k,\hbox{---}}}{s}{\inbr{\sigma^\prime, i^\prime, o^\prime, \hbox{---}}}}\\
|
||||
\withenv{\llang{skip},\,\Phi}{\trans{\inbr{\mbox{\textbf{leave}}\;\sigma^\prime\;\sigma_0, i^\prime, o^\prime, \hbox{---}}}{K}{\inbr{\sigma^{\prime\prime}, i^{\prime\prime}, o^{\prime\prime}, n}}}
|
||||
\withenv{\llang{skip},\,\Phi}{\trans{\inbr{\primi{enter}{\sigma_k\; (\overline{a}@\overline{l})\; [\overline{a_j\gets v_j}]},i_k,o_k,\hbox{---}}}{s}{\inbr{\sigma^\prime, i^\prime, o^\prime, \hbox{---}}}}\\
|
||||
\withenv{\llang{skip},\,\Phi}{\trans{\inbr{\primi{leave}{\sigma^\prime\;\sigma_0}, i^\prime, o^\prime, \hbox{---}}}{K}{\inbr{\sigma^{\prime\prime}, i^{\prime\prime}, o^{\prime\prime}, n}}}
|
||||
\end{array}}
|
||||
{\withenv{K,\,\Phi}{\trans{c_0=\inbr{\sigma_0,\,\_,\,\_,\,\_}}{f (\overline{e_k})}{\inbr{\sigma^{\prime\prime}, i^{\prime\prime}, o^{\prime\prime}, n}}}}
|
||||
\ruleno{Call}
|
||||
|
|
|
|||
107
doc/07.tex
107
doc/07.tex
|
|
@ -11,7 +11,7 @@ For an array $(n, f)$ we assume $\dom{f}=[0\,..\,n-1]$. An element selection fun
|
|||
|
||||
\[
|
||||
\begin{array}{c}
|
||||
[\bullet] : \mathscr A (\mathscr E) \to \mathbb N \to \mathscr E\\[2mm]
|
||||
\bullet[\bullet] : \mathscr A (\mathscr E) \to \mathbb N \to \mathscr E\\[2mm]
|
||||
(n, f) [i] = \left\{
|
||||
\begin{array}{rcl}
|
||||
f\;i &, & i < n\\
|
||||
|
|
@ -21,22 +21,6 @@ For an array $(n, f)$ we assume $\dom{f}=[0\,..\,n-1]$. An element selection fun
|
|||
\end{array}
|
||||
\]
|
||||
|
||||
\begin{comment}
|
||||
A set of (ASCII) characters:
|
||||
|
||||
\[
|
||||
\mathscr C = [0\,..\,255]
|
||||
\]
|
||||
|
||||
A string is an array of characters:
|
||||
|
||||
\[
|
||||
\mathscr S = \mathscr A (\mathscr C)
|
||||
\]
|
||||
|
||||
Adding strings and arrays to the language changes the set of values the programs operate on:
|
||||
\end{comment}
|
||||
|
||||
We represent arrays by \emph{references}. Thus, we introduce a (linearly) ordered set of locations
|
||||
|
||||
\[
|
||||
|
|
@ -57,12 +41,16 @@ unambiguously discriminate between the shapes of each value. To access arrays, w
|
|||
\mathscr M = \mathscr L \to \mathscr A\,(\mathscr V)
|
||||
\]
|
||||
|
||||
We now add two more components to the states: a memory function $\mu$ and the first free memory location $l_m$.
|
||||
We now add two more components to the configurations: a memory function $\mu$ and the first free memory location $l_m$, and
|
||||
define the following primitive:
|
||||
|
||||
%Enriching the value set extends the definitions of state (which now has to map variable names to values) and
|
||||
%stack (similarly), but does not affect the definition of input/output streams, read and write primitives, etc.
|
||||
\[
|
||||
\primi{mem}{\inbr{s,\,\mu,\,l_m,\,i,\,o,\,v}}=\mu
|
||||
\]
|
||||
|
||||
\subsection{Adding arrays/strings on expression level}
|
||||
which gives a memory function from a configuration.
|
||||
|
||||
\subsection{Adding arrays on expression level}
|
||||
|
||||
On expression level, abstractly/concretely:
|
||||
|
||||
|
|
@ -74,19 +62,18 @@ On expression level, abstractly/concretely:
|
|||
\end{array}
|
||||
\]
|
||||
|
||||
In addition, in a concrete syntax we supply two special forms for strings: \llang{'$x$'} as a denotation for integer code of ASCII symbol
|
||||
$x$, and \llang{"..."}~--- a string constant.
|
||||
%In addition, in a concrete syntax we supply two special forms for strings: \llang{'$x$'} as a denotation for integer code of ASCII symbol
|
||||
%$x$, and \llang{"..."}~--- a string constant.
|
||||
|
||||
The semantics of enriched expressions is modified as follows. First, we add two additional premises to the rule for binary operators:
|
||||
|
||||
\setsubarrow{_{\mathscr E}}
|
||||
\[\trule{\begin{array}{c}
|
||||
\withenv{\Phi}{\trans{c}{A}{c^\prime=\inbr{\_,\, \_,\, \_,\, a}}}\\
|
||||
\withenv{\Phi}{\trans{c^\prime}{B}{\inbr{\sigma^{\prime\prime}, i^{\prime\prime}, o^{\prime\prime}, b}}}\\
|
||||
a\in\mathbb Z,\,b\in\mathbb Z
|
||||
\[\trule{\begin{array}{ccc}
|
||||
\withenv{\Phi}{\trans{c}{A}{c^\prime}} &\phantom{XXXXX}& \withenv{\Phi}{\trans{c^\prime}{B}{c^{\prime\prime}}}\\
|
||||
\primi{val}{c^\prime}\in\mathbb Z & & \primi{val}{c^{\prime\prime}}\in\mathbb Z
|
||||
\end{array}
|
||||
}
|
||||
{\withenv{\Phi}{\trans{c}{A\otimes B}{\inbr{\sigma^{\prime\prime}, i^{\prime\prime}, o^{\prime\prime}, a\oplus b}}}}
|
||||
{\withenv{\Phi}{\trans{c}{A\otimes B}{\primi{ret}{c^{\prime\prime}\;(\primi{val}{c^\prime}\oplus \primi{val}{c^{\prime\prime}})}}}}
|
||||
\ruleno{Binop}
|
||||
\]
|
||||
|
||||
|
|
@ -94,31 +81,40 @@ These two premises ensure that both operand expressions are evaluated into integ
|
|||
kinds of expressions (see Figure~\ref{array_expressions}).
|
||||
|
||||
\begin{figure}
|
||||
\[\trule{\begin{array}{c}
|
||||
\withenv{\Phi}{\trans{c}{E}{c^\prime=\inbr{\_, \_, \_, l}}}\\
|
||||
\withenv{\Phi}{\trans{c^\prime}{J}{\inbr{s^{\prime\prime}=\inbr{\_,\, \_,\, \_,\, \mu,\,\_},\, i^{\prime\prime},\, o^{\prime\prime},\, j}}}\\
|
||||
l\in \mathscr L,\,(n,\,f)=\mu\,\;l\,j\in\mathbb N,\,j<n
|
||||
\[\trule{\begin{array}{ccc}
|
||||
\withenv{\Phi}{\trans{c}{e}{c^\prime}} &\phantom{XXXX} &\withenv{\Phi}{\trans{c^\prime}{j}{c^{\prime\prime}}}\\
|
||||
l=\primi{val}{c^\prime} & &j=\primi{val}{c^{\prime\prime}}\\
|
||||
l\in\mathscr L & &j\in\mathbb N\\
|
||||
(n,\,f)=\primi{mem}{l} & &j<n
|
||||
\end{array}}
|
||||
{\withenv{\Phi}{\trans{c}{E\,\mathtt{[}J\mathtt{]}}{\inbr{s^{\prime\prime}, i^{\prime\prime}, o^{\prime\prime}, f\,j}}}}
|
||||
{\withenv{\Phi}{\trans{c}{e\,\mathtt{[}j\mathtt{]}}{\primi{ret}{c^{\prime\prime}(f\;j)}}}}
|
||||
\ruleno{ArrayElement}
|
||||
\]
|
||||
\[\trule{\withenv{\Phi}{\trans{c_j}{e_j}{c_{j+1}=\inbr{\inbr{\sigma_g^{j+1},\,S^{j+1},\,\sigma_l^{j+1},\,\mu^{j+1},\,l_{m_{j+1}}}, i_{j+1}, o_{j+1}, a_j}}},\,j\in [0..k]}
|
||||
{\withenv{\Phi}{\trans{c_0}{\mathtt{[}e_0, e_1,...,e_k\mathtt{]}}{\inbr{\inbr{\sigma_g^{j+1},\,S^{j+1},\,\sigma_l^{j+1},\,\mu^{j+1}[l_{m_{k+1}}\gets (k,\,\lambda i\,.\,a_i)],\, l_{m_{k+1}+1}}, i_{k+1}, o_{k+1}, l_{m_{k+1}}}}}}
|
||||
\ruleno{ArrayConstructor}
|
||||
\]
|
||||
\vskip5mm
|
||||
\[\trule{\begin{array}{c}
|
||||
\withenv{\Phi}{\trans{c}{E}{\inbr{s^{\prime\prime}=\inbr{\_,\,\_,\,\_,\,\mu,\,\_}, i^{\prime\prime}, o^{\prime\prime}, l}}}\\
|
||||
l\in\mathscr L,\,(n,\,f)=\mu\;l
|
||||
\withenv{\Phi}{\trans{c_j}{e_j}{c_{j+1}}},\,j\in [0..k]\\
|
||||
\inbr{s,\,\mu,\,l_m,\,i,\,o,\,\_}=c_{k+1}
|
||||
\end{array}
|
||||
}
|
||||
{\withenv{\Phi}{\trans{c_0}{\mathtt{[}e_0, e_1,...,e_k\mathtt{]}}{\inbr{s,\,\mu\,[l_m\gets(k+1,\,\lambda n.\primi{val}{c_n})],\,l_{m+1},\,i,\,o,\,l_m}}}}
|
||||
\ruleno{Array}
|
||||
\]
|
||||
\vskip5mm
|
||||
\[\trule{\begin{array}{c}
|
||||
\withenv{\Phi}{\trans{c}{e}{c^\prime}}\\
|
||||
l=\primi{val}{c^\prime}\\
|
||||
l\in\mathscr L\\
|
||||
(n,\,f)=(\primi{mem}{c^\prime})\;l
|
||||
\end{array}
|
||||
}
|
||||
{\withenv{\Phi}{\trans{c}{E\mathtt{.length}}{\inbr{s^{\prime\prime}, i^{\prime\prime}, o^{\prime\prime}, n}}}}
|
||||
{\withenv{\Phi}{\trans{c}{e\mathtt{.length}}{\primi{return}{c^\prime\;n}}}}
|
||||
\ruleno{ArrayLength}
|
||||
\]
|
||||
\caption{Big-step Operational Semantics for Array Expressions}
|
||||
\label{array_expressions}
|
||||
\end{figure}
|
||||
|
||||
\subsection{Adding arrays/strings on statement level}
|
||||
\subsection{Adding arrays on statement level}
|
||||
|
||||
On statement level, we add the single construct:
|
||||
|
||||
|
|
@ -127,17 +123,30 @@ On statement level, we add the single construct:
|
|||
\]
|
||||
|
||||
This construct is interpreted as an assignment to an element of an array. The semantics of this construct is described by the following rule:
|
||||
|
||||
\[
|
||||
\trule{\setsubarrow{_{\mathscr E}}
|
||||
\begin{array}{c}
|
||||
\withenv{\Phi}{\trans{c}{E}{c^\prime=\inbr{\_,\_,\_, (n,\,f)}}}\\
|
||||
\withenv{\Phi}{\trans{c^\prime}{J}{c^{\prime\prime}=\inbr{\_,\_,\_,j}}}\\
|
||||
\withenv{\Phi}{\trans{c^{\prime\prime}}{F}{c^{\prime\prime\prime}=\inbr{s^{\prime\prime},i^{\prime\prime},o^{\prime\prime},y}}}\\
|
||||
j\in\mathbb N,\,j<n\\
|
||||
\setsubarrow{}\withenv{\llang{skip},\,\Phi}{\trans{\inbr{\mathtt{update}(s^{\prime\prime}, E, (n,\,f [j\gets y])),i^{\prime\prime},o^{\prime\prime},\hbox{---}}}{K}{\widetilde{c}}}
|
||||
\begin{array}{ccccc}
|
||||
\withenv{\Phi}{\trans{c}{e}{c^\prime}} & \phantom{XXX} & \withenv{\Phi}{\trans{c^\prime}{j}{c^{\prime\prime}}} & \phantom{XXX} & \withenv{\Phi}{\trans{c^{\prime\prime}}{g}{\inbr{s,\mu,l_m,i,o,v}}}\\
|
||||
l=\primi{val}{c^\prime} & & i=\primi{val}{c^{\prime\prime}} & & \\
|
||||
l\in\mathscr L & & i\in\mathbb N & & \\[3mm]
|
||||
\multicolumn{5}{c}{(n,\,f)=\mu\;l}\\
|
||||
\multicolumn{5}{c}{i<n}\\
|
||||
\multicolumn{5}{c}{\setsubarrow{}\withenv{\llang{skip},\,\Phi}{\trans{\inbr{s,\,\mu\,[l\gets (n,\,f\,[i\gets x])],\,l_m,\,i,\,o,\,\hbox{---}}}{K}{\widetilde{c}}}}
|
||||
\end{array}
|
||||
}
|
||||
{\setsubarrow{}\withenv{K,\,\Phi}{\trans{c}{E\mathtt{[}J\mathtt{]}\llang{:=}F}{\widetilde{c}}}}
|
||||
{\setsubarrow{}\withenv{K,\,\Phi}{\trans{c}{e\mathtt{[}j\mathtt{]}\llang{:=}g}{\widetilde{c}}}}
|
||||
\ruleno{ArrayAssign}
|
||||
\]
|
||||
|
||||
\subsection{Strings}
|
||||
|
||||
With arrays in our hands, we can easily add strings as arrays of characters. In fact, on the source language the strings can be
|
||||
introduced as a syntactic extension:
|
||||
|
||||
\begin{enumerate}
|
||||
\item we add a character constants \llang{'c'} as a shortcut for their integer codes;
|
||||
\item we add a string literals \llang{"abcd..."} as a shortcut for arrays \llang{['a', 'b', 'c', 'd', ...]}.
|
||||
\end{enumerate}
|
||||
|
||||
Nothing else has to be done~--- now we have mutable reference-representable strings.
|
||||
|
||||
|
|
|
|||
|
|
@ -45,7 +45,7 @@
|
|||
\newcommand{\trule}[2]{\frac{#1}{#2}}
|
||||
\newcommand{\crule}[3]{\frac{#1}{#2},\;{#3}}
|
||||
\newcommand{\withenv}[2]{{#1}\vdash{#2}}
|
||||
\newcommand{\trans}[3]{{#1}\transarrow{\padding#2\padding}\subarrow{#3}}
|
||||
\newcommand{\trans}[3]{{#1}\transarrow{\padding{\textstyle #2}\padding}\subarrow{#3}}
|
||||
\newcommand{\ctrans}[4]{{#1}\transarrow{\padding#2\padding}\subarrow{#3},\;{#4}}
|
||||
\newcommand{\llang}[1]{\mbox{\lstinline[mathescape]|#1|}}
|
||||
\newcommand{\pair}[2]{\inbr{{#1}\mid{#2}}}
|
||||
|
|
@ -70,6 +70,7 @@
|
|||
\newcommand{\meta}[1]{{\mathcal{#1}}}
|
||||
\renewcommand{\emptyset}{\varnothing}
|
||||
\newcommand{\dom}[1]{\mathtt{dom}\;{#1}}
|
||||
\newcommand{\primi}[2]{\mathbf{#1}\;{#2}}
|
||||
|
||||
\definecolor{light-gray}{gray}{0.90}
|
||||
\newcommand{\graybox}[1]{\colorbox{light-gray}{#1}}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue