1 files changed, 21 insertions, 0 deletions
diff --git a/deftrans.tex b/deftrans.tex
new file mode 100644
index 0000000..0ff04e5
--- /dev/null
+++ b/deftrans.tex
@@ -0,0 +1,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.
+