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
|
% 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. Echter willen we ook nog 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\enspace
\parbox{36mm}{ $\gamma = (\pgm',\ip',\op',\st')$ of \\ $\gamma = (\ip', \op',\st' )$}}$$
De reden dat we hier spreken over $\pgm'$ is omdat de exec regel het programma dat je gaat uitvoeren verandert. In de meeste gevallen zal $\pgm$ = $\pgm'$ gelden maar dat hoeft dus niet.
\medskip
Je kunt de structurele operationele semantiek zoals bij de natuurlijke semantiek definiëren aan de hand van de $\lambda$-regel maar om juist het verschil aan te geven met als je gebruik maakt van compositieregels, hebben wij ervoor gekozen om de structurele operationele semantiek te definiëren gebruik makende van compositieregels.
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}
\qquad
\end{prooftree}
$$
\bigskip
De regel voor $\StmExec$ zou in de structurele operationele semantiek als volgt zijn:
$$
\begin{prooftree}
\axjustifies
\sostrans
{\StmExec:\pgm}{\ip}{\op}{(\stk,\str)}
{\pgm'}{\ip'}{\op'}{(\stk',\str')}
\using{\rexecsos}
\qquad
\text{met $\pop{\stk} = ( \pgm', \stk'')$.}
\end{prooftree}
$$
\bigskip
De regel voor $\StmTail$ zou 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}
$$
De andere regels zoals head en exec zullen we hier niet verder uitwerken omdat deze op een soortgelijke wijzen worden gemaakt.
|
