blob: 9d8985c8a620f1d989afead5c7036f36a31e93a6 (
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
43
|
% vim: set spelllang=nl:
\subsection{\texttt{Input}}
\label{sec:rules:input}
\begin{quote}
i - takes a string from user input, and places it on the stack.
\end{quote}
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 te 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 $\pop\ip = (\val,\ip')$.}
\end{prooftree}
$$
|
