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{Semantiek beschrijving}
  20
  21 Om het eerste element van een stack weg te kunnen gooien gebruiken we de volgende
  22 functie:\\
  23 $$\mathcal{D} : s \rightarrow s$$\\
  24 Deze neemt een stack en gooit het bovenste element weg.\\
  25
  26 Om een stack uit te kunnen breiden met een element gebruiken we de volgende
  27 functie:\\
  28 $$\mathcal{E} : s, \mathbb{Z} \rightarrow s$$\\
  29 Deze functie neemt een stack en een integer en voegt de integer toe bovenop de
  30 stack.\\
  31
  32 Om de bovenste twee elementen van een stack op te tellen gebruiken we de volgende
  33 functie:\\
  34 $$\mathcal{ADD} : Stack \rightarrow Stack$$
  35 $$\mathcal{ADD} [\:] = [\:]$$
  36 $$\mathcal{ADD} [a] = [a] $$
  37 $$\mathcal{ADD} [a:b:rest] = [b+a:rest] $$\\
  38
  39 Om de bovenste twee elementen van een stack van elkaar af te trekken gebruiken we
  40 de volgende functie:\\
  41 $$\mathcal{SUB} : Stack \rightarrow Stack$$
  42 $$\mathcal{SUB} [\:] = [\:]$$
  43 $$\mathcal{SUB} [a] = [a] $$
  44 $$\mathcal{SUB} [a:b:rest] = [b-a:rest] $$\\
  45
  46 Om de bovenste twee elementen van een stack te vermenigvuldigen gebruiken we de
  47 volgende functie:\\
  48 $$\mathcal{MUL} : Stack \rightarrow Stack$$
  49 $$\mathcal{MUL} [\:] = [\:]$$
  50 $$\mathcal{MUL} [a] = [a] $$
  51 $$\mathcal{MUL} [a:b:rest] = [b*a:rest] $$\\
  52
  53 Om de integer deling van de bovenste twee elementen van de stack bovenop de
  54 stack te krijgen gebruiken we de volgende functie:\\
  55 $$\mathcal{DIV} : Stack \rightarrow Stack$$
  56 $$\mathcal{DIV} [\:] = [\:]$$
  57 $$\mathcal{DIV} [a] = [a] $$
  58 $$\mathcal{DIV} [a:b:rest] = [b/a:rest] $$\\
  59
  60 Om de bovenste twee elementen van een stack op te tellen gebruiken we de
  61 volgende functie:\\
  62 $$\mathcal{MOD} : Stack \rightarrow Stack$$
  63 $$\mathcal{MOD} [\:] = [\:]$$
  64 $$\mathcal{MOD} [a] = [a] $$
  65 $$\mathcal{MOD} [a:b:rest] = [b \: mod \: a:rest] $$\\
  66
  67 Om het bovenste element van een stack te dupliceren gebruiken we de
  68 volgende functie:\\
  69 $$\mathcal{DUP} : Stack \rightarrow Stack$$
  70 $$\mathcal{DUP} [\:] = [\:]$$
  71 $$\mathcal{DUP} [a:rest] = [a:a:rest] $$\\
  72
  73 Om de bovenste twee elementen van een stack op te tellen gebruiken we de
  74 volgende functie:\\
  75 $$\mathcal{NOT} : Stack \rightarrow Stack$$
  76 $$\mathcal{NOT} [\:] = [\:]$$
  77 $$\mathcal{NOT} [a:rest] = [0:rest] \: \text{if} \:  a \neq 0$$
  78 $$\mathcal{NOT} [a:rest] = [1:rest] \: \text{if} \: a = 0$$\\
  79
  80 Om de bovenste twee elementen van een stack op te tellen gebruiken we de
  81 volgende functie:\\
  82 $$\mathcal{GRE} : Stack \rightarrow Stack$$
  83 $$\mathcal{GRE} [\:] = [\:]$$
  84 $$\mathcal{GRE} [a] = [a] $$
  85 $$\mathcal{GRE} [a:b:rest] = [0:rest] \: \text{if} \: a \geq b$$
  86 $$\mathcal{GRE} [a:b:rest] = [1:rest] \: \text{if} \: a < b$$\\
  87
  88 Met behulp van deze gedefineerde functies kunnen we nu de volgende semantiekregels opstellen:\\
  89
  90 $
  91 {[pop_{sos}]}\qquad
  92 \langle pop, s_i, s_o, s\rangle \Rightarrow
  93 \langle s_i, s_o,\mathcal{D}(s)\rangle\\
  94 {[add_{sos}]}\qquad
  95 \langle add, s_i, s_o, s\rangle \Rightarrow
  96 \langle s_i, s_o, \mathcal{ADD}(s)\rangle\\
  97 {[subtract_{sos} ]}\qquad
  98 \langle subtract, s_i, s_o, s\rangle \Rightarrow
  99 \langle s_i, s_o, \mathcal{SUB}(s)\rangle\\
 100 {[multiply_{sos}]}\qquad
 101 \langle multiply, s_i, s_o, s\rangle \Rightarrow
 102 \langle s_i, s_o, \mathcal{MUL}(s)\rangle\\
 103 {[divide_{sos}]} \qquad
 104 \langle divide, s_i, s_o, s\rangle \Rightarrow
 105 \langle s_i, s_o, \mathcal{DIV}(s)\rangle\\
 106 {[mod_{sos}]} \qquad\qquad
 107 \langle mod, s_i, s_o, s\rangle \Rightarrow
 108 \langle s_i, s_o, \mathcal{MOD}(s)\rangle\\
 109 {[duplicate_{sos}]} \qquad
 110 \langle duplicate, s_i, s_o, s\rangle \Rightarrow
 111 \langle s_i, s_o, \mathcal{DUP}(s)\rangle\\
 112 {[not_{sos}]}\qquad\qquad
 113 \langle not, s_i, s_o, s\rangle \Rightarrow
 114 \langle s_i, s_o, \mathcal{NOT}(s)\rangle\\
 115 {[greater_{sos}]} \qquad
 116 \langle greater, s_i, s_o, s\rangle \Rightarrow
 117 \langle s_i, s_o, \mathcal{GRE}(s)\rangle \qquad \\
 118 $