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 \subsection{Semantiekbeschrijving}
  20
  21 Om de semantiekregels te kunnen beschrijven maken we gebruik van hulpfuncties. Hieronder staat het type van de functies en een korte beschrijving.
  22 De implementatie van deze functies staat in de appendix bij het aangegeven regelnummer.\\
  23
  24 delete functie (d, r. 5):\\
  25 Om het bovenste element van een stack weg te kunnen gooien gebruiken we de volgende
  26 functie:\\
  27 $$\mathcal{D} : Stack \rightarrow Stack$$
  28 Deze functie haalt het bovenste element van de stack en gooit deze weg.\\
  29
  30 extend functie (e, r. 9):\\
  31 Om een stack uit te kunnen breiden met een element gebruiken we de volgende
  32 functie:\\
  33 $$\mathcal{E} : Stack\rightarrow (\mathbb{Z} \rightarrow Stack)$$\\
  34 Deze functie neemt een stack en een integer en voegt de integer toe bovenop de
  35 stack.\\
  36
  37 add functie (add, r. 13):\\
  38 Om de bovenste twee elementen van een stack op te tellen gebruiken we de volgende
  39 functie:\\
  40 $$\mathcal{ADD} : Stack \rightarrow Stack$$
  41 Deze functie haalt de bovenste twee waarden van de stack, telt ze bij elkaar op, en stopt
  42 het resultaat bovenop de stack.\\
  43
  44 subtract functie (sub, r. 18)\\
  45 Om de bovenste twee elementen van een stack van elkaar af te trekken gebruiken we
  46 de volgende functie:\\
  47 $$\mathcal{SUB} : Stack \rightarrow Stack$$
  48 Deze functie haalt de bovenste twee elementen van de stack, trekt de bovenste
  49 waarde van de tweede bovenste waarde af, en stopt het resultaat bovenop de stack.\\
  50
  51 multiply functie (mul, r. 23):\\
  52 Om de bovenste twee elementen van een stack te vermenigvuldigen gebruiken we de
  53 volgende functie:\\
  54 $$\mathcal{MUL} : Stack \rightarrow Stack$$
  55 Deze functie haalt de bovenste twee elementen van de stack, vermenigvuldigt ze,
  56 en stopt het resultaat bovenop de stack.\\
  57
  58 division functie (div, r. 28):\\
  59 Om de geheeltallige deling van de bovenste twee elementen van de stack bovenop de
  60 stack te krijgen gebruiken we de volgende functie:\\
  61 $$\mathcal{DIV} : Stack \rightarrow Stack$$
  62 Deze functie haalt de bovenste twee elementen van de stack, berekent de
  63 geheeltallige deling van de tweede bovenste waarde door de bovenste waarde,
  64 en stopt het resultaat bovenop de stack.\\
  65
  66 modulo functie (modc, r. 33):\\
  67 Om  de tweede bovenste waarde modulo de bovenste waarde te berekenen
  68 gebruiken we de volgende functie:\\
  69 $$\mathcal{MOD} : Stack \rightarrow Stack$$
  70 Deze functie haalt de bovenste twee elementen van de stack, berekent het
  71 resultaat van de tweede bovenste waarde modulo de bovenste waarde, en
  72 stopt dit bovenop de stack.\\
  73
  74 duplicate functie (dup, r. 38):\\
  75 Om het bovenste element van een stack te dupliceren gebruiken we de
  76 volgende functie:\\
  77 $$\mathcal{DUP} : Stack \rightarrow Stack$$
  78 Deze functie haalt de bovenste waarde van de stack en stopt een kopie
  79 en de bovenste waarde bovenop de stack.\\
  80
  81 not functie (notc, r. 42):\\
  82 Om de not van de bovenste waarde te berekenen gebruiken we de
  83 volgende functie:\\
  84 $$\mathcal{NOT} : Stack \rightarrow Stack$$\\
  85 Deze functie neemt het bovenste element van de stack en stopt 0 bovenaan de
  86 stack als deze waarde niet gelijk is aan 0 en 1 als deze waarde gelijk is aan 0.\\
  87
  88 greater functie (gre, r. 47):\\
  89 Om kijken of de tweede bovenste waarde groter is dan de bovenste waarde
  90 gebruiken we de volgende functie:\\
  91 $$\mathcal{GRE} : Stack \rightarrow Stack$$\\
  92 Deze functie haalt de bovenste twee waarden van de stack en stopt een 1 bovenop
  93 de stack als de tweede bovenste waarde groter is dan de bovenste waarde. Anders
  94 word een 0 bovenop de stack gestopt.\\
  95
  96 roll functie (roll, r. 54):\\
  97 Om de stack te rollen gebruiken we de volgende functie:\\
  98 $$\mathcal{ROLL} : Stack \rightarrow Stack$$\\
  99 Deze functie haalt de bovenste twee elementen van de stack en stopt 1 bovenop
 100 de stack als het tweede bovenste element een hogere waarde heeft als dat van het
 101 bovenste element. Anders word 1 bovenop de stack gestopt.\\
 102
 103 pointer functie (pointer, r. 65):\\
 104
 105 out number functie (outnum, r. 74):\\
 106
 107 in number functie (innum, r. 83):\\
 108
 109
 110
 111
 112
 113 (switch, outchar, inchar)\\
 114
 115
 116 Met behulp van deze gedefinieerde functies kunnen we nu de volgende semantiekregels opstellen:\\
 117
 118
 119
 120 \begin{alignat*}{2}
 121 {[pop_{sos}]}\qquad &
 122 \langle pop, s_i, s_o, s\rangle \Rightarrow
 123 \langle s_i, s_o,\mathcal{D}(s)\rangle\\
 124 {[add_{sos}]}\qquad
 125 &\langle add, s_i, s_o, s\rangle \Rightarrow
 126 \langle s_i, s_o, \mathcal{ADD}(s)\rangle\\
 127 {[subtract_{sos} ]}\qquad &
 128 \langle subtract, s_i, s_o, s\rangle \Rightarrow
 129 \langle s_i, s_o, \mathcal{SUB}(s)\rangle\\
 130 {[multiply_{sos}]}\qquad &
 131 \langle multiply, s_i, s_o, s\rangle \Rightarrow
 132 \langle s_i, s_o, \mathcal{MUL}(s)\rangle\\
 133 {[divide_{sos}]} \qquad &
 134 \langle divide, s_i, s_o, s\rangle \Rightarrow
 135 \langle s_i, s_o, \mathcal{DIV}(s)\rangle\\
 136 {[mod_{sos}]} \qquad &
 137 \langle mod, s_i, s_o, s\rangle \Rightarrow
 138 \langle s_i, s_o, \mathcal{MOD}(s)\rangle\\
 139 {[duplicate_{sos}]} \qquad &
 140 \langle duplicate, s_i, s_o, s\rangle \Rightarrow
 141 \langle s_i, s_o, \mathcal{DUP}(s)\rangle\\
 142 {[not_{sos}]} \qquad &
 143 \langle not, s_i, s_o, s\rangle \Rightarrow
 144 \langle s_i, s_o, \mathcal{NOT}(s)\rangle\\
 145 {[greater_{sos}]} \qquad &
 146 \langle greater, s_i, s_o, s\rangle \Rightarrow
 147 \langle s_i, s_o, \mathcal{GRE}(s)\rangle\\
 148 {[pointer_{sos}]} \qquad &
 149 \langle pointer, s_i, s_o, s\rangle \Rightarrow
 150 \langle s_i, s_o, \mathcal{D}(s)\rangle\\
 151 {[push_{sos}]} \qquad &
 152 \langle push \: n, s_i, s_o, s\rangle \Rightarrow
 153 \langle s_i, s_o, \mathcal{E}(n,s)\rangle\\
 154 {[roll_{sos}]} \qquad &
 155 \langle roll, s_i, s_o, s\rangle \Rightarrow
 156 \langle s_i, s_o, \mathcal{ROLL}(s)\rangle\\
 157 {[innum_{sos}]} \qquad &
 158 \langle innum, s_i, s_o, s\rangle \Rightarrow
 159 \langle \mathcal{INN_{SI}}(s_i), s_o, \mathcal{INN_S}(s)\rangle\\
 160 {[outnum_{sos}]} \qquad &
 161 \langle outnum, s_i, s_o, s\rangle \Rightarrow
 162 \langle s_i, \mathcal{OUTN_{SO}}(s_o),\mathcal{OUTN_S}(s)\rangle\\
 163 {[inchar_{sos}]} \qquad &
 164 \langle inchar, s_i, s_o, s\rangle \Rightarrow
 165 \langle s_i, s_o, s\rangle\\
 166 {[outchar_{sos}]} \qquad &
 167 \langle outchar, s_i, s_o, s\rangle \Rightarrow
 168 \langle s_i, s_o, s\rangle\\
 169 {[switch_{sos}]} \qquad &
 170 \langle switch, s_i, s_o, s\rangle \Rightarrow
 171 \langle s_i, s_o, s\rangle\\
 172 \end{alignat*}
 173