\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
bewijsbomen hebben.  Hierdoor is het niet mogelijk om eigenschappen te bewijzen
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.\\
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}$\\
Het transitie systeem 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
op een niet terminerende transitie.\\ 

\subsection{Semantiekbeschrijving}

Om het bovenste element van een stack weg te kunnen gooien gebruiken we de volgende 
functie:\\
$$\mathcal{D} : Stack \rightarrow Stack$$
$$\mathcal{D} [\:] = [\:]$$
$$\mathcal{D} [a:rest] = [rest] $$
Deze functie haalt het bovenste element van de stack en gooit deze weg.\\

Om een stack uit te kunnen breiden met een element gebruiken we de volgende 
functie:\\
$$\mathcal{E} : Stack\rightarrow (\mathbb{Z} \rightarrow Stack)$$\\
Deze functie neemt een stack en een integer en voegt de integer toe bovenop de 
stack.\\

Om de bovenste twee elementen van een stack op te tellen gebruiken we de volgende 
functie:\\
$$\mathcal{ADD} : Stack \rightarrow Stack$$
$$\mathcal{ADD} [\:] = [\:]$$
$$\mathcal{ADD} [a] = [a] $$
$$\mathcal{ADD} [a:b:rest] = [b+a:rest] $$\\
Deze functie haalt de bovenste twee waarden van de stack, telt ze bij elkaar op, en stopt 
het resultaat bovenop de stack.\\

Om de bovenste twee elementen van een stack van elkaar af te trekken gebruiken we 
de volgende functie:\\
$$\mathcal{SUB} : Stack \rightarrow Stack$$
$$\mathcal{SUB} [\:] = [\:]$$
$$\mathcal{SUB} [a] = [a] $$
$$\mathcal{SUB} [a:b:rest] = [b-a:rest] $$\\
Deze functie haalt de bovenste twee elementen van de stack, trekt de bovenste 
waarde van de tweede bovenste waarde af, en stopt het resultaat bovenop de stack.

Om de bovenste twee elementen van een stack te vermenigvuldigen gebruiken we de 
volgende functie:\\
$$\mathcal{MUL} : Stack \rightarrow Stack$$
$$\mathcal{MUL} [\:] = [\:]$$
$$\mathcal{MUL} [a] = [a] $$
$$\mathcal{MUL} [a:b:rest] = [b*a:rest] $$\\
Deze functie haalt de bovenste twee elementen van de stack, vermenigvuldigt ze, 
en stopt het resultaat bovenop de stack.\\

Om de geheeltallige deling van de bovenste twee elementen van de stack bovenop de 
stack te krijgen gebruiken we de volgende functie:\\
$$\mathcal{DIV} : Stack \rightarrow Stack$$
$$\mathcal{DIV} [\:] = [\:]$$
$$\mathcal{DIV} [a] = [a] $$
$$\mathcal{DIV} [a:b:rest] = [b/a:rest] $$\\
Deze functie haalt de bovenste twee elementen van de stack, berekent de 
geheeltallige deling van de tweede bovenste waarde door de bovenste waarde, 
en stopt het resultaat bovenop de stack.\\

Om    gebruiken we de
volgende functie:\\
$$\mathcal{MOD} : Stack \rightarrow Stack$$
$$\mathcal{MOD} [\:] = [\:]$$
$$\mathcal{MOD} [a] = [a] $$
$$\mathcal{MOD} [a:b:rest] = [b \: mod \: a:rest] $$\\
Deze functie haalt de bovenste twee elementen van de stack, berekent het resultaat van de tweede bovenste 
waarde modulo de bovenste waarde, en stopt dit bovenop de stack.\\

Om het bovenste element van een stack te dupliceren gebruiken we de 
volgende functie:\\
$$\mathcal{DUP} : Stack \rightarrow Stack$$
$$\mathcal{DUP} [\:] = [\:]$$
$$\mathcal{DUP} [a:rest] = [a:a:rest] $$\\
Deze functie haalt stopt een kopie van de bovenste waarde bovenop de stack.\\

Om de   gebruiken we de 
volgende functie:\\
$$\mathcal{NOT} : Stack \rightarrow Stack$$
$$\mathcal{NOT} [\:] = [\:]$$
$$\mathcal{NOT} [0:rest] = [1:rest]$$
$$\mathcal{NOT} [\_:rest] = [0:rest] $$\\

