diff --git a/doc/04.tex b/doc/04.tex index bcfb5cb30..d7563e0ab 100644 --- a/doc/04.tex +++ b/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} diff --git a/doc/05.tex b/doc/05.tex index 25aa943db..8a0a1b650 100644 --- a/doc/05.tex +++ b/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}$} \] diff --git a/doc/06.tex b/doc/06.tex index 6521a34b3..60cad34ef 100644 --- a/doc/06.tex +++ b/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} diff --git a/doc/07.tex b/doc/07.tex index 665ec2503..0ef0f8cc5 100644 --- a/doc/07.tex +++ b/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