1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
|
% vim:set spelllang=nl:
\section{Smurf in structurele operationele semantiek}
\label{sec:sos}
We willen ook 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. Wij hadden een voorkeur om natuurlijke semantiek te
gebruiken omdat we hier meer bekend mee zijn. We wilden echter ook graag laten
zien hoe het eruit zou zien als je structurele operationele semantiek zou
gebruiken.
Bij het definiëren van de structurele operationele semantiek van Smurf zullen
we de verzameling van transities als een relatie $\Rightarrow$ tussen
$\Pgm\times\Input\times\Output\times\State$ en $\Gamma$ beschouwen, waarbij
$\Gamma$ óf $\Pgm\times\Input\times\Output\times\State$ óf
$\Input\times\Output\times\State$ is. Dit schrijven we als
$$
\sostransgamma{\stm:\pgm}{\ip}{\op}{\st}{\gamma}
\qquad\text{met $\gamma \in \{(\pgm',\ip',\op',\st'), (\ip', \op',\st')\}$}.
$$
De reden dat rechts van de pijl $\pgm'$ gebruikt wordt (en niet gewoon $\pgm$)
is dat in het geval van $\StmExec$ de rest van het programma niet zal worden
uitgevoerd. In de meeste gevallen zal $\pgm=\pgm'$ echter wel gelden.
Het is mogelijk om in de structurele operationele semantiek, zoals bij de
natuurlijke semantiek, compositie in te bouwen in iedere regel en een
$\lambda$-regel toe te voegen. In dit geval kiezen we er echter voor om gebruik
te maken van een aparte regel voor compositie. We blijven hiermee in zekere zin
dichter bij de specificatie, omdat we regels per commando kunnen beschrijven in
plaats van voor een heel programma.
De compositieregel is dan als volgt:
$$
\begin{prooftree}
\sostranseind
{\stm}{\ip}{\op}{(\stk, \str)}
{\ip'}{\op'}{(\stk', \str')}
\justifies
\sostrans
{\stm:\pgm}{\ip}{\op}{(\stk,\str)}
{\pgm}{\ip'}{\op'}{(\stk',\str')}
\using{\rcompeensos}
\end{prooftree}
$$
We geven twee voorbeelden van regels in de structurele operationele semantiek.
Het doel is hier niet om een precieze beschrijving van de semantiek te geven
zoals we dat in \autoref{sec:rules} voor natuurlijke semantiek hebben gedaan,
maar enkel om aan te geven dat de twee in het geval van Smurf erg op elkaar
lijken.
De regel voor $\StmTail$ zou in de structurele operationele semantiek als volgt
zijn:
$$
\sostranseind
{\StmTail}{\ip}{\op}{(\stk,\str)}
{\ip}{\op}{(\push{s}{\stk'}, \str)}
\enspace\rtailsos
\quad\text{met $\pop{\stk} = (c~s,\stk')$.}
$$
Afgezien van de compositie, die bij de natuurlijke semantiek in iedere regel is
ingebouwd, verschilt dit niet erg van $\rtailns$ in \autoref{sec:rules:tail}.
Dit geldt voor bijna alle andere commando's net zo. Een apart geval is
$\StmExec$, omdat we hier de compositieregel niet kunnen gebruiken. Wat na het
$\StmExec$-commando volgt wordt immers niet uitgevoerd. We definiëren deze
regel als volgt:
$$
\sostrans
{\StmExec:\pgm}{\ip}{\op}{(\stk,\str)}
{\pgm'}{\ip'}{\op'}{(\stk',\str')}
\enspace\rexecsos
\quad\text{met $\pop{\stk} = ( \pgm', \stk'')$.}
$$
Hier wordt gebruik gemaakt van een ander soort transitie, waarbij een programma
aan de rechterkant voorkomt. Hierdoor is $\rexecsos$ niet te gebruiken als
premisse voor $\rcompeensos$, wat precies is wat we wilden.
|
