blob: d8b68ea0d80097543aeda3443a6fec1f301dd2f1 (
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
39
40
41
42
|
% vim: set spelllang=nl:
\subsection{\texttt{Input}}
\begin{quote}
i - takes a string from user input, and places it on the stack.
\end{quote}
In het bijzonder dit commando is erg slecht gedefinieerd. Mag deze input
bijvoorbeeld line feeds bevatten? Een naïeve implementatie die van stdin
gebruik maakt zou standaard splitsen op line feeds en dit dus niet toestaan.
Een andere implementatie zou gebruik kunnen maken van grafische prompts waarin
het wél mogelijk is meerdere regels input te geven.
Om bij het redeneren over de semantiek geen last te hebben van zulk soort
implementatiedetails hebben we ervoor gekozen hier tot op een hoog niveau van
te abstraheren. We gaan ervan uit dat we een stack van strings, $\Input$,
hebben die ons de input geeft. Hoe deze stack is geïmplementeerd doet niet ter
zake. Ook leggen we geen restricties op aan de karakters waaruit haar elementen
bestaan.
We gaan er verder van uit dat de gebruiker zijn programma volledig wil
uitvoeren en dus voldoende input zal geven, waardoor $\pop\ip$ altijd
gedefinieerd is. Geeft de gebruiker niet genoeg input, dan hoeven we dus geen
afleidingsboom maken (en we zullen dit ook onmogelijk maken).
Dit geeft de volgende regel:
$$
\begin{prooftree}
\trans
{\pgm}{\ip'}{(\push\val\stk, \str)}
{\ip''}{\op}{\st}
\justifies
\trans
{\StmInput:\pgm}{\ip}{(\stk,\str)}
{\ip''}{\op}{\st}
\using{\rinputns}
\qquad
\text{met $(\val,\ip')=\pop\ip$}
\end{prooftree}
$$
|
