summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--analyse.tex101
-rw-r--r--intro.tex1
-rw-r--r--introcoms.tex5
-rw-r--r--org.tex10
-rw-r--r--rulesget.tex2
-rw-r--r--smurf.sty5
-rw-r--r--sosexamp.tex61
-rw-r--r--werkstuk.tex2
8 files changed, 100 insertions, 87 deletions
diff --git a/analyse.tex b/analyse.tex
index d945340..9c14a49 100644
--- a/analyse.tex
+++ b/analyse.tex
@@ -1,8 +1,10 @@
% vim: set spelllang=nl:
\section{Analyse}
\label{sec:analyse}
+
Als analyse willen we graag een stuk code dat een string omdraait bekijken aan
de hand van onze semantiekregels. Deze code ziet er als volgt uit:
+
\begin{smurf}
\footnotesize
"+"i+ ""p ""gtg ""gt "i"p\\
@@ -12,8 +14,10 @@ de hand van onze semantiekregels. Deze code ziet er als volgt uit:
"\textbackslash{}"i\textbackslash{}"p\textbackslash{}"\textbackslash{}""+ ""gq+ ""g+ ""p "" "+" "i"g+ pgx
\end{smurf}
-Omgezet naar onze leesbare (hier een relatief begrip) syntax ziet de code er zo uit:
+Omgezet naar onze leesbare (hier een relatief begrip) syntax ziet de code er zo
+uit:
+%todo leesbaarheid betekent ook witregels waar logisch
\begin{smurf}
\footnotesize
@@ -70,8 +74,8 @@ Omgezet naar onze leesbare (hier een relatief begrip) syntax ziet de code er zo
\end{smurf}
-Nu laten we zien dat deze code daadwerkelijk alle mogelijke strings omdraait, oftewel:\\
-Er is een derivatieboom voor
+Nu laten we zien dat deze code daadwerkelijk alle mogelijke strings omdraait,
+oftewel: er is een afleidingsboom voor
$$
\trans
{Programma}{[s:\Nil]}{(\Nil,\emptystore)}
@@ -81,52 +85,49 @@ voor alle s, waar
$$(c~s)^R=s^R c$$
$$\lambda^R=\lambda$$
-Dit bewijzen we door middel van inductie op de lengte van s.
+\begin{proof}[Bewijs]
+ Met inductie naar de lengte van $s$.
-Basisgeval: s = $\lambda$
-$$%Todo fix dit
-\begin{prooftree}
- \[
- \[
- \[
- \[
- test
- \justifies
- \trans
- {\StmPut : \StmPush~\lambda : ...~}{\Nil}{([\lambda:["+":\Nil]], \emptystore)}
- {\Nil}{\lambda}{\st}
- \using{\rputns}
- \]
- \justifies
- \trans
- {\StmPush~\lambda : \StmPut : ...~}{\Nil}{(["+":\Nil], \emptystore)}
- {\Nil}{\lambda}{\st}
- \using{\rpushns}
- \]
- \justifies
- \trans
- {\StmCat : \StmPush~\lambda : ...~}{\Nil}{([\lambda:["+":\Nil]], \emptystore)}
- {\Nil}{\lambda}{\st}
- \using{\rcatns}
- \]
- \justifies
- \trans
- {\StmInput : \StmCat : ...~}{[\lambda:\Nil]}{(["+":\Nil], \emptystore)}
- {\Nil}{\lambda}{\st}
- \using{\rinputns}
- \]
- \justifies
- \trans
- {\StmPush~"+" : \StmInput : ...~}{[\lambda:\Nil]}{(\Nil,\emptystore)}
- {\Nil}{\lambda}{\st}
- \using{\rpushns}
-\end{prooftree}
-$$
+ Basisgeval: $s=\lambda$.
-
-We willen hierbij een stuk code onderzoeken dat volgens de specificaties geen
-eenduidige uitkomst heeft. Het liefst willen we eens stuk code bedenken waarbij
-onder verschillende interpretaties van de specificaties een geheel andere
-uitkomst mogelijk is. Wellicht kunnen we daarna nieuwe specificaties (gebaseerd
-op de bestaande specificaties) maken die wel eenduidig zijn en aansluiten op
-onze semantiekregels.
+ $$%Todo fix dit
+ \begin{prooftree}
+ \[
+ \[
+ \[
+ \[
+ \vdots %todo afmaken
+ \justifies
+ \trans
+ {\StmPut : \StmPush~\lambda : ...~}{\Nil}{([\lambda:["+":\Nil]], \emptystore)}
+ {\Nil}{\lambda}{\st}
+ \using{\rputns}
+ \]
+ \justifies
+ \trans
+ {\StmPush~\lambda : \StmPut : ...~}{\Nil}{(["+":\Nil], \emptystore)}
+ {\Nil}{\lambda}{\st}
+ \using{\rpushns}
+ \]
+ \justifies
+ \trans
+ {\StmCat : \StmPush~\lambda : ...~}{\Nil}{([\lambda:["+":\Nil]], \emptystore)}
+ {\Nil}{\lambda}{\st}
+ \using{\rcatns}
+ \]
+ \justifies
+ \trans
+ {\StmInput : \StmCat : ...~}{[\lambda:\Nil]}{(["+":\Nil], \emptystore)}
+ {\Nil}{\lambda}{\st}
+ \using{\rinputns}
+ \]
+ \justifies
+ \trans
+ {\StmPush~"+" : \StmInput : ...~}{[\lambda:\Nil]}{(\Nil,\emptystore)}
+ {\Nil}{\lambda}{\st}
+ \using{\rpushns}
+ \end{prooftree}
+ $$
+
+ %todo afmaken
+\end{proof}
diff --git a/intro.tex b/intro.tex
index 6f99329..8812eca 100644
--- a/intro.tex
+++ b/intro.tex
@@ -63,4 +63,3 @@ illustreren met een voorbeeld:
\input{introcoms}
\input{introexmp}
\input{org}
-
diff --git a/introcoms.tex b/introcoms.tex
index 31f2de0..d12f14a 100644
--- a/introcoms.tex
+++ b/introcoms.tex
@@ -5,7 +5,10 @@ We zullen nu kort op informele wijze de verschillende commando's in Smurf
beschrijven. We geven telkens de notatie in Smurf syntax en een leesbaarder
alternatief dat we hieronder zullen gebruiken. Wanneer een commando iets met
elementen op de stack doet, worden die elementen altijd verwijderd.
-Merk op dat de commando's niet exact hetzelfde zijn als in de voorbeeldprogramma's en de taalspecificatie; wij gebruiken een leesbaardere variant op de taal zodat het overzichtelijker is om eigenschappen ervan te bespreken. Alle commando's betekenen nog steeds hetzelfde.
+Merk op dat de commando's niet exact hetzelfde zijn als in de
+voorbeeldprogramma's en de taalspecificatie. We gebruiken een leesbaardere
+variant op de taal zodat het overzichtelijker is om eigenschappen ervan te
+bespreken. Alle commando's betekenen nog steeds hetzelfde.
\begin{description}[style=nextline,font=\normalfont]
\item[\smurfinline{"..."} of $\StmPush~\texttt{...}$]
diff --git a/org.tex b/org.tex
index dff2a3e..a13f0ae 100644
--- a/org.tex
+++ b/org.tex
@@ -5,10 +5,12 @@ In \autoref{sec:def} beschrijven we formele definities om de semantiek van
Smurf te kunnen specificeren. We kijken naar de syntax, input en output, de
programmatoestand en de transities in de natuurlijke semantiek die we gaan
definiëren. \autoref{sec:rules} beschrijft vervolgens per statement in de
-syntax de formele semantiek. Hierbij baseren we ons op de Smurf specificatie
-\cite{safalra}, waarbij we dingen verhelderen en ongedefinieerd gedrag
-definiëren. In \autoref{sec:analyse} bekijken we een stuk code aan de hand van
-de gedefinieerde regels.
+syntax de formele natuurlijke semantiek. Hierbij baseren we ons op de Smurf
+specificatie \cite{safalra}, waarbij we dingen verhelderen en ongedefinieerd
+gedrag definiëren. In \autoref{sec:sos} laten we zien wat voor regels we zouden
+moeten gebruiken als we structurele operationele semantiek zouden gebruiken. In
+\autoref{sec:analyse} bekijken we een stuk code aan de hand van de
+gedefinieerde regels.
\autoref{sec:planning} bevat een planning voor het afwerken van het werkstuk,
die uiteindelijk verwijderd zal worden.
diff --git a/rulesget.tex b/rulesget.tex
index 2fec68c..44daa5f 100644
--- a/rulesget.tex
+++ b/rulesget.tex
@@ -1,6 +1,6 @@
% vim: set spelllang=nl:
\subsection{\texttt{Get}}
-\label{sec:rules:exec}
+\label{sec:rules:get}
\begin{quote}
g - Pops a variable name from the stack, and pushes the value of the
diff --git a/smurf.sty b/smurf.sty
index c226f32..aacea8e 100644
--- a/smurf.sty
+++ b/smurf.sty
@@ -74,9 +74,10 @@
\def\rinputns{\rule{input}{ns}}
\def\routputns{\rule{output}{ns}}
\def\rexecns{\rule{exec}{ns}}
+
\def\rtailsos{\rule{tail}{sos}}
-\def\rcompeensos{\rule{comp1}{sos}}
-\def\rcomptweesos{\rule{comp2}{sos}}
+\def\rcompeensos{\rule{comp$^1$}{sos}}
+\def\rcomptweesos{\rule{comp$^2$}{sos}}
% Common names
\def\stk{\mathit{stk}}
diff --git a/sosexamp.tex b/sosexamp.tex
index d05ae3a..cb2cbb2 100644
--- a/sosexamp.tex
+++ b/sosexamp.tex
@@ -1,54 +1,61 @@
-\subsection{Smurf in structurele operationele semantiek}
-We willen ook nog graag laten zien hoe de definities van Smurf eruit zien als je de structurele operationele semantiek gebruikt. In principe maakt het voor de analyse van Smurf niet uit of je natuurlijke semantiek gebruikt of structurele operationele semantiek. Omdat natuurlijke semantiek en structurele operationele semantiek equivalent zijn wanneer de regels goed gedefineerd zijn. Wij hadden een voorkeur om natuurlijke semantiek te gebruiken omdat we hier meer bekend mee zijn. Echter willen we ook nog graag laten zien hoe het eruit zou zien als je structurele operationele semantiek zou gebruiken.
+% vim:set spelllang=nl:
+\section{Smurf in structurele operationele semantiek}
+\label{sec:sos}
+We willen ook nog graag laten zien hoe de definities van Smurf eruit zien als
+je de structurele operationele semantiek gebruikt. In principe maakt het voor
+de analyse van Smurf niet uit of je natuurlijke semantiek gebruikt of
+structurele operationele semantiek. Omdat natuurlijke semantiek en structurele
+operationele semantiek equivalent zijn wanneer de regels goed gedefinieerd
+zijn. Wij hadden een voorkeur om natuurlijke semantiek te gebruiken omdat we
+hier meer bekend mee zijn. Echter willen we ook nog graag laten zien hoe het
+eruit zou zien als je structurele operationele semantiek zou gebruiken.
-We gebruiken hier in plaats van de lambda regel twee compositie regels om hiervan ook het verschil aan te geven.
+We gebruiken hier in plaats van de labdaregel twee compositieregels om hiervan
+ook het verschil aan te geven.
+
+De twee compositieregels zijn als volgt:
-De twee composities regels zijn als volgt:
-\medskip
-\medskip
$$
\begin{prooftree}
\sostrans
- {\pgm1}{\ip}{\op}{(\stk, \str)}
- {\pgm1'}{\ip'}{\op'}{(\stk', \str')}
+ {\stm}{\ip}{\op}{(\stk, \str)}
+ {\pgm'}{\ip'}{\op'}{(\stk', \str')}
\justifies
\sostrans
- {\pgm1:\pgm2}{\ip}{\op}{(\stk,\str)}
- {\pgm1':\pgm2}{\ip'}{\op'}{(\stk',\str')}
+ {\stm:\pgm}{\ip}{\op}{(\stk,\str)}
+ {\pgm'}{\ip'}{\op'}{(\stk',\str')}
\using{\rcompeensos}
\qquad
\end{prooftree}
$$
+
\medskip
-\medskip
$$
\begin{prooftree}
\sostranseind
- {\pgm1}{\ip}{\op}{(\stk, \str)}
+ {\stm}{\ip}{\op}{(\stk, \str)}
{\ip'}{\op'}{(\stk', \str')}
\justifies
\sostrans
- {\pgm1:\pgm2}{\ip}{\op}{(\stk,\str)}
- {\pgm2}{\ip'}{\op'}{(\stk',\str')}
+ {\stm:\pgm}{\ip}{\op}{(\stk,\str)}
+ {\pgm}{\ip'}{\op'}{(\stk',\str')}
\using{\rcomptweesos}
\qquad
\end{prooftree}
$$
-\medskip
-\medskip
-\medskip
-
-De tailregel zal in de structurele operationele semantiek als volgt zijn:
+\bigskip
+De regel voor $\StmTail$ zou in de structurele operationele semantiek als volgt
+zijn:
$$
\begin{prooftree}
- \axjustifies
- \sostranseind
- {\StmTail}{\ip}{\op}{(\stk,\str)}
- {\ip}{\op}{(\push{s}{\stk'}, \str)}
- \using{\rtailsos}
- \qquad
- \text{met $ \pop{\stk} = (c~s,\stk') $.}
+ \axjustifies
+ \sostranseind
+ {\StmTail}{\ip}{\op}{(\stk,\str)}
+ {\ip}{\op}{(\push{s}{\stk'}, \str)}
+ \using{\rtailsos}
+ \qquad
+ \text{met $\pop{\stk} = (c~s,\stk')$.}
\end{prooftree}
-$$ \ No newline at end of file
+$$
diff --git a/werkstuk.tex b/werkstuk.tex
index 8289f6f..fd43b0c 100644
--- a/werkstuk.tex
+++ b/werkstuk.tex
@@ -47,8 +47,8 @@
\input{intro}
\input{def}
\input{rules}
-\input{analyse}
\input{sosexamp}
+\input{analyse}
\input{planning}
\input{refs}