blob: cd64ab244498e574ee39629626d46252e2b58d78 (
plain) (
blame)
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
|
% vim: set spelllang=nl:
\subsection{Transities}
\label{sec:def:trans}
We hebben ervoor gekozen de semantiek van Smurf in natuurlijke semantiek te
definiëren. In principe hadden we er ook voor kunnen kiezen om structurele
operationele semantiek te gebruiken. In het geval van Smurf komt dit ongeveer
op hetzelfde neer. Hoe regels voor Smurf gedefinieerd zouden kunnen worden in
structurele operationele semantiek wordt toegelicht in \autoref{sec:sos}.
Bij het definiëren van de natuurlijke semantiek van Smurf zullen we de
verzameling van transities als een relatie $\to$ tussen
$\Pgm\times\Input\times\State$ en $\Input\times\Output\times\State$ beschouwen.
Dit schrijven we als
$$\trans{\pgm}{\ip}{\st}{\ip'}{\op}{\st'}$$
en lezen we als
\begin{quote}
``het programma $\pgm$ zal in toestand $\st$ gegeven input $\ip$ leiden tot
toestand $\st'$, met output $\op$ waarbij $\ip'$ gelijk is aan $\ip$ zonder
de geconsumeerde input.''
\end{quote}
We hebben het hele programma $\pgm$ nodig voor de pijl, omdat één commando
($\StmExec$) eventuele verdere statements `weggooit'. %todo ander woord
Verder gebruiken we $\Input$ voor $\StmInput$ en hebben we natuurlijk de
$\State$ nodig voor ieder statement: ieder statement verandert de stack, en
sommige statements veranderen bovendien de variable store.
|
