X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=semantics.tex;h=f7fb7faaeb275084c8127acc152ad400b5903e82;hb=d5eb78db13b8b04fdf0a3edf3e636dd9006948af;hp=fb4c747519ebff4e48ade7d171011b761be35c41;hpb=0039f1b4471d13af48e769f1d76084f2cbe03c20;p=sec1415.git

diff --git a/semantics.tex b/semantics.tex
index fb4c747..f7fb7fa 100644
--- a/semantics.tex
+++ b/semantics.tex
@@ -1,123 +1,172 @@
 \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
+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
+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.\\
+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:\\ 
+gerepresenteerd als: $s=[e_0, e_1, \dots, e_n]$ waarbij $e_i\in\mathbb{Z}$
+ en waarbij het bovenste element op de stack gerepresenteerd wordt door het
+ eerste element in de lijst.\\
+Het transitiesysteem 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
+Waarbij de laatste transitie duidt op een transitie waar een volgende transitie
+aanwezig is en genomen kan worden. De tweede duidt op een transitie waarbij er
+geen volgede beschikbaar is en het programma dus termineerd.
 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<y
-$
-\normalsize
+\subsection{Semantiekbeschrijving}
+
+Om de semantiekregels te kunnen beschrijven maken we gebruik van hulpfuncties. Hieronder staat het type van de functies en een korte beschrijving.
+De implementatie van deze functies staat in de appendix bij het aangegeven regelnummer.\\
+
+delete functie (d, r. 5):\\
+Om het bovenste element van een stack weg te kunnen gooien gebruiken we de volgende 
+functie:\\
+$$\mathcal{D} : Stack \rightarrow Stack$$
+Deze functie haalt het bovenste element van de stack en gooit deze weg.\\
+
+extend functie (e, r. 9):\\
+Om een stack uit te kunnen breiden met een element gebruiken we de volgende 
+functie:\\
+$$\mathcal{E} : \mathbb{Z}\rightarrow (Stack\rightarrow Stack)$$\\
+Deze functie neemt een stack en een integer en voegt de integer toe bovenop de 
+stack.\\
+
+add functie (add, r. 13):\\
+Om de bovenste twee elementen van een stack op te tellen gebruiken we de volgende 
+functie:\\
+$$\mathcal{ADD} : Stack \rightarrow Stack$$
+Deze functie haalt de bovenste twee waarden van de stack, telt ze bij elkaar op, en stopt 
+het resultaat bovenop de stack.\\
+
+subtract functie (sub, r. 18)\\
+Om de bovenste twee elementen van een stack van elkaar af te trekken gebruiken we 
+de volgende functie:\\
+$$\mathcal{SUB} : Stack \rightarrow Stack$$
+Deze functie haalt de bovenste twee elementen van de stack, trekt de bovenste 
+waarde van de tweede bovenste waarde af, en stopt het resultaat bovenop de stack.\\
+
+multiply functie (mul, r. 23):\\
+Om de bovenste twee elementen van een stack te vermenigvuldigen gebruiken we de 
+volgende functie:\\
+$$\mathcal{MUL} : Stack \rightarrow Stack$$
+Deze functie haalt de bovenste twee elementen van de stack, vermenigvuldigt ze, 
+en stopt het resultaat bovenop de stack.\\
+
+division functie (div, r. 28):\\
+Om de geheeltallige deling van de bovenste twee elementen van de stack bovenop de 
+stack te krijgen gebruiken we de volgende functie:\\
+$$\mathcal{DIV} : Stack \rightarrow Stack$$
+Deze functie haalt de bovenste twee elementen van de stack, berekent de 
+geheeltallige deling van de tweede bovenste waarde door de bovenste waarde, 
+en stopt het resultaat bovenop de stack.\\
+
+modulo functie (modc, r. 33):\\
+Om  de tweede bovenste waarde modulo de bovenste waarde te berekenen 
+gebruiken we de volgende functie:\\
+$$\mathcal{MOD} : Stack \rightarrow Stack$$
+Deze functie haalt de bovenste twee elementen van de stack, berekent het 
+resultaat van de tweede bovenste waarde modulo de bovenste waarde, en 
+stopt dit bovenop de stack.\\
+
+duplicate functie (dup, r. 38):\\
+Om het bovenste element van een stack te dupliceren gebruiken we de 
+volgende functie:\\
+$$\mathcal{DUP} : Stack \rightarrow Stack$$
+Deze functie haalt de bovenste waarde van de stack en stopt een kopie 
+en de bovenste waarde bovenop de stack.\\
+
+not functie (notc, r. 42):\\
+Om de not van de bovenste waarde te berekenen gebruiken we de 
+volgende functie:\\
+$$\mathcal{NOT} : Stack \rightarrow Stack$$\\
+Deze functie neemt het bovenste element van de stack en stopt 0 bovenaan de 
+stack als deze waarde niet gelijk is aan 0 en 1 als deze waarde gelijk is aan 0.\\
+
+greater functie (gre, r. 47):\\
+Om kijken of de tweede bovenste waarde groter is dan de bovenste waarde 
+gebruiken we de volgende functie:\\
+$$\mathcal{GRE} : Stack \rightarrow Stack$$\\
+Deze functie haalt de bovenste twee waarden van de stack en stopt een 1 bovenop 
+de stack als de tweede bovenste waarde groter is dan de bovenste waarde. Anders 
+word een 0 bovenop de stack gestopt.\\
+
+roll functie (roll, r. 54):\\
+Om de stack te rollen gebruiken we de volgende functie:\\
+$$\mathcal{ROLL} : Stack \rightarrow Stack$$\\
+Deze functie haalt de bovenste twee elementen van de stack en stopt 1 bovenop 
+de stack als het tweede bovenste element een hogere waarde heeft als dat van het 
+bovenste element. Anders word 1 bovenop de stack gestopt.\\ 
+
+out number (output stack) functie (outnum, r. 70):\\
+Deze functie past de output stack aan als er een integer naartoe geschreven word:\\
+$$\mathcal{OUTN_{SO}} : Stack \rightarrow Stack$$\\
+Deze functie haalt het bovenste element van de stack en stopt dit element bovenop de output stack.\\
+
+in number (stack) functie (innum, r. 75):\\
+Deze functie past de stack aan als er een integer naartoe geschreven word:\\
+$$\mathcal{INN_S} : Stack \rightarrow Stack$$\\
+Deze functie haalt het bovenste element van de input stack en stopt dit element bovenop de output stack.\\
+
+Met behulp van deze gedefinieerde functies kunnen we nu de volgende semantiekregels opstellen:\\
+
+\begin{alignat*}{2}
+{[comp^1_{sos}]}\qquad &
+\frac{\langle S_2, s\rangle \Rightarrow \langle S'_2, s'\rangle}
+{\langle S_1 ;S_2, s\rangle \Rightarrow \langle S_1;S'_2, s'\rangle}\\
+{[comp^2_{sos}]}\qquad &
+\frac{\langle S_2, s\rangle \Rightarrow \langle s'\rangle}
+{\langle S_1 ;S_2, s\rangle \Rightarrow \langle S_1, s'\rangle}\\
+{[pop_{sos}]}\qquad &
+\langle pop, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o,\mathcal{D}(s)\rangle\\
+{[add_{sos}]}\qquad
+&\langle add, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{ADD}(s)\rangle\\
+{[subtract_{sos} ]}\qquad &
+\langle subtract, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{SUB}(s)\rangle\\
+{[multiply_{sos}]}\qquad &
+\langle multiply, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{MUL}(s)\rangle\\
+{[divide_{sos}]} \qquad &
+\langle divide, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{DIV}(s)\rangle\\
+{[mod_{sos}]} \qquad &
+\langle mod, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{MOD}(s)\rangle\\
+{[duplicate_{sos}]} \qquad &
+\langle duplicate, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{DUP}(s)\rangle\\
+{[not_{sos}]} \qquad &
+\langle not, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{NOT}(s)\rangle\\
+{[greater_{sos}]} \qquad &
+\langle greater, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{GRE}(s)\rangle\\
+{[pointer_{sos}]} \qquad &
+\langle pointer, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{D}(s)\rangle\\
+{[switch_{sos}]} \qquad &
+\langle switch, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{D}(s)\rangle\\
+{[push_{sos}]} \qquad &
+\langle push \: n, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{E}(n,s)\rangle\\
+{[roll_{sos}]} \qquad &
+\langle roll, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, s_o, \mathcal{ROLL}(s)\rangle\\
+{[innum_{sos}]} \qquad &
+\langle innum, s_i, s_o, s\rangle \Rightarrow
+\langle \mathcal{D}(s_i), s_o, \mathcal{INN_S}(s)\rangle\\
+{[outnum_{sos}]} \qquad &
+\langle outnum, s_i, s_o, s\rangle \Rightarrow
+\langle s_i, \mathcal{OUTN_{SO}}(s_o),\mathcal{D}(s)\rangle\\
+\end{alignat*}
+