\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{Semantiek beschrijving}
Om het eerste element van een stack weg te kunnen gooien gebruiken we de volgende functie:\\
$$\mathcal{D} : s \rightarrow s$$\\
Deze neemt een stack en gooit het bovenste element weg.\\

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

\footnotesize
$\infer	[{[}delete_{sos}{]}]
		{	\langle delete, s_i, s_o, s\rangle \Rightarrow
				\langle s_i,s_o,\mathcal{D}[s]\rangle}{}\\
\infer	[{[}extend_{sos}{]}]
		{	\langle extend \: z, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o,\mathcal{E}[s, z]\rangle}{}\\
\infer	[{[}pop_{sos} {]}]
		{	\langle delete, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s'\rangle}
		{	\langle pop, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s'\rangle}\\
\infer	[{[}add_{sos} {]}]
		{	\langle delete, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s'\rangle \quad
			\langle delete, s_i, s_o, s'\rangle \Rightarrow
				\langle s_i, s_o, s''\rangle \quad
			\langle extend\: x+y, s_i, s_o, s''\rangle \Rightarrow
				\langle s_i, s_o, s'''\rangle}
		{	\langle add \: x,y, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s'''\rangle}\\
\infer	[{[}subtract_{sos} {]}]
		{	\langle delete, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s'\rangle \quad
			\langle delete, s_i, s_o, s'\rangle \Rightarrow
				\langle s_i, s_o, s''\rangle \quad
			\langle extend\: x-y, s_i, s_o, s''\rangle \Rightarrow
				\langle s_i, s_o, s'''\rangle}
		{	\langle subtract \: x,y, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s'''\rangle}\\
\infer	[{[}multiply_{sos} {]}]
		{	\langle delete, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s'\rangle \quad
			\langle delete, s_i, s_o, s'\rangle \Rightarrow
				\langle s_i, s_o, s''\rangle \quad
			\langle extend\: x*y, s_i, s_o, s''\rangle \Rightarrow
				\langle s_i, s_o, s'''\rangle}
		{	\langle multiply \: x,y, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s'''\rangle}\\
\infer	[{[}divide_{sos} {]}]
		{	\langle delete, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s'\rangle \quad
			\langle delete, s_i, s_o, s'\rangle \Rightarrow
				\langle s_i, s_o, s''\rangle \quad
			\langle extend\: x/y, s_i, s_o, s''\rangle \Rightarrow
				\langle s_i, s_o, s'''\rangle}
		{	\langle divide \: x,y, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s'''\rangle}\\
\infer	[{[}mod_{sos} {]}]
		{	\langle delete, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s'\rangle \quad
			\langle delete, s_i, s_o, s'\rangle \Rightarrow
				\langle s_i, s_o, s''\rangle \quad
			\langle extend\: x \: mod \: y, s_i, s_o, s''\rangle \Rightarrow
				\langle s_i, s_o, s'''\rangle}
		{	\langle mod \: x,y, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s'''\rangle}\\
\infer	[{[}duplicate_{sos} {]}]
		{	\langle extend\: x, s_i, s_o, s\rangle \Rightarrow
			\langle s_i, s_o, s'\rangle}
		{	\langle duplicate \: x, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s'\rangle}\\
\infer	[{[}not^0_{sos} {]}]
		{	\langle delete, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s'\rangle \quad
			\langle extend\: 1, s_i, s_o, s'\rangle \Rightarrow
				\langle s_i, s_o, s''\rangle}
		{	\langle not \: x, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s''\rangle}$ if $x = 0\\
\infer	[{[}not^*_{sos} {]}]
		{	\langle delete, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s'\rangle \quad 
			\langle extend\: 0, s_i, s_o, s'\rangle \Rightarrow
				\langle s_i, s_o, s''\rangle}
		{	\langle not \: x, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s''\rangle}$ if $x\neq 0\\
\infer	[{[}greater^<_{sos} {]}]
		{	\langle delete, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s'\rangle \quad 
			\langle delete, s_i, s_o, s'\rangle \Rightarrow
				\langle s_i, s_o, s''\rangle \quad 
			\langle extend\:,1, s_i, s_o, s''\rangle \Rightarrow 
				\langle s_i, s_o, s'''\rangle}
		{	\langle greater \: x,y, s_i, s_o, s\rangle \Rightarrow
			\langle s_i, s_o, s'''\rangle}$ if $x>y\\
\infer	[{[}greater^>_{sos} {]}]
		{	\langle delete, s_i, s_o, s\rangle \Rightarrow
				\langle s_i, s_o, s'\rangle \quad 
			\langle delete, s_i, s_o, s'\rangle \Rightarrow
				\langle s_i, s_o, s''\rangle \quad 
			\langle extend\: 0, s_i, s_o, s''\rangle \Rightarrow 
				\langle s_i, s_o, s'''\rangle}
		{	\langle greater \: x,y, s_i, s_o, s\rangle \Rightarrow 
				\langle s_i, s_o, s'''\rangle}$ if $x<y
$
\normalsize
