X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=semantics.tex;h=f7fb7faaeb275084c8127acc152ad400b5903e82;hb=d5eb78db13b8b04fdf0a3edf3e636dd9006948af;hp=d80eb80a28dcf9b065158b578d6916676f0fa466;hpb=eaf490e7216d0dc1a16a1b407b19931d29a2bec3;p=sec1415.git diff --git a/semantics.tex b/semantics.tex index d80eb80..f7fb7fa 100644 --- a/semantics.tex +++ b/semantics.tex @@ -1,155 +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{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$$ -$$\mathcal{D} [\:] = [\:]$$ -$$\mathcal{D} [a:rest] = [rest] $$ 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} : Stack\rightarrow (\mathbb{Z} \rightarrow Stack)$$\\ +$$\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$$ -$$\mathcal{ADD} [\:] = [\:]$$ -$$\mathcal{ADD} [a] = [a] $$ -$$\mathcal{ADD} [a:b:rest] = [b+a:rest] $$\\ 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$$ -$$\mathcal{SUB} [\:] = [\:]$$ -$$\mathcal{SUB} [a] = [a] $$ -$$\mathcal{SUB} [a:b:rest] = [b-a:rest] $$\\ 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 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$$ -$$\mathcal{MUL} [\:] = [\:]$$ -$$\mathcal{MUL} [a] = [a] $$ -$$\mathcal{MUL} [a:b:rest] = [b*a:rest] $$\\ 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$$ -$$\mathcal{DIV} [\:] = [\:]$$ -$$\mathcal{DIV} [a] = [a] $$ -$$\mathcal{DIV} [a:b:rest] = [b/a:rest] $$\\ 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.\\ -Om gebruiken we de -volgende functie:\\ +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$$ -$$\mathcal{MOD} [\:] = [\:]$$ -$$\mathcal{MOD} [a] = [a] $$ -$$\mathcal{MOD} [a:b:rest] = [b \: mod \: a:rest] $$\\ -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.\\ +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$$ -$$\mathcal{DUP} [\:] = [\:]$$ -$$\mathcal{DUP} [a:rest] = [a:a:rest] $$\\ -Deze functie haalt stopt een kopie van de bovenste waarde bovenop de stack.\\ +Deze functie haalt de bovenste waarde van de stack en stopt een kopie +en de bovenste waarde bovenop de stack.\\ -Om de gebruiken we de +not functie (notc, r. 42):\\ +Om de not van de bovenste waarde te berekenen gebruiken we de volgende functie:\\ -$$\mathcal{NOT} : Stack \rightarrow Stack$$ -$$\mathcal{NOT} [\:] = [\:]$$ -$$\mathcal{NOT} [a:rest] = [0:rest] \: \text{if} \: a \neq 0$$ -$$\mathcal{NOT} [a:rest] = [1:rest] \: \text{if} \: a = 0$$\\ +$$\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.\\ -Om gebruiken we de -volgende functie:\\ -$$\mathcal{GRE} : Stack \rightarrow Stack$$ -$$\mathcal{GRE} [\:] = [\:]$$ -$$\mathcal{GRE} [a] = [a] $$ -$$\mathcal{GRE} [a:b:rest] = [0:rest] \: \text{if} \: a \geq b$$ -$$\mathcal{GRE} [a:b:rest] = [1:rest] \: \text{if} \: a < b$$\\ +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.\\ -Met behulp van deze gedefineerde functies kunnen we nu de volgende semantiekregels opstellen:\\ +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.\\ -$ -{[pop_{sos}]}\qquad +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 add, s_i, s_o, s\rangle \Rightarrow \langle s_i, s_o, \mathcal{ADD}(s)\rangle\\ -{[subtract_{sos} ]}\qquad +{[subtract_{sos} ]}\qquad & \langle subtract, s_i, s_o, s\rangle \Rightarrow \langle s_i, s_o, \mathcal{SUB}(s)\rangle\\ -{[multiply_{sos}]}\qquad +{[multiply_{sos}]}\qquad & \langle multiply, s_i, s_o, s\rangle \Rightarrow \langle s_i, s_o, \mathcal{MUL}(s)\rangle\\ -{[divide_{sos}]} \qquad +{[divide_{sos}]} \qquad & \langle divide, s_i, s_o, s\rangle \Rightarrow \langle s_i, s_o, \mathcal{DIV}(s)\rangle\\ -{[mod_{sos}]} \qquad\qquad +{[mod_{sos}]} \qquad & \langle mod, s_i, s_o, s\rangle \Rightarrow \langle s_i, s_o, \mathcal{MOD}(s)\rangle\\ -{[duplicate_{sos}]} \qquad +{[duplicate_{sos}]} \qquad & \langle duplicate, s_i, s_o, s\rangle \Rightarrow \langle s_i, s_o, \mathcal{DUP}(s)\rangle\\ -{[not_{sos}]}\qquad\qquad +{[not_{sos}]} \qquad & \langle not, s_i, s_o, s\rangle \Rightarrow \langle s_i, s_o, \mathcal{NOT}(s)\rangle\\ -{[greater_{sos}]} \qquad +{[greater_{sos}]} \qquad & \langle greater, s_i, s_o, s\rangle \Rightarrow \langle s_i, s_o, \mathcal{GRE}(s)\rangle\\ -{[push_{sos}]} \qquad -\langle push, s_i, s_o, s\rangle \Rightarrow -\langle s_i, s_o, s\rangle\\ -{[roll_{sos}]} \qquad +{[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, s\rangle\\ -{[inchar_{sos}]} \qquad -\langle inchar, s_i, s_o, s\rangle \Rightarrow -\langle s_i, s_o, s\rangle\\ -{[innum_{sos}]} \qquad +\langle s_i, s_o, \mathcal{ROLL}(s)\rangle\\ +{[innum_{sos}]} \qquad & \langle innum, 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\\ -{[outnum_{sos}]} \qquad +\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, s_o, s\rangle\\ -$ +\langle s_i, \mathcal{OUTN_{SO}}(s_o),\mathcal{D}(s)\rangle\\ +\end{alignat*} +