X-Git-Url: https://git.martlubbers.net/?a=blobdiff_plain;f=semantics.tex;h=f7fb7faaeb275084c8127acc152ad400b5903e82;hb=d5eb78db13b8b04fdf0a3edf3e636dd9006948af;hp=137f72f4925fd044795291022bd3ab033d7eefff;hpb=1e99906ba6bf2dc7453ba366e2e7c8f77ac4b916;p=sec1415.git diff --git a/semantics.tex b/semantics.tex index 137f72f..f7fb7fa 100644 --- 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 -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} +\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*} +