\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
-op een niet terminerende transitie.\\
+Waarbij bij de eerste transitie de executie van S niet na een stap klaar is en waarbij
+de tweede transitie duidt op een terminerende transitie.\\
\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.\\
+Om de semantiekregels te kunnen beschrijven maken we gebruik van hulpfuncties.
+Hieronder staat het type van de functies en een korte beschrijving.
+De implementatie is gedaan in de vorm van een functioneel programma in de taal \textit{Clean}.
+De implementatie van de functies staat in de appendix.
+Elke functie wordt op de volgende manier aangegeven: \textit{naam functie} (\textit{naam in appendix}, r. \textit{regelnummer in appendix})\\
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.\\
+Deze functie haalt het bovenste element van de stack en gooit dit weg.\\
extend functie (e, r. 9):\\
Om een stack uit te kunnen breiden met een element gebruiken we de volgende
functie:\\
-$$\mathcal{E} : Stack\rightarrow (\mathbb{Z} \rightarrow Stack)$$\\
-Deze functie neemt een stack en een integer en voegt de integer toe bovenop de
+$$\mathcal{E} : \mathbb{Z}\rightarrow (Stack\rightarrow Stack)$$\\
+Deze functie neemt een integer en een stack 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
+Deze functie haalt de bovenste twee waarden van de stack, telt ze bij elkaar op, en legt
het resultaat bovenop de stack.\\
subtract functie (sub, r. 18)\\
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.\\
+waarde van de tweede bovenste waarde af, en legt het resultaat bovenop de stack.\\
multiply functie (mul, r. 23):\\
Om de bovenste twee elementen van een stack te vermenigvuldigen gebruiken we de
en de bovenste waarde bovenop de stack.\\
not functie (notc, r. 42):\\
-Om de not van de bovenste waarde te berekenen gebruiken we de
+Om te kijken of de bovenste waarde gelijk is aan 0 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
+Om te 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.\\
+wordt een 0 bovenop de stack gestopt.\\
roll functie (roll, r. 54):\\
-Om de stack te rollen gebruiken we de volgende functie:\\
+Om de elementen op de stack te verschuiven 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.\\
+Deze functie haalt de bovenste twee elementen van de stack 'rolt' de rest van de stack tot een diepte die gelijk is aan de waarde van het tweede bovenste element. Een rol tot diepte \textit{n} verschuift de elementen 1 tot en met \textit{n} allemaal 1 plaats naar boven. Vervolgens wordt het eerste element van de stack op plaats \textit{n} neergelegd. Het aantal keren dat de stack gerold word is gelijk aan de waarde van het bovenste element. Als deze waarde negatief is word de stack in tegenovergestelde richting gerold. Dit houdt in dat bij elke rol het element op plaats \textit{n} bovenop de stack word gelegd, en de rest van de elementen (dat boven het element op plaats \textit{n} lagen) 1 plaats naar beneden wordt verschoven.\\
-pointer functie (pointer, r. 65):\\
+out number (output stack) functie (outnum, r. 70):\\
+Deze functie past de output stack aan als er een integer naartoe geschreven wordt:\\
+$$\mathcal{OUTN_{SO}} : Stack \rightarrow Stack$$\\
+Deze functie haalt het bovenste element van de stack en stopt dit element bovenop de output stack.\\
-out number functie (outnum, r. 74):\\
-
-in number functie (innum, r. 83):\\
-
-
-
-
-
-(switch, outchar, inchar)\\
-
-
-Met behulp van deze gedefinieerde functies kunnen we nu de volgende semantiekregels opstellen:\\
+in number (stack) functie (innum, r. 75):\\
+Deze functie past de stack aan als er een integer naartoe geschreven wordt:\\
+$$\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 semantiekregels opstellen.
+De meeste regels spreken redelijk voor zich: als een commando wordt uitgevoerd, zorgt dit voor een verandering in de bijbehorende stack. Deze verandering komt tot stand door het toepassen van de bijbehorende hulpfunctie op deze stack.
+Voor de semantiekregels voor de compositie halen we, in tegenstelling tot de normale gang van zaken bij sos, steeds een commando van het einde van de lijst af.
+Hiervoor is gekozen zodat de afleidingsrijen makkelijk te controleren zijn door bij de implementatie in \textit{Clean} de functies een voor een op een stack toe te passen.\\
\begin{alignat*}{2}
+{[comp^1_{sos}]}\qquad &
+\frac{\langle S_2, s\rangle \Rightarrow \langle S'_2, s_i', s_o', s'\rangle}
+{\langle S_1 ;S_2, s\rangle \Rightarrow \langle S_1;S'_2, s_i', s_o', s'\rangle}\\
+{[comp^2_{sos}]}\qquad &
+\frac{\langle S_2, s\rangle \Rightarrow \langle s_i', s_o', s'\rangle}
+{\langle S_1 ;S_2, s\rangle \Rightarrow \langle S_1, s_i', s_o', s'\rangle}\\
{[pop_{sos}]}\qquad &
\langle pop, s_i, s_o, s\rangle \Rightarrow
\langle s_i, s_o,\mathcal{D}(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\\
\langle s_i, s_o, \mathcal{ROLL}(s)\rangle\\
{[innum_{sos}]} \qquad &
\langle innum, s_i, s_o, s\rangle \Rightarrow
-\langle \mathcal{INN_{SI}}(s_i), s_o, \mathcal{INN_S}(s)\rangle\\
+\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{OUTN_S}(s)\rangle\\
-{[inchar_{sos}]} \qquad &
-\langle inchar, s_i, s_o, s\rangle \Rightarrow
-\langle s_i, s_o, s\rangle\\
-{[outchar_{sos}]} \qquad &
-\langle outchar, s_i, s_o, s\rangle \Rightarrow
-\langle s_i, s_o, s\rangle\\
-{[switch_{sos}]} \qquad &
-\langle switch, s_i, s_o, s\rangle \Rightarrow
-\langle s_i, s_o, s\rangle\\
+\langle s_i, \mathcal{OUTN_{SO}}(s_o),\mathcal{D}(s)\rangle\\
\end{alignat*}
repositories / sec1415.git / blobdiff