From a1620cb8b84ad3ba941d93dae86080cf568e30ba Mon Sep 17 00:00:00 2001 From: Evi Date: Fri, 10 Jun 2016 12:24:06 +0200 Subject: meer analyse --- sosexamp.tex | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) (limited to 'sosexamp.tex') diff --git a/sosexamp.tex b/sosexamp.tex index e3926e8..45c8a2e 100644 --- a/sosexamp.tex +++ b/sosexamp.tex @@ -10,15 +10,13 @@ eruit zou zien als je structurele operationele semantiek zou gebruiken. Bij het definiëren van de structurele operationele semantiek van Smurf zullen we de verzameling van transities als een relatie $\Rightarrow$ tussen -$\Pgm\times\Input\times\Output\times\State$ en $\Pgm\times\Input\times\Output\times\State$ beschouwen. +$\Pgm\times\Input\times\Output\times\State$ en $\Gamma$ beschouwen. Waarbij $\Gamma$ óf $\Pgm\times\Input\times\Output\times\State$ óf $\Input\times\Output\times\State$ is. Dit schrijven we als -$$\sostrans{\stm:\pgm}{\ip}{\op}{\st}{\pgm}{\ip'}{\op'}{\st'}$$ -en lezen we als -\begin{quote} - ``het programma $\stm:\pgm$ zal in toestand $\st$ gegeven input $\ip$ en output $\op$ leiden tot - toestand $\st'$, met output $\op'$ waarbij $\ip'$ gelijk is aan $\ip$ zonder - de geconsumeerde input.'' -\end{quote} +$$\sostransgamma{\stm:\pgm}{\ip}{\op}{\st}{\gamma} \qquad \text{met\enspace + \parbox{36mm}{ $\gamma = (\pgm',\ip',\op',\st')$ of \\ $\gamma = (\ip', \op',\st' )$}}$$ + +De reden dat we hier spreken over $\pgm'$ is omdat de exec regel het programma dat je gaat uitvoeren verandert. In de meeste gevallen zal $\pgm$ = $\pgm'$ gelden maar dat hoeft dus niet. +\medskip Je kunt de structurele operationele semantiek zoals bij de natuurlijke semantiek definiëren aan de hand van de $\lambda$-regel maar om juist het verschil aan te geven met als je gebruik maakt van compositieregels, hebben wij ervoor gekozen om de structurele operationele semantiek te definiëren gebruik makende van compositieregels. -- cgit v1.2.3