From 273ea318d8295c427c843ff1dfbf80da192b5b91 Mon Sep 17 00:00:00 2001 From: Dmitry Boulytchev Date: Thu, 6 Dec 2018 21:36:23 +0300 Subject: [PATCH] Lectures --- doc/02.tex | 6 +++++- doc/04.tex | 26 +++++++++++++------------- doc/05.tex | 11 ++++++++--- doc/07.tex | 33 ++++++++++++++++++--------------- 4 files changed, 44 insertions(+), 32 deletions(-) diff --git a/doc/02.tex b/doc/02.tex index 67140fa41..078b52665 100644 --- a/doc/02.tex +++ b/doc/02.tex @@ -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} diff --git a/doc/04.tex b/doc/04.tex index d7563e0ab..e05b3a0f0 100644 --- a/doc/04.tex +++ b/doc/04.tex @@ -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} diff --git a/doc/05.tex b/doc/05.tex index 8a0a1b650..850f48b81 100644 --- a/doc/05.tex +++ b/doc/05.tex @@ -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$\}}$. diff --git a/doc/07.tex b/doc/07.tex index 0ef0f8cc5..b6d91a9d7 100644 --- a/doc/07.tex +++ b/doc/07.tex @@ -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