summaryrefslogtreecommitdiff
path: root/rulesget.tex
blob: 44daa5fd7818679f9b65ec5d9b85e1f5de15f9eb (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
% vim: set spelllang=nl:
\subsection{\texttt{Get}}
\label{sec:rules:get}

\begin{quote}
	g - Pops a variable name from the stack, and pushes the value of the
	variable.
\end{quote}

De regel voor dit statement spreekt voor zich. In het geval dat $\stk$ leeg is,
is $\pop\stk$ niet gedefinieerd en kunnen we de regel dus niet toepassen. 
$$
\begin{prooftree}
	\trans
		{\pgm}{\ip}{(\push{\str~\var}{\stk'}, \str)}
		{\ip'}{\op}{\st}
	\justifies
	\trans
		{\StmGet:\pgm}{\ip}{(\stk,\str)}
		{\ip'}{\op}{\st}
	\using{\rgetns}
	\qquad
	\text{met $\pop{\stk}= (\var,\stk')$.}
\end{prooftree}
$$