diff options
author | W-M-T | 2016-04-29 15:10:55 +0200 |
---|---|---|
committer | W-M-T | 2016-04-29 15:10:55 +0200 |
commit | 42c9484ca61ca7595c715efd109e8fe5d92b0b7f (patch) | |
tree | 2bcff1858670e59de5586dd0e8dc7f7c3c5de1ed /rulesoutput.tex | |
parent | Nederlandse namen voor section en subsection (diff) |
Output rule
Diffstat (limited to 'rulesoutput.tex')
-rw-r--r-- | rulesoutput.tex | 30 |
1 files changed, 30 insertions, 0 deletions
diff --git a/rulesoutput.tex b/rulesoutput.tex new file mode 100644 index 0000000..3f6ab0a --- /dev/null +++ b/rulesoutput.tex @@ -0,0 +1,30 @@ +% 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:\Nil]}{\st} + \justifies + \trans + {\StmOutput:\pgm}{\ip}{(\stk,\str)} + {\ip'}{[\op:[var:\Nil]]}{\st} + \using{\routputns} + \qquad + \text{met $(\var,\stk') = \pop{\stk}$.} +\endprooftree +$$ + +Merk op dat eenzelfde regel, waar $var$ niet achteraan maar vooraan zou komen te staan, even geldig is. Geen van beide opties is beter dan de ander, omdat we geen aannames doen over doe de $\Output$-stack wordt verwerkt. + |