1st version of semantics

Can't deal with branches and loops in the Piet program.

diff --git a/project.synctex.gz b/project.synctex.gz
new file mode 100644 (file)
index 0000000..df0688d
Binary files /dev/null and b/project.synctex.gz differ

diff --git a/semantics.tex b/semantics.tex
index 137f72f..e977049 100644 (file)
--- a/semantics.tex
+++ b/semantics.tex
@@ -16,4 +16,39 @@ $\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 de laatste transitie duidt op een terminerende transitie en de eerste
 op een niet terminerende transitie.\\ 
 

+
+

 \subsection{Semantiek beschrijving}
 \subsection{Semantiek beschrijving}

+Om het eerste element van een stack weg te kunnen gooien gebruiken we de volgende functie:\\
+$$\mathcal{D} : s \rightarrow s$$\\
+Deze neemt een stack en gooit het bovenste element weg.\\
+
+Om een stack uit te kunnen breiden met een element gebruiken we de volgende functie:\\
+$$\mathcal{E} : s, \mathbb{Z} \rightarrow s$$\\
+Deze functie neemt een stack en een integer en voegt de integer toe bovenop de stack.\\
+
+$[delete_{sos} ] \; <delete, s_i, s_o, s> \Rightarrow <s_i, s_o,\mathcal{D}[s]>$\\
+
+$[extend_{sos} ] \; <extend \: z, s_i, s_o, s> \Rightarrow <s_i, s_o,\mathcal{E}[s, z]>$\\
+
+$[pop_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>}{<pop, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>}$\\
+
+$[add_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\: x+y, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<add \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$\\
+
+$[subtract_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\:  x-y, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<subtract \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$\\
+
+$[multiply_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\:  x*y, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<multiply \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$\\
+
+$[divide_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\: x/y, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<divide \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$\\
+
+$[mod_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\:  x \: mod \: y, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<mod \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$\\
+
+$[duplicate_{sos} ] \; \frac{<extend\: x, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>}{<duplicate \: x, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>}$\\
+
+$[not^0_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <extend\: 1, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''>}{<not \: x, s_i, s_o, s> \Rightarrow <s_i, s_o, s''>}$ if x = 0\\
+
+$[not^*_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <extend\: 0, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''>}{<not \: x, s_i, s_o, s> \Rightarrow <s_i, s_o, s''>}$ if x $\neq$ 0\\
+
+$[greater^<_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\:,1, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<greater \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$ if x$<$y\\
+
+$[greater^>_{sos} ] \; \frac{<delete, s_i, s_o, s> \Rightarrow <s_i, s_o, s'>\; <delete, s_i, s_o, s'> \Rightarrow <s_i, s_o, s''> \; <extend\: 0, s_i, s_o, s''> \Rightarrow <s_i, s_o, s'''>}{<greater \: x,y, s_i, s_o, s> \Rightarrow <s_i, s_o, s'''>}$ if x$>$y\\
\ No newline at end of file