semantics.tex

   1 \subsection{Structurele operationele semantiek}
   2 Bij natuurlijke semantiek(ns) ligt de nadruk op de relatie tussen de begin en
   3 de eind state.  Het nadeel hiervan is dat programma’s die niet termineren geen
   4 bewijsbomen hebben.  Hierdoor is het niet mogelijk om eigenschappen te bewijzen
   5 voor zulke programma’s.  Bij structurele operationele semantiek(sos) ligt de
   6 nadruk juist op de individuele stappen van de executie en zijn er w\'el
   7 bewijsrijen voor programma’s die niet termineren.\\
   8 Om deze redenen hebben we gekozen voor sos.\\
   9 Een toestand in onze semantiek wordt beschreven door drie stacks; input, output
  10 en programma. Respectievelijk benoemen we deze met $s_i, s_o, s$ en beschrijven
  11 ze de STDIN, STDOUT en interne stack van het programma.  Stacks worden
  12 gerepresenteerd als: $s=[e_0, e_1, \dots, e_n]$ waarbij $e_i\in\mathbb{Z}$\\
  13 Het transitie systeem zal twee verschillende transities kennen, namelijk:\\
  14 $\langle S, s_i, s_o, s\rangle\Rightarrow\langle S', s_i', s_o', s'\rangle$ en\\
  15 $\langle S, s_i, s_o, s\rangle\Rightarrow\langle s_i', s_o', s'\rangle$\\
  16 Waarbij de laatste transitie duidt op een terminerende transitie en de eerste
  17 op een niet terminerende transitie.\\
  18
  19
  20
  21 \subsection{Semantiek beschrijving}
  22 Om het eerste element van een stack weg te kunnen gooien gebruiken we de volgende functie:\\
  23 $$\mathcal{D} : s \rightarrow s$$\\
  24 Deze neemt een stack en gooit het bovenste element weg.\\
  25
  26 Om een stack uit te kunnen breiden met een element gebruiken we de volgende functie:\\
  27 $$\mathcal{E} : s, \mathbb{Z} \rightarrow s$$\\
  28 Deze functie neemt een stack en een integer en voegt de integer toe bovenop de stack.\\
  29
  30 $[delete_{sos} ] \; <delete, s_i, s_o, s> \Rightarrow <s_i, s_o,\mathcal{D}[s]>$\\
  31
  32 $[extend_{sos} ] \; <extend \: z, s_i, s_o, s> \Rightarrow <s_i, s_o,\mathcal{E}[s, z]>$\\
  33
  34 $[pop_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>}{<pop, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>}$\\
  35
  36 $[add_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\: x+y, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<add \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$\\
  37
  38 $[subtract_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\:  x-y, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<subtract \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$\\
  39
  40 $[multiply_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\:  x*y, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<multiply \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$\\
  41
  42 $[divide_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\: x/y, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<divide \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$\\
  43
  44 $[mod_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\:  x \: mod \: y, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<mod \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$\\
  45
  46 $[duplicate_{sos} ] \; \frac{<extend\: x, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>}{<duplicate \: x, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>}$\\
  47
  48 $[not^0_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <extend\: 1, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''>}{<not \: x, s_i, s_o, s> \Rightarrow <s_i, s_o, s''>}$ if x = 0\\
  49
  50 $[not^*_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <extend\: 0, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''>}{<not \: x, s_i, s_o, s> \Rightarrow <s_i, s_o, s''>}$ if x $\neq$ 0\\
  51
  52 $[greater^<_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\:,1, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<greater \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$ if x$<$y\\
  53
  54 $[greater^>_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\: 0, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<greater \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$ if x$>$y\\