diff options
| -rw-r--r-- | rules.tex | 2 | ||||
| -rw-r--r-- | rulesinput.tex | 42 | ||||
| -rw-r--r-- | smurf.sty | 1 |
3 files changed, 44 insertions, 1 deletions
@@ -19,7 +19,7 @@ Smurfprogramma's makkelijker zal maken. %\input{rulescat} \input{rulesget} \input{rulesput} -%\input{rulesinput} +\input{rulesinput} %\input{rulesoutput} \input{rulesexec} diff --git a/rulesinput.tex b/rulesinput.tex new file mode 100644 index 0000000..d8b68ea --- /dev/null +++ b/rulesinput.tex @@ -0,0 +1,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} +$$ + @@ -57,6 +57,7 @@ \def\rule#1#2{[\mbox{#1}_{\mbox{\footnotesize{#2}}}]} \def\rgetns{\rule{get}{ns}} \def\rputns{\rule{put}{ns}} +\def\rinputns{\rule{input}{ns}} \def\rexecns{\rule{exec}{ns}} % Common names |