\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}