versie-1/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 Om het eerste element van een stack weg te kunnen gooien gebruiken we de volgende functie:\\
  21 $$\mathcal{D} : s \rightarrow s$$\\
  22 Deze neemt een stack en gooit het bovenste element weg.\\
  23
  24 Om een stack uit te kunnen breiden met een element gebruiken we de volgende functie:\\
  25 $$\mathcal{E} : s, \mathbb{Z} \rightarrow s$$\\
  26 Deze functie neemt een stack en een integer en voegt de integer toe bovenop de stack.\\
  27
  28 \footnotesize
  29 $\infer [{[}delete_{sos}{]}]
  30                 {       \langle delete, s_i, s_o, s\rangle \Rightarrow
  31                                 \langle s_i,s_o,\mathcal{D}[s]\rangle}{}\\
  32 \infer  [{[}extend_{sos}{]}]
  33                 {       \langle extend \: z, s_i, s_o, s\rangle \Rightarrow
  34                                 \langle s_i, s_o,\mathcal{E}[s, z]\rangle}{}\\
  35 \infer  [{[}pop_{sos} {]}]
  36                 {       \langle delete, s_i, s_o, s\rangle \Rightarrow
  37                                 \langle s_i, s_o, s'\rangle}
  38                 {       \langle pop, s_i, s_o, s\rangle \Rightarrow
  39                                 \langle s_i, s_o, s'\rangle}\\
  40 \infer  [{[}add_{sos} {]}]
  41                 {       \langle delete, s_i, s_o, s\rangle \Rightarrow
  42                                 \langle s_i, s_o, s'\rangle \quad
  43                         \langle delete, s_i, s_o, s'\rangle \Rightarrow
  44                                 \langle s_i, s_o, s''\rangle \quad
  45                         \langle extend\: x+y, s_i, s_o, s''\rangle \Rightarrow
  46                                 \langle s_i, s_o, s'''\rangle}
  47                 {       \langle add \: x,y, s_i, s_o, s\rangle \Rightarrow
  48                                 \langle s_i, s_o, s'''\rangle}\\
  49 \infer  [{[}subtract_{sos} {]}]
  50                 {       \langle delete, s_i, s_o, s\rangle \Rightarrow
  51                                 \langle s_i, s_o, s'\rangle \quad
  52                         \langle delete, s_i, s_o, s'\rangle \Rightarrow
  53                                 \langle s_i, s_o, s''\rangle \quad
  54                         \langle extend\: x-y, s_i, s_o, s''\rangle \Rightarrow
  55                                 \langle s_i, s_o, s'''\rangle}
  56                 {       \langle subtract \: x,y, s_i, s_o, s\rangle \Rightarrow
  57                                 \langle s_i, s_o, s'''\rangle}\\
  58 \infer  [{[}multiply_{sos} {]}]
  59                 {       \langle delete, s_i, s_o, s\rangle \Rightarrow
  60                                 \langle s_i, s_o, s'\rangle \quad
  61                         \langle delete, s_i, s_o, s'\rangle \Rightarrow
  62                                 \langle s_i, s_o, s''\rangle \quad
  63                         \langle extend\: x*y, s_i, s_o, s''\rangle \Rightarrow
  64                                 \langle s_i, s_o, s'''\rangle}
  65                 {       \langle multiply \: x,y, s_i, s_o, s\rangle \Rightarrow
  66                                 \langle s_i, s_o, s'''\rangle}\\
  67 \infer  [{[}divide_{sos} {]}]
  68                 {       \langle delete, s_i, s_o, s\rangle \Rightarrow
  69                                 \langle s_i, s_o, s'\rangle \quad
  70                         \langle delete, s_i, s_o, s'\rangle \Rightarrow
  71                                 \langle s_i, s_o, s''\rangle \quad
  72                         \langle extend\: x/y, s_i, s_o, s''\rangle \Rightarrow
  73                                 \langle s_i, s_o, s'''\rangle}
  74                 {       \langle divide \: x,y, s_i, s_o, s\rangle \Rightarrow
  75                                 \langle s_i, s_o, s'''\rangle}\\
  76 \infer  [{[}mod_{sos} {]}]
  77                 {       \langle delete, s_i, s_o, s\rangle \Rightarrow
  78                                 \langle s_i, s_o, s'\rangle \quad
  79                         \langle delete, s_i, s_o, s'\rangle \Rightarrow
  80                                 \langle s_i, s_o, s''\rangle \quad
  81                         \langle extend\: x \: mod \: y, s_i, s_o, s''\rangle \Rightarrow
  82                                 \langle s_i, s_o, s'''\rangle}
  83                 {       \langle mod \: x,y, s_i, s_o, s\rangle \Rightarrow
  84                                 \langle s_i, s_o, s'''\rangle}\\
  85 \infer  [{[}duplicate_{sos} {]}]
  86                 {       \langle extend\: x, s_i, s_o, s\rangle \Rightarrow
  87                         \langle s_i, s_o, s'\rangle}
  88                 {       \langle duplicate \: x, s_i, s_o, s\rangle \Rightarrow
  89                                 \langle s_i, s_o, s'\rangle}\\
  90 \infer  [{[}not^0_{sos} {]}]
  91                 {       \langle delete, s_i, s_o, s\rangle \Rightarrow
  92                                 \langle s_i, s_o, s'\rangle \quad
  93                         \langle extend\: 1, s_i, s_o, s'\rangle \Rightarrow
  94                                 \langle s_i, s_o, s''\rangle}
  95                 {       \langle not \: x, s_i, s_o, s\rangle \Rightarrow
  96                                 \langle s_i, s_o, s''\rangle}$ if $x = 0\\
  97 \infer  [{[}not^*_{sos} {]}]
  98                 {       \langle delete, s_i, s_o, s\rangle \Rightarrow
  99                                 \langle s_i, s_o, s'\rangle \quad
 100                         \langle extend\: 0, s_i, s_o, s'\rangle \Rightarrow
 101                                 \langle s_i, s_o, s''\rangle}
 102                 {       \langle not \: x, s_i, s_o, s\rangle \Rightarrow
 103                                 \langle s_i, s_o, s''\rangle}$ if $x\neq 0\\
 104 \infer  [{[}greater^<_{sos} {]}]
 105                 {       \langle delete, s_i, s_o, s\rangle \Rightarrow
 106                                 \langle s_i, s_o, s'\rangle \quad
 107                         \langle delete, s_i, s_o, s'\rangle \Rightarrow
 108                                 \langle s_i, s_o, s''\rangle \quad
 109                         \langle extend\:,1, s_i, s_o, s''\rangle \Rightarrow
 110                                 \langle s_i, s_o, s'''\rangle}
 111                 {       \langle greater \: x,y, s_i, s_o, s\rangle \Rightarrow
 112                         \langle s_i, s_o, s'''\rangle}$ if $x>y\\
 113 \infer  [{[}greater^>_{sos} {]}]
 114                 {       \langle delete, s_i, s_o, s\rangle \Rightarrow
 115                                 \langle s_i, s_o, s'\rangle \quad
 116                         \langle delete, s_i, s_o, s'\rangle \Rightarrow
 117                                 \langle s_i, s_o, s''\rangle \quad
 118                         \langle extend\: 0, s_i, s_o, s''\rangle \Rightarrow
 119                                 \langle s_i, s_o, s'''\rangle}
 120                 {       \langle greater \: x,y, s_i, s_o, s\rangle \Rightarrow
 121                                 \langle s_i, s_o, s'''\rangle}$ if $x<y
 122 $
 123 \normalsize