1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
|
\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}
\allowdisplaybreaks
\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}
\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'}$ (inductiehypothese).
Stel verder dat $\transl{S_1}s \dimpl^{k+1} s''$. Dan hebben we een afleiding $\transl{S_1}s \dimpl \gamma \dimpl^k s''$ met $\gamma=\transl{S_1'}{s'}$. Dus $\transl{S_1}s \dimpl \transl{S_1'}{s'} \dimpl^k s''$.
Dan geldt volgens de inductiehypothese voor elke $S_2$ dat$\transl{\scomp{S_1'}{S_2}}{s'} \dimpl^k \transl{S_2}{s''}$.
Voor de afleiding van $\transl{\scomp{S_1}{S_2}}s$ moeten we dan $\rcompsos1$ toepassen, en dus krijgen we: $\transl{\scomp{S_1}{S_2}}s \dimpl \transl{\scomp{S_1'}{S_2}}{s'} \dimpl^k \transl{S_2}{s''}$.
Hieruit volgt dat $\transl{\scomp{S_1}{S_2}}s \dimpl^{k+1} \transl{S_2}{s''}$.
Uit het principe van volledige inductie volgt nu dat als $\transl{S_1}s \dimpl^k s'$, dan ook $\transl{\scomp{S_1}{S_2}}s \dimpl^k \transl{S_2}{s'}$, voor alle $S_1, S_2, s$ en $k\in\mathbb N$.
\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}
|
