% 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.