Merge branch 'master' of github.com:W-M-T/Berekeningsmodellen-IBC025---voorjaar-2016

2 files changed, 32 insertions, 19 deletions

diff --git a/deftrans.tex b/deftrans.tex
index d83bf55..a4d5669 100644
--- a/deftrans.tex
+++ b/deftrans.tex
@@ -1,7 +1,9 @@
 % 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 denken wij dat we door het gebruik van natuurlijke semantiek meer kunnen in onze analyse. 
+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, dit zullen we dan ook nog even kort toelichten in \autoref{sec:sos} . Echter zal de verdere uitwerking dus in natuurlijke semantiek zijn. 
+
+\medskip
 
 Bij het definiëren van de natuurlijke semantiek van Smurf zullen we de
 verzameling van transities als een relatie $\to$ tussen
diff --git a/sosexamp.tex b/sosexamp.tex
index 641acb4..e3926e8 100644
--- a/sosexamp.tex
+++ b/sosexamp.tex
@@ -1,46 +1,55 @@
 % vim:set spelllang=nl:
 \section{Smurf in structurele operationele semantiek}
 \label{sec:sos}
-We willen ook nog graag laten zien hoe de definities van Smurf eruit zien als
+We willen ook laten zien hoe de definities van Smurf eruit zien als
 je de structurele operationele semantiek gebruikt. In principe maakt het voor
 de analyse van Smurf niet uit of je natuurlijke semantiek gebruikt of
-structurele operationele semantiek. Omdat natuurlijke semantiek en structurele
-operationele semantiek equivalent zijn wanneer de regels goed gedefinieerd
-zijn. Wij hadden een voorkeur om natuurlijke semantiek te gebruiken omdat we
+structurele operationele semantiek. Wij hadden een voorkeur om natuurlijke semantiek te gebruiken omdat we
 hier meer bekend mee zijn. Echter willen we ook nog graag laten zien hoe het
 eruit zou zien als je structurele operationele semantiek zou gebruiken.
 
-We gebruiken hier in plaats van de $\lambda$-regel twee compositieregels om
-hiervan ook het verschil aan te geven.
+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.
+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}
 
-De twee compositieregels zijn als volgt:
+ 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. 
+
+De compositieregel is dan als volgt:
 
 $$
 \begin{prooftree}
-	\sostrans
+	\sostranseind
 		{\stm}{\ip}{\op}{(\stk, \str)}
-		{\pgm'}{\ip'}{\op'}{(\stk', \str')}
+		{\ip'}{\op'}{(\stk', \str')}
 	\justifies
 	\sostrans
 		{\stm:\pgm}{\ip}{\op}{(\stk,\str)}
-		{\pgm'}{\ip'}{\op'}{(\stk',\str')}
+		{\pgm}{\ip'}{\op'}{(\stk',\str')}
 	\using{\rcompeensos}
 	\qquad
 \end{prooftree}
 $$
 
-\medskip
+\bigskip
+
+De regel voor $\StmExec$ zou in de structurele operationele semantiek als volgt zijn: 
 $$
 \begin{prooftree}
-	\sostranseind
-		{\stm}{\ip}{\op}{(\stk, \str)}
-		{\ip'}{\op'}{(\stk', \str')}
-	\justifies
+\axjustifies
 	\sostrans
-		{\stm:\pgm}{\ip}{\op}{(\stk,\str)}
-		{\pgm}{\ip'}{\op'}{(\stk',\str')}
-	\using{\rcomptweesos}
+		{\StmExec:\pgm}{\ip}{\op}{(\stk,\str)}
+		{\pgm'}{\ip'}{\op'}{(\stk',\str')}
+	\using{\rexecsos}
 	\qquad
+		\text{met $\pop{\stk} = ( \pgm', \stk'')$.}
 \end{prooftree}
 $$
 
@@ -59,3 +68,5 @@ $$
 	\text{met $\pop{\stk} = (c~s,\stk')$.}
 \end{prooftree}
 $$
+
+De andere regels zoals head en exec zullen we hier niet verder uitwerken omdat deze op een soortgelijke wijzen worden gemaakt. 
\ No newline at end of file