diff options
| -rw-r--r-- | analyse.tex | 101 | ||||
| -rw-r--r-- | intro.tex | 1 | ||||
| -rw-r--r-- | introcoms.tex | 5 | ||||
| -rw-r--r-- | org.tex | 10 | ||||
| -rw-r--r-- | rulesget.tex | 2 | ||||
| -rw-r--r-- | smurf.sty | 5 | ||||
| -rw-r--r-- | sosexamp.tex | 61 | ||||
| -rw-r--r-- | werkstuk.tex | 2 |
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} @@ -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{...}$] @@ -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 @@ -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} |