1 files changed, 88 insertions, 0 deletions
diff --git a/task2.tex b/task2.tex
new file mode 100644
index 0000000..a85aa89
--- /dev/null
+++ b/task2.tex
@@ -0,0 +1,88 @@
+\documentclass[a4paper,9pt]{article}
+
+\usepackage[dutch]{babel}
+\usepackage{geometry}
+
+\author{Camil Staps}
+\title{Semantiek \& Correctheid\\\Large{Leertaak 2}}
+
+\usepackage{senc}
+\usepackage{prooftree} 
+\usepackage{alltt}
+\usepackage{stmaryrd}
+\usepackage[figuresleft]{rotating}
+\usepackage{mathdots}
+
+%\renewcommand{\trans}[3]{#1} 
+
+\begin{document}
+
+\maketitle
+
+\section*{Opdracht 2.3}
+Zie Figuur \ref{fig:boom}.
+Hier geldt:
+
+\begin{align*}
+    s_0 &= [x\mapsto17, y\mapsto5]\\ %todo
+    s_1 &= s_0[z\mapsto0]\\
+    s_2 &= s_1[z\mapsto1]\\
+    s_3 &= s_2[x\mapsto12]\\
+    s_{13} &= s_3[z\mapsto6,x\mapsto-13].
+\end{align*}
+
+\begin{sidewaysfigure}
+  \scriptsize
+  $$
+  \begin{prooftree}
+      \[
+        \axjustifies \trans{\sass{z}{0}}{s_0}{s_1} \using{\rassp}
+      \]\quad
+      \[
+        \[
+          \[\axjustifies \trans{\sass{z}{z+1}}{s_1}{s_2} \using{\rassp}\]\quad
+          \[\axjustifies \trans{\sass{x}{x-y}}{s_2}{s_3} \using{\rassp}\]
+          \justifies \trans{\scomp{\sass{z}{z+1}}{\sass{x}{x-y}}}{s_1}{s_3} \using{\rcomp}
+        \]\quad
+        \[\vdots\quad
+          \[
+            \[
+              \axjustifies \trans{\swhile{y\le x}{(\scomp{\sass{z}{z+1}}{\sass{x}{x-y}})}}{s_{13}}{s_{13}}%todo
+              \using{\rwhileff}
+            \]
+            \justifies \iddots \using{\rwhilett}
+          \]
+          \axjustifies
+          \trans{\swhile{y\le x}{(\scomp{\sass{z}{z+1}}{\sass{x}{x-y}})}}{s_3}{s_{13}}
+        \]
+        \justifies \trans{\swhile{y\le x}{(\scomp{\sass{z}{z+1}}{\sass{x}{x-y}})}}{s_1}{s_{13}}
+        \using{\rwhilett}
+      \]
+      \justifies \trans{\scomp{\sass{z}{0}}{\swhile{y\le x}{(\scomp{\sass{z}{z+1}}{\sass{x}{x-y}})}}}{s_0}{s_{13}}
+      \using{\rcomp}
+  \end{prooftree}
+  $$
+  \caption{Afleidingsboom voor opgave 2.3}
+  \label{fig:boom}
+\end{sidewaysfigure}
+
+\section*{Het \texttt{do} statement}
+\subsection*{Syntax}
+We voegen een regel $S ::= \sdowhile{S}{b}$ toe.
+
+\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}
+\end{prooftree}$$
+
+\section*{Opdracht 2.4}
+\begin{itemize}
+    \item Termineert als $x\ge1$, anders niet.
+    \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).
+\end{itemize}
+
+\end{document}
+