summaryrefslogtreecommitdiff
path: root/rulesoutput.tex
blob: d4bb487312e33e56300270434512032755fa758f (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
% vim: set spelllang=nl:
\subsection{\texttt{Output}}

\begin{quote}
	o - Output the string at the top of the stack
\end{quote}

Net als bij het inputcommando gaan we op een abstracte wijze met de output om.
We houden gedurende het hele programma een stack van strings, genaamd $\Output$
bij waar het programma zijn output naar wegschrijft.

Dit geeft de volgende regel:

$$
\prooftree
        \trans
        {\pgm}{\ip}{(\stk',\str)}
        	{\ip'}{\op}{\st}
	\justifies
        \trans
        {\StmOutput:\pgm}{\ip}{(\stk,\str)}
            {\ip'}{\push{s}{\op}}{\st}
	\using{\routputns}
	\qquad
	\text{met $\pop{\stk} = (s,\stk') $,}
\endprooftree
$$

waarbij $\op$ in de bovenste regel de gehele outputstack weergeeft. Merk op
dat eenzelfde regel waar $s$ niet voor op de stack wordt gezet maar achter,
even geldig is. Geen van beide opties is beter dan de ander omdat we geen
aannames doen over hoe de $\Output$-stack wordt verwerkt.