diff options
author | Camil Staps | 2016-02-16 10:28:20 +0100 |
---|---|---|
committer | Camil Staps | 2016-02-16 10:28:20 +0100 |
commit | fcc62f10bc11948534a4571a052ee87e0627d4f4 (patch) | |
tree | d2e0f17a44c63fed73ceca0f9185842e19b8c490 | |
parent | Task 2 (diff) |
Fix task 2
-rw-r--r-- | task2.tex | 13 |
1 files changed, 6 insertions, 7 deletions
@@ -24,7 +24,7 @@ Zie Figuur \ref{fig:boom}. Hier geldt: \begin{align*} - s_0 &= [x\mapsto17, y\mapsto5]\\ %todo + s_0 &= s[x\mapsto17, y\mapsto5]\\ %todo s_1 &= s_0[z\mapsto0]\\ s_2 &= s_1[z\mapsto1]\\ s_3 &= s_2[x\mapsto12]\\ @@ -68,20 +68,19 @@ Hier geldt: \section*{Het \texttt{do} statement} \subsection*{Syntax} -We voegen een regel $S ::= \sdowhile{S}{b}$ toe. +$S ::= \ldots \mid \sdowhile{S}{b}$. \subsection*{Semantiek} -$$\trans{\sdowhile{S}{b}}{s}{s} \axif{\B{b}s=\ff}$$ $$\begin{prooftree} -\trans{S}{s}{s'} \quad \trans{\sdowhile{S}{b}}{s'}{s''} -\justifies \trans{\sdowhile{S}{b}}{s}{s''} \ruleif{\B{b}s=\tt} +\trans{S}{s}{s'} \quad \trans{\swhile{b}{S}}{s'}{s''} +\justifies \trans{\sdowhile{S}{b}}{s}{s''} \end{prooftree}$$ \section*{Opdracht 2.4} \begin{itemize} - \item Termineert als $x\ge1$, anders niet. + \item Termineert op toestanden $s$ waarvoor $s(x)\ge1$. Loopt op alle andere toestanden. \item Idem. - \item Termineert niet. $\B{\mtrue}=\tt$, dus we gebruiken $\rwhilett$. Aangezien {\sskip} de toestand niet verandert kunnen we dus $\swhile{\mtrue}{\sskip}$ afleiden, waarna we weer hetzelfde kunnen doen (en blijven doen). + \item Loopt op alle toestanden. $\B{\mtrue}=\tt$, dus we gebruiken $\rwhilett$. Aangezien {\sskip} de toestand niet verandert kunnen we dus $\swhile{\mtrue}{\sskip}$ afleiden, waarna we weer hetzelfde kunnen doen (en blijven doen). \end{itemize} \end{document} |