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
}
21 Om het eerste element van een stack weg te kunnen gooien gebruiken we de volgende
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
28 $$
\mathcal{E
} : s,
\mathbb{Z
} \rightarrow s$$\\
29 Deze functie neemt een stack en een integer en voegt de integer toe bovenop de
32 Om de bovenste twee elementen van een stack op te tellen gebruiken we de volgende
34 $$
\mathcal{ADD
} : Stack
\rightarrow Stack$$
35 $$
\mathcal{ADD
} [\:
] =
[\:
]$$
36 $$
\mathcal{ADD
} [a
] =
[a
] $$
37 $$
\mathcal{ADD
} [a:b:rest
] =
[b+a:rest
] $$\\
39 Om de bovenste twee elementen van een stack van elkaar af te trekken gebruiken we
40 de volgende functie:\\
41 $$
\mathcal{SUB
} : Stack
\rightarrow Stack$$
42 $$
\mathcal{SUB
} [\:
] =
[\:
]$$
43 $$
\mathcal{SUB
} [a
] =
[a
] $$
44 $$
\mathcal{SUB
} [a:b:rest
] =
[b-a:rest
] $$\\
46 Om de bovenste twee elementen van een stack te vermenigvuldigen gebruiken we de
48 $$
\mathcal{MUL
} : Stack
\rightarrow Stack$$
49 $$
\mathcal{MUL
} [\:
] =
[\:
]$$
50 $$
\mathcal{MUL
} [a
] =
[a
] $$
51 $$
\mathcal{MUL
} [a:b:rest
] =
[b*a:rest
] $$\\
53 Om de integer deling van de bovenste twee elementen van de stack bovenop de
54 stack te krijgen gebruiken we de volgende functie:\\
55 $$
\mathcal{DIV
} : Stack
\rightarrow Stack$$
56 $$
\mathcal{DIV
} [\:
] =
[\:
]$$
57 $$
\mathcal{DIV
} [a
] =
[a
] $$
58 $$
\mathcal{DIV
} [a:b:rest
] =
[b/a:rest
] $$\\
60 Om de bovenste twee elementen van een stack op te tellen gebruiken we de
62 $$
\mathcal{MOD
} : Stack
\rightarrow Stack$$
63 $$
\mathcal{MOD
} [\:
] =
[\:
]$$
64 $$
\mathcal{MOD
} [a
] =
[a
] $$
65 $$
\mathcal{MOD
} [a:b:rest
] =
[b \: mod \: a:rest
] $$\\
67 Om het bovenste element van een stack te dupliceren gebruiken we de
69 $$
\mathcal{DUP
} : Stack
\rightarrow Stack$$
70 $$
\mathcal{DUP
} [\:
] =
[\:
]$$
71 $$
\mathcal{DUP
} [a:rest
] =
[a:a:rest
] $$\\
73 Om de bovenste twee elementen van een stack op te tellen gebruiken we de
75 $$
\mathcal{NOT
} : Stack
\rightarrow Stack$$
76 $$
\mathcal{NOT
} [\:
] =
[\:
]$$
77 $$
\mathcal{NOT
} [a:rest
] =
[0:rest
] \:
\text{if
} \: a
\neq 0$$
78 $$
\mathcal{NOT
} [a:rest
] =
[1:rest
] \:
\text{if
} \: a =
0$$\\
80 Om de bovenste twee elementen van een stack op te tellen gebruiken we de
82 $$
\mathcal{GRE
} : Stack
\rightarrow Stack$$
83 $$
\mathcal{GRE
} [\:
] =
[\:
]$$
84 $$
\mathcal{GRE
} [a
] =
[a
] $$
85 $$
\mathcal{GRE
} [a:b:rest
] =
[0:rest
] \:
\text{if
} \: a
\geq b$$
86 $$
\mathcal{GRE
} [a:b:rest
] =
[1:rest
] \:
\text{if
} \: a < b$$\\
88 Met behulp van deze gedefineerde functies kunnen we nu de volgende semantiekregels opstellen:\\
92 \langle pop, s_i, s_o, s
\rangle \Rightarrow
93 \langle s_i, s_o,
\mathcal{D
}(s)
\rangle\\
95 \langle add, s_i, s_o, s
\rangle \Rightarrow
96 \langle s_i, s_o,
\mathcal{ADD
}(s)
\rangle\\
97 {[subtract_
{sos
} ]}\qquad
98 \langle subtract, s_i, s_o, s
\rangle \Rightarrow
99 \langle s_i, s_o,
\mathcal{SUB
}(s)
\rangle\\
100 {[multiply_
{sos
}]}\qquad
101 \langle multiply, s_i, s_o, s
\rangle \Rightarrow
102 \langle s_i, s_o,
\mathcal{MUL
}(s)
\rangle\\
103 {[divide_
{sos
}]} \qquad
104 \langle divide, s_i, s_o, s
\rangle \Rightarrow
105 \langle s_i, s_o,
\mathcal{DIV
}(s)
\rangle\\
106 {[mod_
{sos
}]} \qquad\qquad
107 \langle mod, s_i, s_o, s
\rangle \Rightarrow
108 \langle s_i, s_o,
\mathcal{MOD
}(s)
\rangle\\
109 {[duplicate_
{sos
}]} \qquad
110 \langle duplicate, s_i, s_o, s
\rangle \Rightarrow
111 \langle s_i, s_o,
\mathcal{DUP
}(s)
\rangle\\
112 {[not_
{sos
}]}\qquad\qquad
113 \langle not, s_i, s_o, s
\rangle \Rightarrow
114 \langle s_i, s_o,
\mathcal{NOT
}(s)
\rangle\\
115 {[greater_
{sos
}]} \qquad
116 \langle greater, s_i, s_o, s
\rangle \Rightarrow
117 \langle s_i, s_o,
\mathcal{GRE
}(s)
\rangle \qquad \\