st/lama_byterun
1
0
Fork 0
mirror of https://github.com/ProgramSnail/Lama.git synced 2025-12-24 15:48:47 +00:00
Code Issues Projects Releases Packages Wiki Activity Actions

Lectures

Browse source
This commit is contained in:
Dmitry Boulytchev 2018-12-06 21:36:23 +03:00
parent 96a659c976
commit 273ea318d8
4 changed files with 44 additions and 32 deletions
Download patch file Download diff file Expand all files Collapse all files

6
doc/02.tex
View file

@ -53,10 +53,14 @@ With the relation ``$\Rightarrow$'' defined we can abbreviate the ``surface'' se
\begin{figure}[t]
\arraycolsep=10pt
\[\trans{\inbr{\sigma,\, \iota,\, o}}{\llang{x := $\;\;e$}}{\inbr{\sigma\,[x\gets\sembr{e}_{\mathscr E}\;\sigma],\, \iota,\, o}}\ruleno{Assign}\]
\[\trans{\inbr{\sigma,\, z\iota,\, o}}{\llang{read ($x$)}}{\inbr{\sigma\,[x\gets z],\, \iota,\, o}}\ruleno{Read}\]
\[\trans{\inbr{\sigma,\, \iota,\, o}}{\llang{write ($e$)}}{\inbr{\sigma,\, \iota,\, o(\sembr{e}_{\mathscr E}\;\sigma)}}\ruleno{Write}\]
\[\trule{\trans{c_1}{S_1}{c^\prime},\;\trans{c^\prime}{S_2}{c_2}}{\trans{c_1}{S_1\llang{;}S_2}{c_2}}\ruleno{Seq}\]
\[\trule{\begin{array}{cc}
\trans{c_1}{S_1}{c^\prime} & \trans{c^\prime}{S_2}{c_2}
\end{array}}
{\trans{c_1}{S_1\llang{;}S_2}{c_2}}\ruleno{Seq}\]
\caption{Big-step operational semantics for statements}
\label{bs_stmt}
\end{figure}

26
doc/04.tex
View file

@ -26,33 +26,33 @@ In the concrete syntax for the constructs we add the closing keywords ``\llang{i
\begin{figure}[t]
\arraycolsep=10pt
%\def\arraystretch{2.9}
\[\trans{c}{\llang{skip}}{c}\ruleno{Skip$_{bs}$}\]\vskip2mm
\[\trans{c}{\llang{skip}}{c}\ruleno{Skip}\]\vskip2mm
\[
\trule{\begin{array}{cc}
\sembr{e}\;s\ne 0 & \trans{c}{\mbox{$S_1$}}{c^\prime}
\sembr{e}\;\sigma\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}}
\ruleno{If-True$_{bs}$}
{\trans{c=\inbr{\sigma,\, \_,\, \_}}{\llang{if $\;e\;$ then $\;S_1\;$ else $\;S_2\;$}}{c^\prime}}
\ruleno{If-True}
\]\vskip2mm
\[
\trule{\begin{array}{cc}
\sembr{e}\;s=0 & \trans{c}{\mbox{$S_1$}}{c^\prime}
\sembr{e}\;\sigma=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}}
\ruleno{If-False$_{bs}$}
{\trans{c=\inbr{\sigma,\, \_,\, \_}}{\llang{if $\;e\;$ then $\;S_1\;$ else $\;S_2\;$}}{c^\prime}}
\ruleno{If-False}
\]\vskip3mm
\[
\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}}\\
{\sembr{e}\;\sigma\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}}}
\ruleno{While-True$_{bs}$}
{\trans{c=\inbr{\sigma,\, \_,\, \_}}{\llang{while $\;e\;$ do $\;S\;$}}{c^{\prime\prime}}}
\ruleno{While-True}
\]\vskip3mm
\[
\trule{\sembr{e}\;s=0}
{\trans{c=\inbr{s, \_, \_}}{\llang{while $\;e\;$ do $\;S\;$}}{c}}
\ruleno{While-False$_{bs}$}
\trule{\sembr{e}\;\sigma=0}
{\trans{c=\inbr{\sigma,\, \_,\, \_}}{\llang{while $\;e\;$ do $\;S\;$}}{c}}
\ruleno{While-False}
\]
\caption{Big-step operational semantics for control flow statements}
\label{bs_stmt_cf}

11
doc/05.tex
View file

@ -110,9 +110,14 @@ propagate this environment, adding $\withenv{\Gamma}{...}$ for each transition `
need now is to describe the rule for procedure calls:
\[
\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}$}
\arraycolsep=10pt
\trule{\begin{array}{cc}
\llang{fun $\;f\;$ ($\bar{a}$) local $\;\bar{l}\;$ \{$S$\}}=\Gamma\,f &
\withenv{\Gamma}{\trans{\inbr{\primi{enter}{\sigma\,(\bar{a}\bar{l})[\overline{a\gets\sembr{e}\sigma}]},\,\iota,\,o}}{S}{\inbr{\sigma^\prime,\,\iota^\prime,\,o^\prime}}}
\end{array}
}
{\withenv{\Gamma}{\trans{\inbr{\sigma,\,\iota,\,o}}{f (\bar{e})}{\inbr{\primi{leave}{\sigma^\prime\,\sigma},\,\iota^\prime,o^\prime}}}}
\ruleno{Call}
\]
where $\Gamma\,f = \llang{fun $\;f\;$ ($\bar{a}$) local $\;\bar{l}\;$ \{$S$\}}$.

33
doc/07.tex
View file

@ -68,9 +68,10 @@ On expression level, abstractly/concretely:
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}{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
\arraycolsep=10pt
\[\trule{\begin{array}{cc}
\withenv{\Phi}{\trans{c}{A}{c^\prime}} & \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}{\primi{ret}{c^{\prime\prime}\;(\primi{val}{c^\prime}\oplus \primi{val}{c^{\prime\prime}})}}}}
@ -81,11 +82,12 @@ 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}{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
\arraycolsep=10pt
\[\trule{\begin{array}{cc}
\withenv{\Phi}{\trans{c}{e}{c^\prime}} &\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{]}}{\primi{ret}{c^{\prime\prime}(f\;j)}}}}
\ruleno{ArrayElement}
@ -125,13 +127,14 @@ 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}{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}}}}
\arraycolsep=10pt
\begin{array}{ccc}
\withenv{\Phi}{\trans{c}{e}{c^\prime}} & \withenv{\Phi}{\trans{c^\prime}{j}{c^{\prime\prime}}} & \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{3}{c}{(n,\,f)=\mu\;l}\\
\multicolumn{3}{c}{i<n}\\
\multicolumn{3}{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{:=}g}{\widetilde{c}}}}