Deze functie neemt het bovenste element van de stack en stopt 0 bovenaan de 
stack als deze waarde niet gelijk is aan 0 en 1 als deze waarde gelijk is aan 0.\\

Om   gebruiken we de 
volgende functie:\\
$$\mathcal{GRE} : Stack \rightarrow Stack$$
$$\mathcal{GRE} [\:] = [\:]$$
$$\mathcal{GRE} [a] = [a] $$
$$\mathcal{GRE} [a:b:rest]$$
$$\qquad \qquad | \: a \geq b =  [0:rest]$$
$$\qquad \qquad | \: a < b =  [1:rest]$$\\

$$\mathcal{ROLL} : Stack \rightarrow Stack$$
$$\mathcal{ROLL} [\:] = [\:]$$
$$\mathcal{ROLL} [a] = [a] $$
$$\mathcal{ROLL} [a:b:rest]$$
$$\qquad \qquad | modulo \: a \: b == 0 = rest$$
$$\qquad \qquad | b <= 0 = rest$$
$$\qquad \qquad | b > length rest = rest$$
$$\qquad \qquad | a == 1 = roll1 [b:rest]$$
$$\qquad \qquad | a > 0 = roll([a-1] ++ [b] ++ roll1 [b:rest]$$
$$\qquad \qquad | a < 0 = roll(modulo \: a \: b] ++ [b:rest])$$

$$\mathcal{ROLL}1 : Stack \rightarrow Stack$$
$$\mathcal{ROLL}1 [1:rest] = [rest]$$
$$\mathcal{ROLL}1 [b:c:d:rest] = [d] ++ \mathcal{ROLL}1 [b-1:c:rest]$$


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

Met behulp van deze gedefinieerde functies kunnen we nu de volgende semantiekregels opstellen:\\

$
{[pop_{sos}]}\qquad
\langle pop, s_i, s_o, s\rangle \Rightarrow
\langle s_i, s_o,\mathcal{D}(s)\rangle\\
{[add_{sos}]}\qquad
\langle add, s_i, s_o, s\rangle \Rightarrow
\langle s_i, s_o, \mathcal{ADD}(s)\rangle\\
{[subtract_{sos} ]}\qquad
\langle subtract, s_i, s_o, s\rangle \Rightarrow
\langle s_i, s_o, \mathcal{SUB}(s)\rangle\\
{[multiply_{sos}]}\qquad
\langle multiply, s_i, s_o, s\rangle \Rightarrow
\langle s_i, s_o, \mathcal{MUL}(s)\rangle\\
{[divide_{sos}]} \qquad
\langle divide, s_i, s_o, s\rangle \Rightarrow
\langle s_i, s_o, \mathcal{DIV}(s)\rangle\\
{[mod_{sos}]} \qquad\qquad
\langle mod, s_i, s_o, s\rangle \Rightarrow
\langle s_i, s_o, \mathcal{MOD}(s)\rangle\\
{[duplicate_{sos}]} \qquad
\langle duplicate, s_i, s_o, s\rangle \Rightarrow
\langle s_i, s_o, \mathcal{DUP}(s)\rangle\\
{[not_{sos}]}\qquad\qquad
\langle not, s_i, s_o, s\rangle \Rightarrow
\langle s_i, s_o, \mathcal{NOT}(s)\rangle\\
{[greater_{sos}]} \qquad
\langle greater, s_i, s_o, s\rangle \Rightarrow
\langle s_i, s_o, \mathcal{GRE}(s)\rangle\\
{[push_{sos}]} \qquad
\langle push \: n, s_i, s_o, s\rangle \Rightarrow
\langle s_i, s_o, \mathcal{E}(n,s)\rangle\\
{[roll_{sos}]} \qquad
\langle roll, s_i, s_o, s\rangle \Rightarrow
\langle s_i, s_o, \mathcal{ROLL}(s)\rangle\\
{[inchar_{sos}]} \qquad
\langle inchar, s_i, s_o, s\rangle \Rightarrow
\langle s_i, s_o, s\rangle\\
{[innum_{sos}]} \qquad
\langle innum, 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\\
{[outnum_{sos}]} \qquad
\langle outnum, s_i, s_o, s\rangle \Rightarrow
\langle s_i, s_o, s\rangle\\
$
