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.\\
19 \subsection{Semantiek beschrijving
}
20 Om het eerste element van een stack weg te kunnen gooien gebruiken we de volgende functie:\\
21 $$
\mathcal{D
} : s
\rightarrow s$$\\
22 Deze neemt een stack en gooit het bovenste element weg.\\
24 Om een stack uit te kunnen breiden met een element gebruiken we de volgende functie:\\
25 $$
\mathcal{E
} : s,
\mathbb{Z
} \rightarrow s$$\\
26 Deze functie neemt een stack en een integer en voegt de integer toe bovenop de stack.\\
29 $
\infer [{[}delete_
{sos
}{]}]
30 { \langle delete, s_i, s_o, s
\rangle \Rightarrow
31 \langle s_i,s_o,
\mathcal{D
}[s
]\rangle}{}\\
32 \infer [{[}extend_
{sos
}{]}]
33 { \langle extend \: z, s_i, s_o, s
\rangle \Rightarrow
34 \langle s_i, s_o,
\mathcal{E
}[s, z
]\rangle}{}\\
35 \infer [{[}pop_
{sos
} {]}]
36 { \langle delete, s_i, s_o, s
\rangle \Rightarrow
37 \langle s_i, s_o, s'
\rangle}
38 { \langle pop, s_i, s_o, s
\rangle \Rightarrow
39 \langle s_i, s_o, s'
\rangle}\\
40 \infer [{[}add_
{sos
} {]}]
41 { \langle delete, s_i, s_o, s
\rangle \Rightarrow
42 \langle s_i, s_o, s'
\rangle \quad
43 \langle delete, s_i, s_o, s'
\rangle \Rightarrow
44 \langle s_i, s_o, s''
\rangle \quad
45 \langle extend\: x+y, s_i, s_o, s''
\rangle \Rightarrow
46 \langle s_i, s_o, s'''
\rangle}
47 { \langle add \: x,y, s_i, s_o, s
\rangle \Rightarrow
48 \langle s_i, s_o, s'''
\rangle}\\
49 \infer [{[}subtract_
{sos
} {]}]
50 { \langle delete, s_i, s_o, s
\rangle \Rightarrow
51 \langle s_i, s_o, s'
\rangle \quad
52 \langle delete, s_i, s_o, s'
\rangle \Rightarrow
53 \langle s_i, s_o, s''
\rangle \quad
54 \langle extend\: x-y, s_i, s_o, s''
\rangle \Rightarrow
55 \langle s_i, s_o, s'''
\rangle}
56 { \langle subtract \: x,y, s_i, s_o, s
\rangle \Rightarrow
57 \langle s_i, s_o, s'''
\rangle}\\
58 \infer [{[}multiply_
{sos
} {]}]
59 { \langle delete, s_i, s_o, s
\rangle \Rightarrow
60 \langle s_i, s_o, s'
\rangle \quad
61 \langle delete, s_i, s_o, s'
\rangle \Rightarrow
62 \langle s_i, s_o, s''
\rangle \quad
63 \langle extend\: x*y, s_i, s_o, s''
\rangle \Rightarrow
64 \langle s_i, s_o, s'''
\rangle}
65 { \langle multiply \: x,y, s_i, s_o, s
\rangle \Rightarrow
66 \langle s_i, s_o, s'''
\rangle}\\
67 \infer [{[}divide_
{sos
} {]}]
68 { \langle delete, s_i, s_o, s
\rangle \Rightarrow
69 \langle s_i, s_o, s'
\rangle \quad
70 \langle delete, s_i, s_o, s'
\rangle \Rightarrow
71 \langle s_i, s_o, s''
\rangle \quad
72 \langle extend\: x/y, s_i, s_o, s''
\rangle \Rightarrow
73 \langle s_i, s_o, s'''
\rangle}
74 { \langle divide \: x,y, s_i, s_o, s
\rangle \Rightarrow
75 \langle s_i, s_o, s'''
\rangle}\\
76 \infer [{[}mod_
{sos
} {]}]
77 { \langle delete, s_i, s_o, s
\rangle \Rightarrow
78 \langle s_i, s_o, s'
\rangle \quad
79 \langle delete, s_i, s_o, s'
\rangle \Rightarrow
80 \langle s_i, s_o, s''
\rangle \quad
81 \langle extend\: x \: mod \: y, s_i, s_o, s''
\rangle \Rightarrow
82 \langle s_i, s_o, s'''
\rangle}
83 { \langle mod \: x,y, s_i, s_o, s
\rangle \Rightarrow
84 \langle s_i, s_o, s'''
\rangle}\\
85 \infer [{[}duplicate_
{sos
} {]}]
86 { \langle extend\: x, s_i, s_o, s
\rangle \Rightarrow
87 \langle s_i, s_o, s'
\rangle}
88 { \langle duplicate \: x, s_i, s_o, s
\rangle \Rightarrow
89 \langle s_i, s_o, s'
\rangle}\\
90 \infer [{[}not^
0_
{sos
} {]}]
91 { \langle delete, s_i, s_o, s
\rangle \Rightarrow
92 \langle s_i, s_o, s'
\rangle \quad
93 \langle extend\:
1, s_i, s_o, s'
\rangle \Rightarrow
94 \langle s_i, s_o, s''
\rangle}
95 { \langle not \: x, s_i, s_o, s
\rangle \Rightarrow
96 \langle s_i, s_o, s''
\rangle}$ if $x =
0\\
97 \infer [{[}not^*_
{sos
} {]}]
98 { \langle delete, s_i, s_o, s
\rangle \Rightarrow
99 \langle s_i, s_o, s'
\rangle \quad
100 \langle extend\:
0, s_i, s_o, s'
\rangle \Rightarrow
101 \langle s_i, s_o, s''
\rangle}
102 { \langle not \: x, s_i, s_o, s
\rangle \Rightarrow
103 \langle s_i, s_o, s''
\rangle}$ if $x
\neq 0\\
104 \infer [{[}greater^<_
{sos
} {]}]
105 { \langle delete, s_i, s_o, s
\rangle \Rightarrow
106 \langle s_i, s_o, s'
\rangle \quad
107 \langle delete, s_i, s_o, s'
\rangle \Rightarrow
108 \langle s_i, s_o, s''
\rangle \quad
109 \langle extend\:,
1, s_i, s_o, s''
\rangle \Rightarrow
110 \langle s_i, s_o, s'''
\rangle}
111 { \langle greater \: x,y, s_i, s_o, s
\rangle \Rightarrow
112 \langle s_i, s_o, s'''
\rangle}$ if $x>y\\
113 \infer [{[}greater^>_
{sos
} {]}]
114 { \langle delete, s_i, s_o, s
\rangle \Rightarrow
115 \langle s_i, s_o, s'
\rangle \quad
116 \langle delete, s_i, s_o, s'
\rangle \Rightarrow
117 \langle s_i, s_o, s''
\rangle \quad
118 \langle extend\:
0, s_i, s_o, s''
\rangle \Rightarrow
119 \langle s_i, s_o, s'''
\rangle}
120 { \langle greater \: x,y, s_i, s_o, s
\rangle \Rightarrow
121 \langle s_i, s_o, s'''
\rangle}$ if $x<y