--- /dev/null
+\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
repositories / sec1415.git / blobdiff