X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=versie-1%2Fsemantics.tex;fp=versie-1%2Fsemantics.tex;h=fb4c747519ebff4e48ade7d171011b761be35c41;hb=4272348e58a32a4433614c55ea9ef650fe7b4f60;hp=0000000000000000000000000000000000000000;hpb=3c6cc0ecaf6173ed11e218bb96fa4ab52bc22233;p=sec1415.git diff --git a/versie-1/semantics.tex b/versie-1/semantics.tex new file mode 100644 index 0000000..fb4c747 --- /dev/null +++ b/versie-1/semantics.tex @@ -0,0 +1,123 @@ +\subsection{Structurele operationele semantiek} +Bij natuurlijke semantiek(ns) ligt de nadruk op de relatie tussen de begin en +de eind state. Het nadeel hiervan is dat programma’s die niet termineren geen +bewijsbomen hebben. Hierdoor is het niet mogelijk om eigenschappen te bewijzen +voor zulke programma’s. Bij structurele operationele semantiek(sos) ligt de +nadruk juist op de individuele stappen van de executie en zijn er w\'el +bewijsrijen voor programma’s die niet termineren.\\ +Om deze redenen hebben we gekozen voor sos.\\ +Een toestand in onze semantiek wordt 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. Stacks worden +gerepresenteerd als: $s=[e_0, e_1, \dots, e_n]$ waarbij $e_i\in\mathbb{Z}$\\ +Het transitie systeem zal twee verschillende transities kennen, namelijk:\\ +$\langle S, s_i, s_o, s\rangle\Rightarrow\langle S', s_i', s_o', s'\rangle$ en\\ +$\langle S, s_i, s_o, s\rangle\Rightarrow\langle s_i', s_o', s'\rangle$\\ +Waarbij de laatste transitie duidt op een terminerende transitie en de eerste +op een niet terminerende transitie.\\ + +\subsection{Semantiek beschrijving} +Om het eerste element van een stack weg te kunnen gooien gebruiken we de volgende functie:\\ +$$\mathcal{D} : s \rightarrow s$$\\ +Deze neemt een stack en gooit het bovenste element weg.\\ + +Om een stack uit te kunnen breiden met een element gebruiken we de volgende functie:\\ +$$\mathcal{E} : s, \mathbb{Z} \rightarrow s$$\\ +Deze functie neemt een stack en een integer en voegt de integer toe bovenop de stack.\\ + +\footnotesize +$\infer [{[}delete_{sos}{]}] + { \langle delete, s_i, s_o, s\rangle \Rightarrow + \langle s_i,s_o,\mathcal{D}[s]\rangle}{}\\ +\infer [{[}extend_{sos}{]}] + { \langle extend \: z, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o,\mathcal{E}[s, z]\rangle}{}\\ +\infer [{[}pop_{sos} {]}] + { \langle delete, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'\rangle} + { \langle pop, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'\rangle}\\ +\infer [{[}add_{sos} {]}] + { \langle delete, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'\rangle \quad + \langle delete, s_i, s_o, s'\rangle \Rightarrow + \langle s_i, s_o, s''\rangle \quad + \langle extend\: x+y, s_i, s_o, s''\rangle \Rightarrow + \langle s_i, s_o, s'''\rangle} + { \langle add \: x,y, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'''\rangle}\\ +\infer [{[}subtract_{sos} {]}] + { \langle delete, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'\rangle \quad + \langle delete, s_i, s_o, s'\rangle \Rightarrow + \langle s_i, s_o, s''\rangle \quad + \langle extend\: x-y, s_i, s_o, s''\rangle \Rightarrow + \langle s_i, s_o, s'''\rangle} + { \langle subtract \: x,y, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'''\rangle}\\ +\infer [{[}multiply_{sos} {]}] + { \langle delete, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'\rangle \quad + \langle delete, s_i, s_o, s'\rangle \Rightarrow + \langle s_i, s_o, s''\rangle \quad + \langle extend\: x*y, s_i, s_o, s''\rangle \Rightarrow + \langle s_i, s_o, s'''\rangle} + { \langle multiply \: x,y, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'''\rangle}\\ +\infer [{[}divide_{sos} {]}] + { \langle delete, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'\rangle \quad + \langle delete, s_i, s_o, s'\rangle \Rightarrow + \langle s_i, s_o, s''\rangle \quad + \langle extend\: x/y, s_i, s_o, s''\rangle \Rightarrow + \langle s_i, s_o, s'''\rangle} + { \langle divide \: x,y, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'''\rangle}\\ +\infer [{[}mod_{sos} {]}] + { \langle delete, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'\rangle \quad + \langle delete, s_i, s_o, s'\rangle \Rightarrow + \langle s_i, s_o, s''\rangle \quad + \langle extend\: x \: mod \: y, s_i, s_o, s''\rangle \Rightarrow + \langle s_i, s_o, s'''\rangle} + { \langle mod \: x,y, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'''\rangle}\\ +\infer [{[}duplicate_{sos} {]}] + { \langle extend\: x, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'\rangle} + { \langle duplicate \: x, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'\rangle}\\ +\infer [{[}not^0_{sos} {]}] + { \langle delete, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'\rangle \quad + \langle extend\: 1, s_i, s_o, s'\rangle \Rightarrow + \langle s_i, s_o, s''\rangle} + { \langle not \: x, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s''\rangle}$ if $x = 0\\ +\infer [{[}not^*_{sos} {]}] + { \langle delete, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'\rangle \quad + \langle extend\: 0, s_i, s_o, s'\rangle \Rightarrow + \langle s_i, s_o, s''\rangle} + { \langle not \: x, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s''\rangle}$ if $x\neq 0\\ +\infer [{[}greater^<_{sos} {]}] + { \langle delete, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'\rangle \quad + \langle delete, s_i, s_o, s'\rangle \Rightarrow + \langle s_i, s_o, s''\rangle \quad + \langle extend\:,1, s_i, s_o, s''\rangle \Rightarrow + \langle s_i, s_o, s'''\rangle} + { \langle greater \: x,y, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'''\rangle}$ if $x>y\\ +\infer [{[}greater^>_{sos} {]}] + { \langle delete, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'\rangle \quad + \langle delete, s_i, s_o, s'\rangle \Rightarrow + \langle s_i, s_o, s''\rangle \quad + \langle extend\: 0, s_i, s_o, s''\rangle \Rightarrow + \langle s_i, s_o, s'''\rangle} + { \langle greater \: x,y, s_i, s_o, s\rangle \Rightarrow + \langle s_i, s_o, s'''\rangle}$ if $x