summaryrefslogtreecommitdiff
path: root/deftrans.tex
diff options
context:
space:
mode:
Diffstat (limited to 'deftrans.tex')
-rw-r--r--deftrans.tex6
1 files changed, 3 insertions, 3 deletions
diff --git a/deftrans.tex b/deftrans.tex
index aae4239..67b5323 100644
--- a/deftrans.tex
+++ b/deftrans.tex
@@ -1,16 +1,16 @@
% vim: set spelllang=nl:
\subsection{Transities}
\label{sec:def:trans}
-
+We hebben gekozen om de semantiek van Smurf in natuurlijke semantiek te definiëren. In principe hadden we er ook voor kunnen kiezen om te gaan voor structurele operationele semantiek, echter denk wij dat we door het gebruik van natuurlijke semantiek meer kunnen in onze analyse.
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}$$
+$$\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 de input $\ip$ niet geconsumeerd is.''
+ toestand $\st'$, waarbij als de toestand niet verandert geldt $\st'$ = $\st$, met output $\op$ waarbij de input $\ip'$ met $\ip'$ = $\ip$ als $\ip$ niet geconsumeerd is.''
\end{quote}
We hebben het hele programma $\Pgm$ nodig voor de pijl, omdat één commando