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.\\ 
 
+
+
 \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