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  en waarbij het bovenste element op de stack gerepresenteerd wordt door het
  14  eerste element in de lijst.\\
  15 Het transitiesysteem zal twee verschillende transities kennen, namelijk:\\
  16 $\langle S, s_i, s_o, s\rangle\Rightarrow\langle S', s_i', s_o', s'\rangle$ en\\
  17 $\langle S, s_i, s_o, s\rangle\Rightarrow\langle s_i', s_o', s'\rangle$\\
  18 Waarbij de laatste transitie duidt op een transitie waar een volgende transitie
  19 aanwezig is en genomen kan worden. De tweede duidt op een transitie waarbij er
  20 geen volgede beschikbaar is en het programma dus termineerd.
  21 op een niet terminerende transitie.\\
  22
  23 \subsection{Semantiekbeschrijving}
  24
  25 Om de semantiekregels te kunnen beschrijven maken we gebruik van hulpfuncties. Hieronder staat het type van de functies en een korte beschrijving.
  26 De implementatie van deze functies staat in de appendix. De functies worden op de volgende manier aangegeven: \textit{naam functie} (\textit{naam in appendix}, r. \textit{regelnummer})\\
  27
  28 delete functie (d, r. 5):\\
  29 Om het bovenste element van een stack weg te kunnen gooien gebruiken we de volgende
  30 functie:\\
  31 $$\mathcal{D} : Stack \rightarrow Stack$$
  32 Deze functie haalt het bovenste element van de stack en gooit dit weg.\\
  33
  34 extend functie (e, r. 9):\\
  35 Om een stack uit te kunnen breiden met een element gebruiken we de volgende
  36 functie:\\
  37 $$\mathcal{E} : \mathbb{Z}\rightarrow (Stack\rightarrow Stack)$$\\
  38 Deze functie neemt een integer en een stack en voegt de integer toe bovenop de
  39 stack.\\
  40
  41 add functie (add, r. 13):\\
  42 Om de bovenste twee elementen van een stack op te tellen gebruiken we de volgende
  43 functie:\\
  44 $$\mathcal{ADD} : Stack \rightarrow Stack$$
  45 Deze functie haalt de bovenste twee waarden van de stack, telt ze bij elkaar op, en legt
  46 het resultaat bovenop de stack.\\
  47
  48 subtract functie (sub, r. 18)\\
  49 Om de bovenste twee elementen van een stack van elkaar af te trekken gebruiken we
  50 de volgende functie:\\
  51 $$\mathcal{SUB} : Stack \rightarrow Stack$$
  52 Deze functie haalt de bovenste twee elementen van de stack, trekt de bovenste
  53 waarde van de tweede bovenste waarde af, en legt het resultaat bovenop de stack.\\
  54
  55 multiply functie (mul, r. 23):\\
  56 Om de bovenste twee elementen van een stack te vermenigvuldigen gebruiken we de
  57 volgende functie:\\
  58 $$\mathcal{MUL} : Stack \rightarrow Stack$$
  59 Deze functie haalt de bovenste twee elementen van de stack, vermenigvuldigt ze,
  60 en stopt het resultaat bovenop de stack.\\
  61
  62 division functie (div, r. 28):\\
  63 Om de geheeltallige deling van de bovenste twee elementen van de stack bovenop de
  64 stack te krijgen gebruiken we de volgende functie:\\
  65 $$\mathcal{DIV} : Stack \rightarrow Stack$$
  66 Deze functie haalt de bovenste twee elementen van de stack, berekent de
  67 geheeltallige deling van de tweede bovenste waarde door de bovenste waarde,
  68 en stopt het resultaat bovenop de stack.\\
  69
  70 modulo functie (modc, r. 33):\\
  71 Om  de tweede bovenste waarde modulo de bovenste waarde te berekenen
  72 gebruiken we de volgende functie:\\
  73 $$\mathcal{MOD} : Stack \rightarrow Stack$$
  74 Deze functie haalt de bovenste twee elementen van de stack, berekent het
  75 resultaat van de tweede bovenste waarde modulo de bovenste waarde, en
  76 stopt dit bovenop de stack.\\
  77
  78 duplicate functie (dup, r. 38):\\
  79 Om het bovenste element van een stack te dupliceren gebruiken we de
  80 volgende functie:\\
  81 $$\mathcal{DUP} : Stack \rightarrow Stack$$
  82 Deze functie haalt de bovenste waarde van de stack en stopt een kopie
  83 en de bovenste waarde bovenop de stack.\\
  84
  85 not functie (notc, r. 42):\\
  86 Om te kijken of de bovenste waarde gelijk is aan 0 gebruiken we de
  87 volgende functie:\\
  88 $$\mathcal{NOT} : Stack \rightarrow Stack$$\\
  89 Deze functie neemt het bovenste element van de stack en stopt 0 bovenaan de
  90 stack als deze waarde niet gelijk is aan 0 en 1 als deze waarde gelijk is aan 0.\\
  91
  92 greater functie (gre, r. 47):\\
  93 Om te kijken of de tweede bovenste waarde groter is dan de bovenste waarde
  94 gebruiken we de volgende functie:\\
  95 $$\mathcal{GRE} : Stack \rightarrow Stack$$\\
  96 Deze functie haalt de bovenste twee waarden van de stack en stopt een 1 bovenop
  97 de stack als de tweede bovenste waarde groter is dan de bovenste waarde. Anders
  98 wordt een 0 bovenop de stack gestopt.\\
  99
 100 roll functie (roll, r. 54):\\
 101 Om de stack elementen te verschuiven gebruiken we de volgende functie:\\
 102 $$\mathcal{ROLL} : Stack \rightarrow Stack$$\\
 103 Deze functie haalt de bovenste twee elementen van de stack 'rolt' de rest van de stack tot een diepte die gelijk is aan de waarde van het tweede bovenste element. Een rol tot diepte \textit{n} verschuift de elementen 1 tot en met \textit{n} allemaal 1 plaats naar boven. Vervolgens wordt het eerste element van de stack op plaats \textit{n} neergelegd. Het aantal keren dat de stack gerold wordt is gelijk aan de waarde van het bovenste element. Als deze waarde negatief is word de stack in tegenovergestelde richting gerold. Dit houdt in dat bij elke rol het element op plaats \textit{n} bovenop de stack word gelegt, en de rest van de elementen (dat boven het element op plaats \textit{n} lagen) 1 plaats naar beneden wordt verschoven.\\
 104
 105 out number (output stack) functie (outnum, r. 70):\\
 106 Deze functie past de output stack aan als er een integer naartoe geschreven wordt:\\
 107 $$\mathcal{OUTN_{SO}} : Stack \rightarrow Stack$$\\
 108 Deze functie haalt het bovenste element van de stack en stopt dit element bovenop de output stack.\\
 109
 110 in number (stack) functie (innum, r. 75):\\
 111 Deze functie past de stack aan als er een integer naartoe geschreven wordt:\\
 112 $$\mathcal{INN_S} : Stack \rightarrow Stack$$\\
 113 Deze functie haalt het bovenste element van de input stack en stopt dit element bovenop de output stack.\\
 114
 115 Met behulp van deze gedefinieerde functies kunnen we nu de volgende semantiekregels opstellen:\\
 116
 117 \begin{alignat*}{2}
 118 {[comp^1_{sos}]}\qquad &
 119 \frac{\langle S_2, s\rangle \Rightarrow \langle S'_2, s_i', s_o', s'\rangle}
 120 {\langle S_1 ;S_2, s\rangle \Rightarrow \langle S_1;S'_2, s_i', s_o', s'\rangle}\\
 121 {[comp^2_{sos}]}\qquad &
 122 \frac{\langle S_2, s\rangle \Rightarrow \langle s_i', s_o', s'\rangle}
 123 {\langle S_1 ;S_2, s\rangle \Rightarrow \langle S_1, s_i', s_o', s'\rangle}\\
 124 {[pop_{sos}]}\qquad &
 125 \langle pop, s_i, s_o, s\rangle \Rightarrow
 126 \langle s_i, s_o,\mathcal{D}(s)\rangle\\
 127 {[add_{sos}]}\qquad
 128 &\langle add, s_i, s_o, s\rangle \Rightarrow
 129 \langle s_i, s_o, \mathcal{ADD}(s)\rangle\\
 130 {[subtract_{sos} ]}\qquad &
 131 \langle subtract, s_i, s_o, s\rangle \Rightarrow
 132 \langle s_i, s_o, \mathcal{SUB}(s)\rangle\\
 133 {[multiply_{sos}]}\qquad &
 134 \langle multiply, s_i, s_o, s\rangle \Rightarrow
 135 \langle s_i, s_o, \mathcal{MUL}(s)\rangle\\
 136 {[divide_{sos}]} \qquad &
 137 \langle divide, s_i, s_o, s\rangle \Rightarrow
 138 \langle s_i, s_o, \mathcal{DIV}(s)\rangle\\
 139 {[mod_{sos}]} \qquad &
 140 \langle mod, s_i, s_o, s\rangle \Rightarrow
 141 \langle s_i, s_o, \mathcal{MOD}(s)\rangle\\
 142 {[duplicate_{sos}]} \qquad &
 143 \langle duplicate, s_i, s_o, s\rangle \Rightarrow
 144 \langle s_i, s_o, \mathcal{DUP}(s)\rangle\\
 145 {[not_{sos}]} \qquad &
 146 \langle not, s_i, s_o, s\rangle \Rightarrow
 147 \langle s_i, s_o, \mathcal{NOT}(s)\rangle\\
 148 {[greater_{sos}]} \qquad &
 149 \langle greater, s_i, s_o, s\rangle \Rightarrow
 150 \langle s_i, s_o, \mathcal{GRE}(s)\rangle\\
 151 {[pointer_{sos}]} \qquad &
 152 \langle pointer, s_i, s_o, s\rangle \Rightarrow
 153 \langle s_i, s_o, \mathcal{D}(s)\rangle\\
 154 {[switch_{sos}]} \qquad &
 155 \langle switch, s_i, s_o, s\rangle \Rightarrow
 156 \langle s_i, s_o, \mathcal{D}(s)\rangle\\
 157 {[push_{sos}]} \qquad &
 158 \langle push \: n, s_i, s_o, s\rangle \Rightarrow
 159 \langle s_i, s_o, \mathcal{E}(n,s)\rangle\\
 160 {[roll_{sos}]} \qquad &
 161 \langle roll, s_i, s_o, s\rangle \Rightarrow
 162 \langle s_i, s_o, \mathcal{ROLL}(s)\rangle\\
 163 {[innum_{sos}]} \qquad &
 164 \langle innum, s_i, s_o, s\rangle \Rightarrow
 165 \langle \mathcal{D}(s_i), s_o, \mathcal{INN_S}(s)\rangle\\
 166 {[outnum_{sos}]} \qquad &
 167 \langle outnum, s_i, s_o, s\rangle \Rightarrow
 168 \langle s_i, \mathcal{OUTN_{SO}}(s_o),\mathcal{D}(s)\rangle\\
 169 \end{alignat*}
 170