From c9dd036a671fe348e16ef407617e1ecda9e79c81 Mon Sep 17 00:00:00 2001
From: Camil Staps
Date: Tue, 15 Mar 2016 08:07:59 +0100
Subject: Task 6

---
 task6.tex | 86 +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 86 insertions(+)
 create mode 100644 task6.tex

(limited to 'task6.tex')

diff --git a/task6.tex b/task6.tex
new file mode 100644
index 0000000..09b585f
--- /dev/null
+++ b/task6.tex
@@ -0,0 +1,86 @@
+\documentclass[landscape,a4paper,9pt]{article}
+
+\usepackage[dutch]{babel}
+\usepackage{geometry}
+
+\author{Camil Staps}
+\title{Semantiek \& Correctheid\\\Large{Leertaak 6}}
+
+\usepackage{senc}
+\usepackage{amsthm}
+
+\begin{document}
+
+\maketitle
+
+\section*{Opdracht 2.16}
+
+\def\assA{\sass{z}{z+1}}
+\def\assB{\sass{x}{x-y}}
+\def\whileBody{\scomp\assA\assB}
+\def\whileLoop{\swhile{y\leq x}{(\whileBody)}}
+\def\whileComp{\scomp\whileBody\whileLoop}
+\def\ifLoop{\sifthenelse{y\leq x}{(\whileComp)}\sskip}
+
+\def\s#1#2#3{[#1,#2,#3]}
+
+\begin{align*}
+           & \transl{\scomp{\sass{z}{0}}{\whileLoop}}{[x\mapsto17,y\mapsto5]} \\
+  \dimpl\> & \transl\whileLoop{\s{17}50} \\
+  \dimpl\> & \transl\ifLoop{\s{17}50} \\
+  \dimpl\> & \transl\whileComp{\s{17}50} \\
+  \dimpl\> & \transl{\scomp\assB\whileLoop}{\s{17}51} \\
+  \dimpl\> & \transl\whileLoop{\s{12}51} \\
+  \dimpl\> & \transl\ifLoop{\s{12}51} \\
+  \dimpl\> & \transl\whileComp{\s{12}51} \\
+  \dimpl\> & \transl{\scomp\assB\whileLoop}{\s{12}52} \\
+  \dimpl\> & \transl\whileLoop{\s752} \\
+  \dimpl\> & \transl\ifLoop{\s752} \\
+  \dimpl\> & \transl\whileComp{\s752} \\
+  \dimpl\> & \transl{\scomp\assB\whileLoop}{\s753} \\
+  \dimpl\> & \transl\whileLoop{\s253} \\
+  \dimpl\> & \transl\ifLoop{\s253} \\
+  \dimpl\> & \transl\sskip{\s253} \\
+  \dimpl\> & \s253,
+\end{align*}
+waar $\s{a}{b}{c}$ kort is voor $[x\mapsto a,y\mapsto b,z\mapsto c]$.
+
+\medskip
+Een toestand $s$ waarvoor de afleidingsrij van $\scomp{\sass{z}0}\whileLoop$ en $s$ oneindig is, is bijvoorbeeld $s=[x\mapsto0,y\mapsto0]$.
+
+\section*{Opdracht 2.18}
+\begin{alignat*}{3}
+  [\text{for}^\text{tt}_\text{sos}]\quad & \transl{\sfor{x}{a_1}{a_2}{S}}{s} \dimpl \transl{\scomp{\sass{x}{a_1}}\scomp{S}{{\sfor{x}{a_1+1}{a_2}{S}}}}{s} && \text{~if~} a_1 \le a_2 \\
+  [\text{for}^\text{ff}_\text{sos}]\quad & \transl{\sfor{x}{a_1}{a_2}{S}}{s} \dimpl \transl{S}{s} && \text{~if~} a_1 \geq a_2
+\end{alignat*}
+
+\section*{Opdracht 2.21}
+Volgt dit niet direct uit $\rcompsos2$?
+%\begin{proof}
+%  In het geval dat $k=0$ is dit overduidelijk waar.
+%
+%  Stel dat voor $k\leq k_0$ geldt dat als $\transl{S_1}s\dimpl^ks'$, dan $\transl{\scomp{S_1}{S_2}}s\dimpl^k\transl{S_2}{s'}$ (\textbf{IH}).
+%\end{proof}
+
+\section*{Semantische equivalentie}
+De definitie van semantische equivalentie is beter met een conjunctie dan met een disjunctie. Anders zouden alle paren statements $S_1,S_2$ equivalent zijn terwijl er toestanden zijn waarbij de twee statements na een eindig aantal stappen in verschillende toestanden $\gamma\neq\gamma'$ terechtkomen, die beide terminaal zijn, omdat dan de tweede conditie in de definitie waar is.
+
+\section*{Opdracht 2.32}
+$$S ::= \dots \mid \sassert{b}{S}$$
+$$\rassert \quad \transl{\sassert{b}{S}}{s} \dimpl \transl{\sifthenelse{b}{S}{\sabort}}{s}$$
+
+\section*{Opdracht 2.33}
+In het geval van natuurlijke semantiek kunnen we in elke toestand $s$ terechtkomen waarvoor geldt dat $s~x>0$.
+
+In het geval van structureel operationele semantiek hebben we afleidingsrijen van de volgende vormen:
+
+\def\orwhile{\swhile{x\leq0}{\sor{\sass{x}{x-1}}{\sass{x}{(-1)\cdot x}}}}
+\begin{align*}
+  \transl{\scomp{\sass{x}{-1}}\orwhile}s \dimpl^* & s \quad\text{met $s~x>0$;}\\
+  \transl{\scomp{\sass{x}{-1}}\orwhile}s \dimpl^* & \transl{\orwhile}s \\
+                                         \dimpl\enspace & \dots\\
+\end{align*}
+Volgens mij zijn de twee semantieken voor dit statement dus \emph{niet} gelijk, want natuurlijke semantiek garandeert dat het statement op elke toestand termineert, terwijl structureel operationele semantiek dit niet doet.
+
+\end{document}
+
-- 
cgit v1.2.3

