summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorCamil Staps2016-02-16 10:28:20 +0100
committerCamil Staps2016-02-16 10:28:20 +0100
commitfcc62f10bc11948534a4571a052ee87e0627d4f4 (patch)
treed2e0f17a44c63fed73ceca0f9185842e19b8c490
parentTask 2 (diff)
Fix task 2
-rw-r--r--task2.tex13
1 files changed, 6 insertions, 7 deletions
diff --git a/task2.tex b/task2.tex
index a85aa89..9a2c87f 100644
--- a/task2.tex
+++ b/task2.tex
@@ -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}