Task 6

2 files changed, 100 insertions, 0 deletions

diff --git a/senc.sty b/senc.sty
index 9a6af38..f6e15d8 100644
--- a/senc.sty
+++ b/senc.sty
@@ -6,6 +6,7 @@
 \def\s{s\;}
 
 \def\x{\mathtt{x}}
+\def\y{\mathtt{y}}
 
 \def\tt{\mathbf{tt}}
 \def\ff{\mathbf{ff}}
@@ -25,3 +26,16 @@
 %\renewcommand{\allttsub}[1]{\begin{math}_{\textcolor{red}{#1}}\end{math}}
 \renewcommand{\psqan}[5]{\{#1\}^{\textcolor{red}{#4}}\espace #2 \espace \{#3\}^{\textcolor{red}{#5}}}
 
+\newcommand{\transl}[2]{\langle #1, #2\rangle}
+\newcommand{\sfor}[4]{\mbox{\texttt{for~}}\sass#1#2\mbox{\texttt{~to~}}#3\mbox{\texttt{~do~}}#4}
+\newcommand{\sassert}[2]{\mbox{\texttt{assert~}}#1\mbox{\texttt{~before~}}#2}
+\newcommand{\sabort}{\mbox{\texttt{abort}}}
+
+\def\rcompsos#1{[\mbox{comp}_{\mbox{\footnotesize{sos}}}^{#1}]}
+\def\rasssos{[\mbox{ass}_{\mbox{\footnotesize{sos}}}]}
+\def\rskipsos{[\mbox{skip}_{\mbox{\footnotesize{sos}}}]}
+\def\rifsos#1{[\mbox{if}_{\mbox{\footnotesize{sos}}}^{\mbox{\footnotesize{#1}}}]}
+\def\rwhilesos{[\mbox{while}_{\mbox{\footnotesize{sos}}}]}
+
+\def\rassert{[\mbox{assert}_{\mbox{\footnotesize{sos}}}]}
+
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}
+