semantics aangetikt maar niet gedaan, analysis mee begonnen, skip klaar en compositie ook

[sec1415.git] / semantics.tex

diff --git a/semantics.tex b/semantics.tex
index 137f72f..f7fb7fa 100644 (file)
--- a/semantics.tex
+++ b/semantics.tex
@@ -1,19 +1,172 @@
 \subsection{Structurele operationele semantiek}
 Bij natuurlijke semantiek(ns) ligt de nadruk op de relatie tussen de begin en
 \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
 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
 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
 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$\\ 
 $\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.\\ 
 
 op een niet terminerende transitie.\\ 
 

-\subsection{Semantiek beschrijving}
+\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*}
+