versie-0/semantics.tex

   1 Bij natuurlijke semantiek(ns) ligt de nadruk op de relatie tussen de begin en de eind state.
   2 Het nadeel hiervan is dat programma’s die niet termineren geen bewijsbomen hebben.
   3 Hierdoor is het niet mogelijk om eigenschappen te bewijzen voor zulke programma’s.
   4 Bij structurele operationele semantiek(sos) ligt de nadruk juist op de individuele stappen van de executie en heeft wel bewijsrijen voor programma’s die niet termineren.\\
   5 Om deze redenen hebben we gekozen voor sos.\\
   6 Een toestand in onze semantiek word beschreven door drie stacks; input, output en programma. Respectievelijk benoemen we deze met $s_i, s_o, s$ en beschrijven ze de STDIN, STDOUT en interne stack van het programma.
   7 Stacks worden gerepresenteerd als: $s=\{n_0, n_1, ..., n_n\}$ waarbij $n_i\in\mathbb{Z}$\\
   8 Het transitie systeem zal twee verschillende transities kennen, namelijk:\\
   9 $s\rightarrow \langle S, s_i, s_o, s\rangle$ en $s\rightarrow \langle s_i, s_o, s\rangle$\\
  10 Waarbij de laatste transitie duidt op een terminerende transitie en de eerste op een niet terminerende transitie.\\
  11 Bij de semantiek verwachten we nog een klein probleem dat te maken heeft met het feit dat we nog niet precies weten hoe we de righting van het programma en moeten implementeren, ook weten we nog niet of dit \"uberhaupt nodig is in de semantiekbeschrijving.