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 bij het aangegeven 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 deze 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 stack en een integer 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 stopt
  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 stopt 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 de not van de bovenste waarde te berekenen 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 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 word een 0 bovenop de stack gestopt.\\
  99
 100 roll functie (roll, r. 54):\\
 101 Om de stack te rollen gebruiken we de volgende functie:\\
 102 $$\mathcal{ROLL} : Stack \rightarrow Stack$$\\
 103 Deze functie haalt de bovenste twee elementen van de stack en stopt 1 bovenop
 104 de stack als het tweede bovenste element een hogere waarde heeft als dat van het
 105 bovenste element. Anders word 1 bovenop de stack gestopt.\\
 106
 107 out number (output stack) functie (outnum, r. 70):\\
 108 Deze functie past de output stack aan als er een integer naartoe geschreven word:\\
 109 $$\mathcal{OUTN_{SO}} : Stack \rightarrow Stack$$\\
 110 Deze functie haalt het bovenste element van de stack en stopt dit element bovenop de output stack.\\
 111
 112 in number (stack) functie (innum, r. 75):\\
 113 Deze functie past de stack aan als er een integer naartoe geschreven word:\\
 114 $$\mathcal{INN_S} : Stack \rightarrow Stack$$\\
 115 Deze functie haalt het bovenste element van de input stack en stopt dit element bovenop de output stack.\\
 116
 117 Met behulp van deze gedefinieerde functies kunnen we nu de volgende semantiekregels opstellen:\\
 118
 119 \begin{alignat*}{2}
 120 {[comp^1_{sos}]}\qquad &
 121 \frac{\langle S_2, s\rangle \Rightarrow \langle S'_2, s'\rangle}
 122 {\langle S_1 ;S_2, s\rangle \Rightarrow \langle S_1;S'_2, s'\rangle}\\
 123 {[comp^2_{sos}]}\qquad &
 124 \frac{\langle S_2, s\rangle \Rightarrow \langle s'\rangle}
 125 {\langle S_1 ;S_2, s\rangle \Rightarrow \langle S_1, s'\rangle}\\
 126 {[pop_{sos}]}\qquad &
 127 \langle pop, s_i, s_o, s\rangle \Rightarrow
 128 \langle s_i, s_o,\mathcal{D}(s)\rangle\\
 129 {[add_{sos}]}\qquad
 130 &\langle add, s_i, s_o, s\rangle \Rightarrow
 131 \langle s_i, s_o, \mathcal{ADD}(s)\rangle\\
 132 {[subtract_{sos} ]}\qquad &
 133 \langle subtract, s_i, s_o, s\rangle \Rightarrow
 134 \langle s_i, s_o, \mathcal{SUB}(s)\rangle\\
 135 {[multiply_{sos}]}\qquad &
 136 \langle multiply, s_i, s_o, s\rangle \Rightarrow
 137 \langle s_i, s_o, \mathcal{MUL}(s)\rangle\\
 138 {[divide_{sos}]} \qquad &
 139 \langle divide, s_i, s_o, s\rangle \Rightarrow
 140 \langle s_i, s_o, \mathcal{DIV}(s)\rangle\\
 141 {[mod_{sos}]} \qquad &
 142 \langle mod, s_i, s_o, s\rangle \Rightarrow
 143 \langle s_i, s_o, \mathcal{MOD}(s)\rangle\\
 144 {[duplicate_{sos}]} \qquad &
 145 \langle duplicate, s_i, s_o, s\rangle \Rightarrow
 146 \langle s_i, s_o, \mathcal{DUP}(s)\rangle\\
 147 {[not_{sos}]} \qquad &
 148 \langle not, s_i, s_o, s\rangle \Rightarrow
 149 \langle s_i, s_o, \mathcal{NOT}(s)\rangle\\
 150 {[greater_{sos}]} \qquad &
 151 \langle greater, s_i, s_o, s\rangle \Rightarrow
 152 \langle s_i, s_o, \mathcal{GRE}(s)\rangle\\
 153 {[pointer_{sos}]} \qquad &
 154 \langle pointer, s_i, s_o, s\rangle \Rightarrow
 155 \langle s_i, s_o, \mathcal{D}(s)\rangle\\
 156 {[switch_{sos}]} \qquad &
 157 \langle switch, s_i, s_o, s\rangle \Rightarrow
 158 \langle s_i, s_o, \mathcal{D}(s)\rangle\\
 159 {[push_{sos}]} \qquad &
 160 \langle push \: n, s_i, s_o, s\rangle \Rightarrow
 161 \langle s_i, s_o, \mathcal{E}(n,s)\rangle\\
 162 {[roll_{sos}]} \qquad &
 163 \langle roll, s_i, s_o, s\rangle \Rightarrow
 164 \langle s_i, s_o, \mathcal{ROLL}(s)\rangle\\
 165 {[innum_{sos}]} \qquad &
 166 \langle innum, s_i, s_o, s\rangle \Rightarrow
 167 \langle \mathcal{D}(s_i), s_o, \mathcal{INN_S}(s)\rangle\\
 168 {[outnum_{sos}]} \qquad &
 169 \langle outnum, s_i, s_o, s\rangle \Rightarrow
 170 \langle s_i, \mathcal{OUTN_{SO}}(s_o),\mathcal{D}(s)\rangle\\
 171 \end{alignat*}
 172