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 het bovenste element van een stack weg te kunnen gooien gebruiken we de volgende
  22 functie:\\
  23 $$\mathcal{D} : Stack \rightarrow Stack$$
  24 $$\mathcal{D} [\:] = [\:]$$
  25 $$\mathcal{D} [a:rest] = [rest] $$
  26 Deze functie haalt het bovenste element van de stack en gooit deze weg.\\
  27
  28 Om een stack uit te kunnen breiden met een element gebruiken we de volgende
  29 functie:\\
  30 $$\mathcal{E} : Stack\rightarrow (\mathbb{Z} \rightarrow Stack)$$\\
  31 Deze functie neemt een stack en een integer en voegt de integer toe bovenop de
  32 stack.\\
  33
  34 Om de bovenste twee elementen van een stack op te tellen gebruiken we de volgende
  35 functie:\\
  36 $$\mathcal{ADD} : Stack \rightarrow Stack$$
  37 $$\mathcal{ADD} [\:] = [\:]$$
  38 $$\mathcal{ADD} [a] = [a] $$
  39 $$\mathcal{ADD} [a:b:rest] = [b+a:rest] $$\\
  40 Deze functie haalt de bovenste twee waarden van de stack, telt ze bij elkaar op, en stopt
  41 het resultaat bovenop de stack.\\
  42
  43 Om de bovenste twee elementen van een stack van elkaar af te trekken gebruiken we
  44 de volgende functie:\\
  45 $$\mathcal{SUB} : Stack \rightarrow Stack$$
  46 $$\mathcal{SUB} [\:] = [\:]$$
  47 $$\mathcal{SUB} [a] = [a] $$
  48 $$\mathcal{SUB} [a:b:rest] = [b-a:rest] $$\\
  49 Deze functie haalt de bovenste twee elementen van de stack, trekt de bovenste
  50 waarde van de tweede bovenste waarde af, en stopt het resultaat bovenop de stack.
  51
  52 Om de bovenste twee elementen van een stack te vermenigvuldigen gebruiken we de
  53 volgende functie:\\
  54 $$\mathcal{MUL} : Stack \rightarrow Stack$$
  55 $$\mathcal{MUL} [\:] = [\:]$$
  56 $$\mathcal{MUL} [a] = [a] $$
  57 $$\mathcal{MUL} [a:b:rest] = [b*a:rest] $$\\
  58 Deze functie haalt de bovenste twee elementen van de stack, vermenigvuldigt ze,
  59 en stopt het resultaat bovenop de stack.\\
  60
  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 $$\mathcal{DIV} [\:] = [\:]$$
  65 $$\mathcal{DIV} [a] = [a] $$
  66 $$\mathcal{DIV} [a:b:rest] = [b/a:rest] $$\\
  67 Deze functie haalt de bovenste twee elementen van de stack, berekent de
  68 geheeltallige deling van de tweede bovenste waarde door de bovenste waarde,
  69 en stopt het resultaat bovenop de stack.\\
  70
  71 Om    gebruiken we de
  72 volgende functie:\\
  73 $$\mathcal{MOD} : Stack \rightarrow Stack$$
  74 $$\mathcal{MOD} [\:] = [\:]$$
  75 $$\mathcal{MOD} [a] = [a] $$
  76 $$\mathcal{MOD} [a:b:rest] = [b \: mod \: a:rest] $$\\
  77 Deze functie haalt de bovenste twee elementen van de stack, berekent het resultaat van de tweede bovenste
  78 waarde modulo de bovenste waarde, en stopt dit bovenop de stack.\\
  79
  80 Om het bovenste element van een stack te dupliceren gebruiken we de
  81 volgende functie:\\
  82 $$\mathcal{DUP} : Stack \rightarrow Stack$$
  83 $$\mathcal{DUP} [\:] = [\:]$$
  84 $$\mathcal{DUP} [a:rest] = [a:a:rest] $$\\
  85 Deze functie haalt stopt een kopie van de bovenste waarde bovenop de stack.\\
  86
  87 Om de   gebruiken we de
  88 volgende functie:\\
  89 $$\mathcal{NOT} : Stack \rightarrow Stack$$
  90 $$\mathcal{NOT} [\:] = [\:]$$
  91 $$\mathcal{NOT} [a:rest] = [0:rest] \: \text{if} \:  a \neq 0$$
  92 $$\mathcal{NOT} [a:rest] = [1:rest] \: \text{if} \: a = 0$$\\
  93 Deze functie neemt het bovenste element van de stack en stopt 0 bovenaan de
  94 stack als deze waarde niet gelijk is aan 0 en 1 als deze waarde gelijk is aan 0.\\
  95
  96 Om   gebruiken we de
  97 volgende functie:\\
  98 $$\mathcal{GRE} : Stack \rightarrow Stack$$
  99 $$\mathcal{GRE} [\:] = [\:]$$
 100 $$\mathcal{GRE} [a] = [a] $$
 101 $$\mathcal{GRE} [a:b:rest] = [0:rest] \: \text{if} \: a \geq b$$
 102 $$\mathcal{GRE} [a:b:rest] = [1:rest] \: \text{if} \: a < b$$\\
 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 Met behulp van deze gedefineerde functies kunnen we nu de volgende semantiekregels opstellen:\\
 108
 109 $
 110 {[pop_{sos}]}\qquad
 111 \langle pop, s_i, s_o, s\rangle \Rightarrow
 112 \langle s_i, s_o,\mathcal{D}(s)\rangle\\
 113 {[add_{sos}]}\qquad
 114 \langle add, s_i, s_o, s\rangle \Rightarrow
 115 \langle s_i, s_o, \mathcal{ADD}(s)\rangle\\
 116 {[subtract_{sos} ]}\qquad
 117 \langle subtract, s_i, s_o, s\rangle \Rightarrow
 118 \langle s_i, s_o, \mathcal{SUB}(s)\rangle\\
 119 {[multiply_{sos}]}\qquad
 120 \langle multiply, s_i, s_o, s\rangle \Rightarrow
 121 \langle s_i, s_o, \mathcal{MUL}(s)\rangle\\
 122 {[divide_{sos}]} \qquad
 123 \langle divide, s_i, s_o, s\rangle \Rightarrow
 124 \langle s_i, s_o, \mathcal{DIV}(s)\rangle\\
 125 {[mod_{sos}]} \qquad\qquad
 126 \langle mod, s_i, s_o, s\rangle \Rightarrow
 127 \langle s_i, s_o, \mathcal{MOD}(s)\rangle\\
 128 {[duplicate_{sos}]} \qquad
 129 \langle duplicate, s_i, s_o, s\rangle \Rightarrow
 130 \langle s_i, s_o, \mathcal{DUP}(s)\rangle\\
 131 {[not_{sos}]}\qquad\qquad
 132 \langle not, s_i, s_o, s\rangle \Rightarrow
 133 \langle s_i, s_o, \mathcal{NOT}(s)\rangle\\
 134 {[greater_{sos}]} \qquad
 135 \langle greater, s_i, s_o, s\rangle \Rightarrow
 136 \langle s_i, s_o, \mathcal{GRE}(s)\rangle\\
 137 {[push_{sos}]} \qquad
 138 \langle push, s_i, s_o, s\rangle \Rightarrow
 139 \langle s_i, s_o, s\rangle\\
 140 {[roll_{sos}]} \qquad
 141 \langle roll, s_i, s_o, s\rangle \Rightarrow
 142 \langle s_i, s_o, s\rangle\\
 143 {[inchar_{sos}]} \qquad
 144 \langle inchar, s_i, s_o, s\rangle \Rightarrow
 145 \langle s_i, s_o, s\rangle\\
 146 {[innum_{sos}]} \qquad
 147 \langle innum, s_i, s_o, s\rangle \Rightarrow
 148 \langle s_i, s_o, s\rangle\\
 149 {[outchar_{sos}]} \qquad
 150 \langle outchar, s_i, s_o, s\rangle \Rightarrow
 151 \langle s_i, s_o, s\rangle\\
 152 {[outnum_{sos}]} \qquad
 153 \langle outnum, s_i, s_o, s\rangle \Rightarrow
 154 \langle s_i, s_o, s\rangle\\
 155 $