diff options
| -rw-r--r-- | defio.tex | 4 | ||||
| -rw-r--r-- | defstate.tex | 13 | ||||
| -rw-r--r-- | rules.tex | 2 | ||||
| -rw-r--r-- | rulesget.tex | 16 | ||||
| -rw-r--r-- | rulesput.tex | 23 | ||||
| -rw-r--r-- | smurf.sty | 8 |
6 files changed, 58 insertions, 8 deletions
@@ -15,10 +15,12 @@ Op een stack zijn twee instructies gedefinieerd: \begin{gather*} \pushop : a \times \Stack{a} \to \Stack{a} \\ \push{e}{s} \isdef [e:s] \\[1em] - \popop : \Stack{a} \to a \times \Stack{a} \\ + \popop : \Stack{a} \hookrightarrow a \times \Stack{a} \\ \pop{[e:s]} \isdef (e,s) \\ \end{gather*} +$\popop$ is een partiële functie omdat $\pop\Nil$ niet gedefinieerd is. + \medskip We zullen de input en output beide als $\Stack{\String}$ modelleren. In feite zal zelfs blijken dat we op $\Input$ de operatie $\pushop$ niet nodig hebben, diff --git a/defstate.tex b/defstate.tex index 3ff1a79..4dee41e 100644 --- a/defstate.tex +++ b/defstate.tex @@ -16,3 +16,16 @@ $\lambda$ in overeenstemming met de documentatie \cite{safalra}: variable values are initially set to the empty string. \end{quote} +Om de waarde van een key $k$ uit store $\str$ te halen gebruiken we simpelweg +$\str~k$. Vervolgens definiëren we $\putop:\SynString \times \SynString \times +(\String\to\String) \to (\String\to\String)$ die gegeven een variabelenaam, een +waarde en een oude store een nieuwe store oplevert: + +$$ + \put{\var}{\val}{\str} k = + \begin{cases} + \val & \text{als $k=\var$} \\ + \str~k & \text{als $k\ne\var$} + \end{cases} +$$ + @@ -17,8 +17,8 @@ Smurfprogramma's makkelijker zal maken. %\input{rulestail} %\input{rulesquotify} %\input{rulescat} -%\input{rulesput} \input{rulesget} +\input{rulesput} %\input{rulesinput} %\input{rulesoutput} %\input{rulesexec} diff --git a/rulesget.tex b/rulesget.tex index b61b764..f8810a7 100644 --- a/rulesget.tex +++ b/rulesget.tex @@ -1,19 +1,27 @@ % vim: set spelllang=nl: \subsection{\texttt{Get}} -$\StmGet$ neemt het bovenste element van de stack en gebruikt dit als -variabelenaam om in de variable store te zoeken. +\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. Omdat +$\StmGet$ geen IO gebruikt kunnen we $\ip$, $\ip'$ en $\op$ direct doorgeven. $$ \begin{prooftree} \trans - {\pgm}{\ip}{([\str~\var:\stk], \str)} + {\pgm}{\ip}{(\push{\str~\var}{\stk}, \str)} {\ip'}{\op}{\st} \justifies \trans - {\StmGet:\pgm}{\ip}{([\var:\stk],\str)} + {\StmGet:\pgm}{\ip}{(\stk,\str)} {\ip'}{\op}{\st} \using{\rgetns} + \qquad + \text{met $(\var,\stk') = \pop{\stk}$.} \end{prooftree} $$ diff --git a/rulesput.tex b/rulesput.tex index ce3c624..1691a5b 100644 --- a/rulesput.tex +++ b/rulesput.tex @@ -1,9 +1,30 @@ % vim: set spelllang=nl: \subsection{\texttt{Put}} +\begin{quote} + p - Pops a variable name from the stack, pops a value from the stack, and + assigns that value to the variable name. +\end{quote} + +We halen twee strings van de stack en gebruiken $\putop$ om een nieuwe variable +store te krijgen. Hiermee wordt de rest van het programma uitgevoerd. Als er +minder dan twee elementen op de stack staan kan deze regel niet worden +toegepast, aangezien $\popop$ een partiële functie is. + $$ \begin{prooftree} - hallo + \trans + {\pgm}{\ip}{(\stk'', \put\var\val\str)} + {\ip'}{\op}{\st} + \justifies + \trans + {\StmPut:\pgm}{\ip}{(\stk,\str)} + {\ip'}{\op}{\st} + \using{\rputns} + \qquad + \text{met\enspace + \parbox{36mm}{$(\var,\stk') = \pop{\stk}$,\\$(\val,\stk'') = \pop{\stk'}$.} + } \end{prooftree} $$ @@ -10,7 +10,7 @@ \def\String{\mathit{String}} \def\Char{\mathit{Char}} -% Stacks +% Stack \def\Stack#1{\mathbf{Stack}\left[\mathit{#1}\right]} \def\Nil{\texttt{Nil}} \def\pushop{\mathit{push}} @@ -18,6 +18,10 @@ \def\push#1#2{\pushop\left(#1, #2\right)} \def\pop#1{\popop\left(#1\right)} +% Store +\def\putop{\mathit{put}} +\def\put#1#2#3{\putop\left(#1, #2, #3\right)} + % Syntax \def\SynPgm{\langle\Pgm\rangle} \def\SynStm{\langle\Stm\rangle} @@ -43,6 +47,7 @@ % Rules \def\rule#1#2{[\mbox{#1}_{\mbox{\footnotesize{#2}}}]} \def\rgetns{\rule{get}{ns}} +\def\rputns{\rule{put}{ns}} % Common names \def\stk{\mathit{stk}} @@ -53,4 +58,5 @@ \def\stm{\mathit{stm}} \def\st{\mathit{st}} \def\var{\mathit{var}} +\def\val{\mathit{val}} |