X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=semantics.tex;h=f7fb7faaeb275084c8127acc152ad400b5903e82;hb=d5eb78db13b8b04fdf0a3edf3e636dd9006948af;hp=00eca8a6968db66c17aa5e2ac9b16b65d3a4ed77;hpb=bf5101db32613e6ccd3b6cc3043734822cf29bd9;p=sec1415.git

diff --git a/semantics.tex b/semantics.tex
index 00eca8a..f7fb7fa 100644
--- a/semantics.tex
+++ b/semantics.tex
@@ -1,21 +1,23 @@
 \subsection{Structurele operationele semantiek}
 Bij natuurlijke semantiek(ns) ligt de nadruk op de relatie tussen de begin en
-de eind state.  Het nadeel hiervan is dat programma’s die niet termineren geen
+de eind state.  Het nadeel hiervan is dat programma's die niet termineren geen
 bewijsbomen hebben.  Hierdoor is het niet mogelijk om eigenschappen te bewijzen
-voor zulke programma’s.  Bij structurele operationele semantiek(sos) ligt de
+voor zulke programma's.  Bij structurele operationele semantiek(sos) ligt de
 nadruk juist op de individuele stappen van de executie en zijn er w\'el
-bewijsrijen voor programma’s die niet termineren.\\
+bewijsrijen voor programma's die niet termineren.\\
 Om deze redenen hebben we gekozen voor sos.\\ 
 Een toestand in onze semantiek wordt beschreven door drie stacks; input, output
 en programma. Respectievelijk benoemen we deze met $s_i, s_o, s$ en beschrijven
 ze de STDIN, STDOUT en interne stack van het programma.  Stacks worden
 gerepresenteerd als: $s=[e_0, e_1, \dots, e_n]$ waarbij $e_i\in\mathbb{Z}$
- en waarbij het bovenste element op de stack gerepresenteerd word door het
+ en waarbij het bovenste element op de stack gerepresenteerd wordt door het
  eerste element in de lijst.\\
-Het transitie systeem zal twee verschillende transities kennen, namelijk:\\ 
+Het transitiesysteem zal twee verschillende transities kennen, namelijk:\\ 
 $\langle S, s_i, s_o, s\rangle\Rightarrow\langle S', s_i', s_o', s'\rangle$ en\\ 
 $\langle S, s_i, s_o, s\rangle\Rightarrow\langle s_i', s_o', s'\rangle$\\ 
-Waarbij de laatste transitie duidt op een terminerende transitie en de eerste
+Waarbij de laatste transitie duidt op een transitie waar een volgende transitie
+aanwezig is en genomen kan worden. De tweede duidt op een transitie waarbij er
+geen volgede beschikbaar is en het programma dus termineerd.
 op een niet terminerende transitie.\\ 
 
 \subsection{Semantiekbeschrijving}
@@ -102,27 +104,25 @@ Deze functie haalt de bovenste twee elementen van de stack en stopt 1 bovenop
 de stack als het tweede bovenste element een hogere waarde heeft als dat van het 
 bovenste element. Anders word 1 bovenop de stack gestopt.\\ 
 
-out number (output stack) functie (outnum, r. 79):\\
+out number (output stack) functie (outnum, r. 70):\\
 Deze functie past de output stack aan als er een integer naartoe geschreven word:\\
 $$\mathcal{OUTN_{SO}} : Stack \rightarrow Stack$$\\
 Deze functie haalt het bovenste element van de stack en stopt dit element bovenop de output stack.\\
 
-in number (stack) functie (innum, r. 84):\\
+in number (stack) functie (innum, r. 75):\\
 Deze functie past de stack aan als er een integer naartoe geschreven word:\\
 $$\mathcal{INN_S} : Stack \rightarrow Stack$$\\
 Deze functie haalt het bovenste element van de input stack en stopt dit element bovenop de output stack.\\
 
-(outchar, inchar)\\
-
 Met behulp van deze gedefinieerde functies kunnen we nu de volgende semantiekregels opstellen:\\
 
 \begin{alignat*}{2}
 {[comp^1_{sos}]}\qquad &
-\frac{\langle S_1, s\rangle \Rightarrow \langle S'_1, s'\rangle}
-{\langle S_1 ;S_2, s\rangle \Rightarrow \langle S'_1;S_2, s'\rangle}\\
+\frac{\langle S_2, s\rangle \Rightarrow \langle S'_2, s'\rangle}
+{\langle S_1 ;S_2, s\rangle \Rightarrow \langle S_1;S'_2, s'\rangle}\\
 {[comp^2_{sos}]}\qquad &
-\frac{\langle S_1, s\rangle \Rightarrow \langle s'\rangle}
-{\langle S_1 ;S_2, s\rangle \Rightarrow \langle S_2, s'\rangle}\\
+\frac{\langle S_2, s\rangle \Rightarrow \langle s'\rangle}
+{\langle S_1 ;S_2, s\rangle \Rightarrow \langle S_1, s'\rangle}\\
 {[pop_{sos}]}\qquad &
 \langle pop, s_i, s_o, s\rangle \Rightarrow
 \langle s_i, s_o,\mathcal{D}(s)\rangle\\
@@ -168,11 +168,5 @@ Met behulp van deze gedefinieerde functies kunnen we nu de volgende semantiekreg
 {[outnum_{sos}]} \qquad &
 \langle outnum, s_i, s_o, s\rangle \Rightarrow
 \langle s_i, \mathcal{OUTN_{SO}}(s_o),\mathcal{D}(s)\rangle\\
-{[inchar_{sos}]} \qquad &
-\langle inchar, s_i, s_o, s\rangle \Rightarrow
-\langle s_i, s_o, s\rangle\\
-{[outchar_{sos}]} \qquad &
-\langle outchar, s_i, s_o, s\rangle \Rightarrow
-\langle s_i, s_o, s\rangle\\
 \end{alignat*}