Merge branch 'master' of github.com:dopefishh/sec2014 into commentaar_verwerken

[sec1415.git] / semantics.tex

diff --git a/semantics.tex b/semantics.tex
index 7812014..994aeb6 100644 (file)
--- a/semantics.tex
+++ b/semantics.tex
@@ -9,7 +9,9 @@ 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}$\\
+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 word door het
+ eerste element in de lijst.\\
 Het transitie systeem 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$\\ 
@@ -30,7 +32,7 @@ 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.\\
 
@@ -100,24 +102,25 @@ 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.\\ 
 
-pointer functie (pointer, r. 65):\\
-
-out number functie (outnum, r. 74):\\
-
-in number functie (innum, r. 83):\\
-
-
-
-
-
-(switch, outchar, inchar)\\
+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\\
@@ -148,6 +151,9 @@ Met behulp van deze gedefinieerde functies kunnen we nu de volgende semantiekreg
 {[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\\
@@ -156,18 +162,9 @@ Met behulp van deze gedefinieerde functies kunnen we nu de volgende semantiekreg
 \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*}