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 bij de eerste transitie de executie van S niet na een stap klaar is en waarbij
  19 de tweede transitie duidt op een terminerende transitie.\\
  20
  21 \subsection{Semantiekbeschrijving}
  22
  23 Om de semantiekregels te kunnen beschrijven maken we gebruik van hulpfuncties.
  24 Hieronder staat het type van de functies en een korte beschrijving.
  25 De implementatie is gedaan in de vorm van een functioneel programma in de taal \textit{Clean}.
  26 De implementatie van de functies staat in de appendix.
  27 Elke functie wordt op de volgende manier aangegeven: \textit{naam functie} (\textit{naam in appendix}, r. \textit{regelnummer in appendix})\\
  28
  29 delete functie (d, r. 5):\\
  30 Om het bovenste element van een stack weg te kunnen gooien gebruiken we de volgende
  31 functie:\\
  32 $$\mathcal{D} : Stack \rightarrow Stack$$
  33 Deze functie haalt het bovenste element van de stack en gooit dit weg.\\
  34
  35 extend functie (e, r. 9):\\
  36 Om een stack uit te kunnen breiden met een element gebruiken we de volgende
  37 functie:\\
  38 $$\mathcal{E} : \mathbb{Z}\rightarrow (Stack\rightarrow Stack)$$\\
  39 Deze functie neemt een integer en een stack en voegt de integer toe bovenop de
  40 stack.\\
  41
  42 add functie (add, r. 13):\\
  43 Om de bovenste twee elementen van een stack op te tellen gebruiken we de volgende
  44 functie:\\
  45 $$\mathcal{ADD} : Stack \rightarrow Stack$$
  46 Deze functie haalt de bovenste twee waarden van de stack, telt ze bij elkaar op, en legt
  47 het resultaat bovenop de stack.\\
  48
  49 subtract functie (sub, r. 18)\\
  50 Om de bovenste twee elementen van een stack van elkaar af te trekken gebruiken we
  51 de volgende functie:\\
  52 $$\mathcal{SUB} : Stack \rightarrow Stack$$
  53 Deze functie haalt de bovenste twee elementen van de stack, trekt de bovenste
  54 waarde van de tweede bovenste waarde af, en legt het resultaat bovenop de stack.\\
  55
  56 multiply functie (mul, r. 23):\\
  57 Om de bovenste twee elementen van een stack te vermenigvuldigen gebruiken we de
  58 volgende functie:\\
  59 $$\mathcal{MUL} : Stack \rightarrow Stack$$
  60 Deze functie haalt de bovenste twee elementen van de stack, vermenigvuldigt ze,
  61 en stopt het resultaat bovenop de stack.\\
  62
  63 division functie (div, r. 28):\\
  64 Om de geheeltallige deling van de bovenste twee elementen van de stack bovenop de
  65 stack te krijgen gebruiken we de volgende functie:\\
  66 $$\mathcal{DIV} : Stack \rightarrow Stack$$
  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 modulo functie (modc, r. 33):\\
  72 Om  de tweede bovenste waarde modulo de bovenste waarde te berekenen
  73 gebruiken we de volgende functie:\\
  74 $$\mathcal{MOD} : Stack \rightarrow Stack$$
  75 Deze functie haalt de bovenste twee elementen van de stack, berekent het
  76 resultaat van de tweede bovenste waarde modulo de bovenste waarde, en
  77 stopt dit bovenop de stack.\\
  78
  79 duplicate functie (dup, r. 38):\\
  80 Om het bovenste element van een stack te dupliceren gebruiken we de
  81 volgende functie:\\
  82 $$\mathcal{DUP} : Stack \rightarrow Stack$$
  83 Deze functie haalt de bovenste waarde van de stack en stopt een kopie
  84 en de bovenste waarde bovenop de stack.\\
  85
  86 not functie (notc, r. 42):\\
  87 Om te kijken of de bovenste waarde gelijk is aan 0 gebruiken we de
  88 volgende functie:\\
  89 $$\mathcal{NOT} : Stack \rightarrow Stack$$\\
  90 Deze functie neemt het bovenste element van de stack en stopt 0 bovenaan de
  91 stack als deze waarde niet gelijk is aan 0 en 1 als deze waarde gelijk is aan 0.\\
  92
  93 greater functie (gre, r. 47):\\
  94 Om te kijken of de tweede bovenste waarde groter is dan de bovenste waarde
  95 gebruiken we de volgende functie:\\
  96 $$\mathcal{GRE} : Stack \rightarrow Stack$$\\
  97 Deze functie haalt de bovenste twee waarden van de stack en stopt een 1 bovenop
  98 de stack als de tweede bovenste waarde groter is dan de bovenste waarde. Anders
  99 wordt een 0 bovenop de stack gestopt.\\
 100
 101 roll functie (roll, r. 54):\\
 102 Om de elementen op de stack te verschuiven gebruiken we de volgende functie:\\
 103 $$\mathcal{ROLL} : Stack \rightarrow Stack$$\\
 104 Deze functie haalt de bovenste twee elementen van de stack 'rolt' de rest van de stack tot een diepte die gelijk is aan de waarde van het tweede bovenste element. Een rol tot diepte \textit{n} verschuift de elementen 1 tot en met \textit{n} allemaal 1 plaats naar boven. Vervolgens wordt het eerste element van de stack op plaats \textit{n} neergelegd. Het aantal keren dat de stack gerold word is gelijk aan de waarde van het bovenste element. Als deze waarde negatief is word de stack in tegenovergestelde richting gerold. Dit houdt in dat bij elke rol het element op plaats \textit{n} bovenop de stack word gelegd, en de rest van de elementen (dat boven het element op plaats \textit{n} lagen) 1 plaats naar beneden wordt verschoven.\\
 105
 106 out number (output stack) functie (outnum, r. 70):\\
 107 Deze functie past de output stack aan als er een integer naartoe geschreven wordt:\\
 108 $$\mathcal{OUTN_{SO}} : Stack \rightarrow Stack$$\\
 109 Deze functie haalt het bovenste element van de stack en stopt dit element bovenop de output stack.\\
 110
 111 in number (stack) functie (innum, r. 75):\\
 112 Deze functie past de stack aan als er een integer naartoe geschreven wordt:\\
 113 $$\mathcal{INN_S} : Stack \rightarrow Stack$$\\
 114 Deze functie haalt het bovenste element van de input stack en stopt dit element bovenop de output stack.\\
 115
 116 Met behulp van deze gedefinieerde functies kunnen we nu de semantiekregels opstellen.
 117 De meeste regels spreken redelijk voor zich: als een commando wordt uitgevoerd, zorgt dit voor een verandering in de bijbehorende stack. Deze verandering komt tot stand door het toepassen van de bijbehorende hulpfunctie op deze stack.
 118
 119 Voor de semantiekregels voor de compositie halen we, in tegenstelling tot de normale gang van zaken bij sos, steeds een commando van het einde van de lijst af.
 120 Hiervoor is gekozen zodat de afleidingsrijen makkelijk te controleren zijn door bij de implementatie in \textit{Clean} de functies een voor een op een stack toe te passen.\\
 121
 122 \begin{alignat*}{2}
 123 {[comp^1_{sos}]}\qquad &
 124 \frac{\langle S_2, s\rangle \Rightarrow \langle S'_2, s_i', s_o', s'\rangle}
 125 {\langle S_1 ;S_2, s\rangle \Rightarrow \langle S_1;S'_2, s_i', s_o', s'\rangle}\\
 126 {[comp^2_{sos}]}\qquad &
 127 \frac{\langle S_2, s\rangle \Rightarrow \langle s_i', s_o', s'\rangle}
 128 {\langle S_1 ;S_2, s\rangle \Rightarrow \langle S_1, s_i', s_o', s'\rangle}\\
 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 &
 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 &
 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 {[pointer_{sos}]} \qquad &
 157 \langle pointer, s_i, s_o, s\rangle \Rightarrow
 158 \langle s_i, s_o, \mathcal{D}(s)\rangle\\
 159 {[switch_{sos}]} \qquad &
 160 \langle switch, s_i, s_o, s\rangle \Rightarrow
 161 \langle s_i, s_o, \mathcal{D}(s)\rangle\\
 162 {[push_{sos}]} \qquad &
 163 \langle push \: n, s_i, s_o, s\rangle \Rightarrow
 164 \langle s_i, s_o, \mathcal{E}(n,s)\rangle\\
 165 {[roll_{sos}]} \qquad &
 166 \langle roll, s_i, s_o, s\rangle \Rightarrow
 167 \langle s_i, s_o, \mathcal{ROLL}(s)\rangle\\
 168 {[innum_{sos}]} \qquad &
 169 \langle innum, s_i, s_o, s\rangle \Rightarrow
 170 \langle \mathcal{D}(s_i), s_o, \mathcal{INN_S}(s)\rangle\\
 171 {[outnum_{sos}]} \qquad &
 172 \langle outnum, s_i, s_o, s\rangle \Rightarrow
 173 \langle s_i, \mathcal{OUTN_{SO}}(s_o),\mathcal{D}(s)\rangle\\
 174 \end{alignat*}
 175