blob: 0ff04e5f62e2c84f4b5611fa06942e3e88fcae07 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
% vim: set spelllang=nl:
\subsection{Transities}
\label{sec:def:trans}
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}{\i}{\st}{\i}{\o}{\st}$$
en lezen we als
\begin{quote}
``het programma $\pgm$ zal in toestand $\st$ gegeven input $\i$ leiden tot
toestand $\st$ met output $\o$ waarbij de input $\i$ niet geconsumeerd is.''
\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.
|
