\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}
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\\
{[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*}
repositories / sec1415.git / blobdiff