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 word door het
  14  eerste element in de lijst.\\
  15 Het transitie systeem 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 terminerende transitie en de eerste
  19 op een niet terminerende transitie.\\
  20
  21 \subsection{Semantiekbeschrijving}
  22
  23 Om de semantiekregels te kunnen beschrijven maken we gebruik van hulpfuncties. Hieronder staat het type van de functies en een korte beschrijving.
  24 De implementatie van deze functies staat in de appendix bij het aangegeven regelnummer.\\
  25
  26 delete functie (d, r. 5):\\
  27 Om het bovenste element van een stack weg te kunnen gooien gebruiken we de volgende
  28 functie:\\
  29 $$\mathcal{D} : Stack \rightarrow Stack$$
  30 Deze functie haalt het bovenste element van de stack en gooit deze weg.\\
  31
  32 extend functie (e, r. 9):\\
  33 Om een stack uit te kunnen breiden met een element gebruiken we de volgende
  34 functie:\\
  35 $$\mathcal{E} : \mathbb{Z}\rightarrow (Stack\rightarrow Stack)$$\\
  36 Deze functie neemt een stack en een integer en voegt de integer toe bovenop de
  37 stack.\\
  38
  39 add functie (add, r. 13):\\
  40 Om de bovenste twee elementen van een stack op te tellen gebruiken we de volgende
  41 functie:\\
  42 $$\mathcal{ADD} : Stack \rightarrow Stack$$
  43 Deze functie haalt de bovenste twee waarden van de stack, telt ze bij elkaar op, en stopt
  44 het resultaat bovenop de stack.\\
  45
  46 subtract functie (sub, r. 18)\\
  47 Om de bovenste twee elementen van een stack van elkaar af te trekken gebruiken we
  48 de volgende functie:\\
  49 $$\mathcal{SUB} : Stack \rightarrow Stack$$
  50 Deze functie haalt de bovenste twee elementen van de stack, trekt de bovenste
  51 waarde van de tweede bovenste waarde af, en stopt het resultaat bovenop de stack.\\
  52
  53 multiply functie (mul, r. 23):\\
  54 Om de bovenste twee elementen van een stack te vermenigvuldigen gebruiken we de
  55 volgende functie:\\
  56 $$\mathcal{MUL} : Stack \rightarrow Stack$$
  57 Deze functie haalt de bovenste twee elementen van de stack, vermenigvuldigt ze,
  58 en stopt het resultaat bovenop de stack.\\
  59
  60 division functie (div, r. 28):\\
  61 Om de geheeltallige deling van de bovenste twee elementen van de stack bovenop de
  62 stack te krijgen gebruiken we de volgende functie:\\
  63 $$\mathcal{DIV} : Stack \rightarrow Stack$$
  64 Deze functie haalt de bovenste twee elementen van de stack, berekent de
  65 geheeltallige deling van de tweede bovenste waarde door de bovenste waarde,
  66 en stopt het resultaat bovenop de stack.\\
  67
  68 modulo functie (modc, r. 33):\\
  69 Om  de tweede bovenste waarde modulo de bovenste waarde te berekenen
  70 gebruiken we de volgende functie:\\
  71 $$\mathcal{MOD} : Stack \rightarrow Stack$$
  72 Deze functie haalt de bovenste twee elementen van de stack, berekent het
  73 resultaat van de tweede bovenste waarde modulo de bovenste waarde, en
  74 stopt dit bovenop de stack.\\
  75
  76 duplicate functie (dup, r. 38):\\
  77 Om het bovenste element van een stack te dupliceren gebruiken we de
  78 volgende functie:\\
  79 $$\mathcal{DUP} : Stack \rightarrow Stack$$
  80 Deze functie haalt de bovenste waarde van de stack en stopt een kopie
  81 en de bovenste waarde bovenop de stack.\\
  82
  83 not functie (notc, r. 42):\\
  84 Om de not van de bovenste waarde te berekenen gebruiken we de
  85 volgende functie:\\
  86 $$\mathcal{NOT} : Stack \rightarrow Stack$$\\
  87 Deze functie neemt het bovenste element van de stack en stopt 0 bovenaan de
  88 stack als deze waarde niet gelijk is aan 0 en 1 als deze waarde gelijk is aan 0.\\
  89
  90 greater functie (gre, r. 47):\\
  91 Om kijken of de tweede bovenste waarde groter is dan de bovenste waarde
  92 gebruiken we de volgende functie:\\
  93 $$\mathcal{GRE} : Stack \rightarrow Stack$$\\
  94 Deze functie haalt de bovenste twee waarden van de stack en stopt een 1 bovenop
  95 de stack als de tweede bovenste waarde groter is dan de bovenste waarde. Anders
  96 word een 0 bovenop de stack gestopt.\\
  97
  98 roll functie (roll, r. 54):\\
  99 Om de stack te rollen gebruiken we de volgende functie:\\
 100 $$\mathcal{ROLL} : Stack \rightarrow Stack$$\\
 101 Deze functie haalt de bovenste twee elementen van de stack en stopt 1 bovenop
 102 de stack als het tweede bovenste element een hogere waarde heeft als dat van het
 103 bovenste element. Anders word 1 bovenop de stack gestopt.\\
 104
 105 out number (output stack) functie (outnum, r. 70):\\
 106 Deze functie past de output stack aan als er een integer naartoe geschreven word:\\
 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 word:\\
 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'\rangle}
 120 {\langle S_1 ;S_2, s\rangle \Rightarrow \langle S_1;S'_2, s'\rangle}\\
 121 {[comp^2_{sos}]}\qquad &
 122 \frac{\langle S_2, s\rangle \Rightarrow \langle s'\rangle}
 123 {\langle S_1 ;S_2, s\rangle \Rightarrow \langle S_1, 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