1 \subsection{Structurele operationele semantiek
}
2 Bij natuurlijke semantiek(ns) ligt de nadruk op de relatie tussen de begin en
3 de eind state. Het nadeel hiervan is dat programma’s die niet termineren geen
4 bewijsbomen hebben. Hierdoor is het niet mogelijk om eigenschappen te bewijzen
5 voor zulke programma’s. Bij structurele operationele semantiek(sos) ligt de
6 nadruk juist op de individuele stappen van de executie en zijn er w\'el
7 bewijsrijen voor programma’s die niet termineren.\\
8 Om deze redenen hebben we gekozen voor sos.\\
9 Een toestand in onze semantiek wordt beschreven door drie stacks; input, output
10 en programma. Respectievelijk benoemen we deze met $s_i, s_o, s$ en beschrijven
11 ze de STDIN, STDOUT en interne stack van het programma. Stacks worden
12 gerepresenteerd als: $s=
[e_0, e_1,
\dots, e_n
]$ waarbij $e_i
\in\mathbb{Z
}$\\
13 Het transitie systeem zal twee verschillende transities kennen, namelijk:\\
14 $
\langle S, s_i, s_o, s
\rangle\Rightarrow\langle S', s_i', s_o', s'
\rangle$ en\\
15 $
\langle S, s_i, s_o, s
\rangle\Rightarrow\langle s_i', s_o', s'
\rangle$\\
16 Waarbij de laatste transitie duidt op een terminerende transitie en de eerste
17 op een niet terminerende transitie.\\
21 \subsection{Semantiek beschrijving
}
22 Om het eerste element van een stack weg te kunnen gooien gebruiken we de volgende functie:\\
23 $$
\mathcal{D
} : s
\rightarrow s$$\\
24 Deze neemt een stack en gooit het bovenste element weg.\\
26 Om een stack uit te kunnen breiden met een element gebruiken we de volgende functie:\\
27 $$
\mathcal{E
} : s,
\mathbb{Z
} \rightarrow s$$\\
28 Deze functie neemt een stack en een integer en voegt de integer toe bovenop de stack.\\
30 $
[delete_
{sos
} ] \; <delete, s_i, s_o, s>
\Rightarrow <s_i, s_o,
\mathcal{D
}[s
]>$\\
32 $
[extend_
{sos
} ] \; <extend \: z, s_i, s_o, s>
\Rightarrow <s_i, s_o,
\mathcal{E
}[s, z
]>$\\
34 $
[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'>
}$\\
36 $
[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'''>
}$\\
38 $
[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'''>
}$\\
40 $
[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'''>
}$\\
42 $
[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'''>
}$\\
44 $
[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'''>
}$\\
46 $
[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'>
}$\\
48 $
[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\\
50 $
[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\\
52 $
[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\\
54 $
[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\\