diff options
| -rw-r--r-- | introcoms.tex | 1 | ||||
| -rw-r--r-- | smurf.sty | 6 | ||||
| -rw-r--r-- | sosexamp.tex | 54 | ||||
| -rw-r--r-- | werkstuk.tex | 1 |
4 files changed, 62 insertions, 0 deletions
diff --git a/introcoms.tex b/introcoms.tex index 0aa01b0..31f2de0 100644 --- a/introcoms.tex +++ b/introcoms.tex @@ -5,6 +5,7 @@ We zullen nu kort op informele wijze de verschillende commando's in Smurf beschrijven. We geven telkens de notatie in Smurf syntax en een leesbaarder alternatief dat we hieronder zullen gebruiken. Wanneer een commando iets met elementen op de stack doet, worden die elementen altijd verwijderd. +Merk op dat de commando's niet exact hetzelfde zijn als in de voorbeeldprogramma's en de taalspecificatie; wij gebruiken een leesbaardere variant op de taal zodat het overzichtelijker is om eigenschappen ervan te bespreken. Alle commando's betekenen nog steeds hetzelfde. \begin{description}[style=nextline,font=\normalfont] \item[\smurfinline{"..."} of $\StmPush~\texttt{...}$] @@ -58,6 +58,9 @@ % Transitions \def\trans#1#2#3#4#5#6{\left\langle#1,#2,#3\right\rangle\to\left(#4,#5,#6\right)} +\def\sostrans#1#2#3#4#5#6#7#8{\left\langle#1,#2,#3,#4\right\rangle\Rightarrow\left(#5,#6,#7,#8\right)} +\def\sostranseind#1#2#3#4#5#6#7{\left\langle#1,#2,#3,#4\right\rangle\Rightarrow\left(#5,#6,#7\right)} + % Rules \def\rule#1#2{[\mbox{#1}_{\mbox{\footnotesize{#2}}}]} \def\rlambdans{\rule{$\lambda$}{ns}} @@ -71,6 +74,9 @@ \def\rinputns{\rule{input}{ns}} \def\routputns{\rule{output}{ns}} \def\rexecns{\rule{exec}{ns}} +\def\rtailsos{\rule{tail}{sos}} +\def\rcompeensos{\rule{comp1}{sos}} +\def\rcomptweesos{\rule{comp2}{sos}} % Common names \def\stk{\mathit{stk}} diff --git a/sosexamp.tex b/sosexamp.tex new file mode 100644 index 0000000..d05ae3a --- /dev/null +++ b/sosexamp.tex @@ -0,0 +1,54 @@ +\subsection{Smurf in structurele operationele semantiek} +We willen ook nog graag laten zien hoe de definities van Smurf eruit zien als je de structurele operationele semantiek gebruikt. In principe maakt het voor de analyse van Smurf niet uit of je natuurlijke semantiek gebruikt of structurele operationele semantiek. Omdat natuurlijke semantiek en structurele operationele semantiek equivalent zijn wanneer de regels goed gedefineerd zijn. Wij hadden een voorkeur om natuurlijke semantiek te gebruiken omdat we hier meer bekend mee zijn. Echter willen we ook nog graag laten zien hoe het eruit zou zien als je structurele operationele semantiek zou gebruiken. + +We gebruiken hier in plaats van de lambda regel twee compositie regels om hiervan ook het verschil aan te geven. + +De twee composities regels zijn als volgt: +\medskip +\medskip +$$ +\begin{prooftree} + \sostrans + {\pgm1}{\ip}{\op}{(\stk, \str)} + {\pgm1'}{\ip'}{\op'}{(\stk', \str')} + \justifies + \sostrans + {\pgm1:\pgm2}{\ip}{\op}{(\stk,\str)} + {\pgm1':\pgm2}{\ip'}{\op'}{(\stk',\str')} + \using{\rcompeensos} + \qquad +\end{prooftree} +$$ +\medskip +\medskip +$$ +\begin{prooftree} + \sostranseind + {\pgm1}{\ip}{\op}{(\stk, \str)} + {\ip'}{\op'}{(\stk', \str')} + \justifies + \sostrans + {\pgm1:\pgm2}{\ip}{\op}{(\stk,\str)} + {\pgm2}{\ip'}{\op'}{(\stk',\str')} + \using{\rcomptweesos} + \qquad +\end{prooftree} +$$ + +\medskip +\medskip +\medskip + +De tailregel zal in de structurele operationele semantiek als volgt zijn: + +$$ +\begin{prooftree} + \axjustifies + \sostranseind + {\StmTail}{\ip}{\op}{(\stk,\str)} + {\ip}{\op}{(\push{s}{\stk'}, \str)} + \using{\rtailsos} + \qquad + \text{met $ \pop{\stk} = (c~s,\stk') $.} +\end{prooftree} +$$
\ No newline at end of file diff --git a/werkstuk.tex b/werkstuk.tex index 24a290f..8289f6f 100644 --- a/werkstuk.tex +++ b/werkstuk.tex @@ -48,6 +48,7 @@ \input{def} \input{rules} \input{analyse} +\input{sosexamp} \input{planning} \input{refs} |