blob: 9a2c87fce010f9af911f037c265eaeed80827bb9 (
plain) (
blame)
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
|
\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 &= s[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}
$S ::= \ldots \mid \sdowhile{S}{b}$.
\subsection*{Semantiek}
$$\begin{prooftree}
\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 op toestanden $s$ waarvoor $s(x)\ge1$. Loopt op alle andere toestanden.
\item Idem.
\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}
|
