aanpassing semantiek & analyse

[sec1415.git] / semantics.tex

diff --git a/semantics.tex b/semantics.tex
index 7812014..00eca8a 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,27 @@ 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 (output stack) functie (outnum, r. 79):\\
+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.\\
 
-out number functie (outnum, r. 74):\\
-
-in number functie (innum, r. 83):\\
-
-
-
-
-
-(switch, outchar, inchar)\\
+in number (stack) functie (innum, r. 84):\\
+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.\\
 
+(outchar, inchar)\\
 
 Met behulp van deze gedefinieerde functies kunnen we nu de volgende semantiekregels opstellen:\\
 
-
-
 \begin{alignat*}{2}
+{[comp^1_{sos}]}\qquad &
+\frac{\langle S_1, s\rangle \Rightarrow \langle S'_1, s'\rangle}
+{\langle S_1 ;S_2, s\rangle \Rightarrow \langle S'_1;S_2, s'\rangle}\\
+{[comp^2_{sos}]}\qquad &
+\frac{\langle S_1, s\rangle \Rightarrow \langle s'\rangle}
+{\langle S_1 ;S_2, s\rangle \Rightarrow \langle S_2, 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 +153,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 +164,15 @@ 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\\
+\langle s_i, \mathcal{OUTN_{SO}}(s_o),\mathcal{D}(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\\
 \end{alignat*}