blob: 975c04f441f09d020d2bdeea74839ec10744eaf5 (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
|
% vim: set spelllang=nl:
\subsection{Toestanden}
\label{sec:def:state}
Een toestand $s\in\State$ van Smurf bevat zowel een stack als een variable
store. Hieruit volgt de voor de hand liggende definitie voor $\State$,
$$\State \isdef \Stack{\String} \times (\String \to \String),$$
waarbij we $s=(\stk,\str)\in\State$ lezen als de toestand $s$ met stack $\stk$
en variable store $\str$.
De variable store is een totale functie. Initieel zijn alle waardes in de store
$\lambda$ in overeenstemming met de documentatie \cite{safalra}:
\begin{quote}
Any string can be used as a variable name, including the empty string. All
variable values are initially set to the empty string.
\end{quote}
Een toewijzing van $\val$ aan $\var$ noteren we als $\var\mapsto\val$. Een
store noteren we als een verzameling van zulke toewijzingen, zodat we bijvoorbeeld
$\{\texttt{x}\mapsto\texttt{hello world}\}$ noteren voor de store die
\texttt{x} naar ``hello world'' stuurt. We laten de strings die naar $\lambda$
sturen normaal gesproken weg. De initiële store schrijven we dus als
$\emptystore$.
Om de waarde van een key $k$ uit store $\str$ te halen gebruiken we simpelweg
$\str~k$. Vervolgens definiëren we $\putop:\SynString \times \SynString \times
(\String\to\String) \to (\String\to\String)$ die gegeven een variabelenaam, een
waarde en een oude store een nieuwe store oplevert:
$$
\smurfput{\var}{\val}{\str} \var' =
\begin{cases}
\val & \text{als $\var'=\var$} \\
\str~\var' & \text{als $\var'\ne\var$}
\end{cases}
$$
|
