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} [0:rest] = [1:rest]$$
  92 $$\mathcal{NOT} [\_:rest] = [0:rest] $$\\
  93
  94 Deze functie neemt het bovenste element van de stack en stopt 0 bovenaan de
  95 stack als deze waarde niet gelijk is aan 0 en 1 als deze waarde gelijk is aan 0.\\
  96
  97 Om   gebruiken we de
  98 volgende functie:\\
  99 $$\mathcal{GRE} : Stack \rightarrow Stack$$
 100 $$\mathcal{GRE} [\:] = [\:]$$
 101 $$\mathcal{GRE} [a] = [a] $$
 102 $$\mathcal{GRE} [a:b:rest]$$
 103 $$\qquad \qquad | \: a \geq b =  [0:rest]$$
 104 $$\qquad \qquad | \: a < b =  [1:rest]$$\\
 105
 106 $$\mathcal{ROLL} : Stack \rightarrow Stack$$
 107 $$\mathcal{ROLL} [\:] = [\:]$$
 108 $$\mathcal{ROLL} [a] = [a] $$
 109 $$\mathcal{ROLL} [a:b:rest]$$
 110 $$\qquad \qquad | modulo \: a \: b == 0 = rest$$
 111 $$\qquad \qquad | b <= 0 = rest$$
 112 $$\qquad \qquad | b > length rest = rest$$
 113 $$\qquad \qquad | a == 1 = roll1 [b:rest]$$
 114 $$\qquad \qquad | a > 0 = roll([a-1] ++ [b] ++ roll1 [b:rest]$$
 115 $$\qquad \qquad | a < 0 = roll(modulo \: a \: b] ++ [b:rest])$$
 116
 117 $$\mathcal{ROLL}1 : Stack \rightarrow Stack$$
 118 $$\mathcal{ROLL}1 [1:rest] = [rest]$$
 119 $$\mathcal{ROLL}1 [b:c:d:rest] = [d] ++ \mathcal{ROLL}1 [b-1:c:rest]$$
 120
 121
 122 Deze functie haalt de bovenste twee elementen van de stack en stopt 1 bovenop
 123 de stack als het tweede bovenste element een hogere waarde heeft als dat van het
 124 bovenste element. Anders word 1 bovenop de stack gestopt.\\
 125
 126 Met behulp van deze gedefinieerde functies kunnen we nu de volgende semantiekregels opstellen:\\
 127
 128 $
 129 {[pop_{sos}]}\qquad
 130 \langle pop, s_i, s_o, s\rangle \Rightarrow
 131 \langle s_i, s_o,\mathcal{D}(s)\rangle\\
 132 {[add_{sos}]}\qquad
 133 \langle add, s_i, s_o, s\rangle \Rightarrow
 134 \langle s_i, s_o, \mathcal{ADD}(s)\rangle\\
 135 {[subtract_{sos} ]}\qquad
 136 \langle subtract, s_i, s_o, s\rangle \Rightarrow
 137 \langle s_i, s_o, \mathcal{SUB}(s)\rangle\\
 138 {[multiply_{sos}]}\qquad
 139 \langle multiply, s_i, s_o, s\rangle \Rightarrow
 140 \langle s_i, s_o, \mathcal{MUL}(s)\rangle\\
 141 {[divide_{sos}]} \qquad
 142 \langle divide, s_i, s_o, s\rangle \Rightarrow
 143 \langle s_i, s_o, \mathcal{DIV}(s)\rangle\\
 144 {[mod_{sos}]} \qquad\qquad
 145 \langle mod, s_i, s_o, s\rangle \Rightarrow
 146 \langle s_i, s_o, \mathcal{MOD}(s)\rangle\\
 147 {[duplicate_{sos}]} \qquad
 148 \langle duplicate, s_i, s_o, s\rangle \Rightarrow
 149 \langle s_i, s_o, \mathcal{DUP}(s)\rangle\\
 150 {[not_{sos}]}\qquad\qquad
 151 \langle not, s_i, s_o, s\rangle \Rightarrow
 152 \langle s_i, s_o, \mathcal{NOT}(s)\rangle\\
 153 {[greater_{sos}]} \qquad
 154 \langle greater, s_i, s_o, s\rangle \Rightarrow
 155 \langle s_i, s_o, \mathcal{GRE}(s)\rangle\\
 156 {[push_{sos}]} \qquad
 157 \langle push \: n, s_i, s_o, s\rangle \Rightarrow
 158 \langle s_i, s_o, \mathcal{E}(n,s)\rangle\\
 159 {[roll_{sos}]} \qquad
 160 \langle roll, s_i, s_o, s\rangle \Rightarrow
 161 \langle s_i, s_o, \mathcal{ROLL}(s)\rangle\\
 162 {[inchar_{sos}]} \qquad
 163 \langle inchar, s_i, s_o, s\rangle \Rightarrow
 164 \langle s_i, s_o, s\rangle\\
 165 {[innum_{sos}]} \qquad
 166 \langle innum, s_i, s_o, s\rangle \Rightarrow
 167 \langle s_i, s_o, s\rangle\\
 168 {[outchar_{sos}]} \qquad
 169 \langle outchar, s_i, s_o, s\rangle \Rightarrow
 170 \langle s_i, s_o, s\rangle\\
 171 {[outnum_{sos}]} \qquad
 172 \langle outnum, s_i, s_o, s\rangle \Rightarrow
 173 \langle s_i, s_o, s\rangle\\
 174 $