diff options
| -rw-r--r-- | abs.tex | 5 | ||||
| -rw-r--r-- | analyse.tex | 2 | ||||
| -rw-r--r-- | cleansmurf-proofs.tex | 6 | ||||
| -rw-r--r-- | cleansmurf-rules.tex | 30 | ||||
| -rw-r--r-- | cleansmurf-trees.tex | 8 | ||||
| -rw-r--r-- | cleansmurf-types.tex | 39 | ||||
| -rw-r--r-- | def.tex | 11 | ||||
| -rw-r--r-- | defio.tex | 20 | ||||
| -rw-r--r-- | defmeta.tex | 2 | ||||
| -rw-r--r-- | defsyn.tex | 3 | ||||
| -rw-r--r-- | deftrans.tex | 10 | ||||
| -rw-r--r-- | intro.tex | 21 | ||||
| -rw-r--r-- | introcoms.tex | 27 | ||||
| -rw-r--r-- | introexmp.tex | 75 | ||||
| -rw-r--r-- | org.tex | 6 | ||||
| -rw-r--r-- | rules.tex | 10 | ||||
| -rw-r--r-- | rulesexec.tex | 3 | ||||
| -rw-r--r-- | rulespush.tex | 4 | ||||
| -rw-r--r-- | smurf.sty | 1 | ||||
| -rw-r--r-- | sosexamp.tex | 38 | ||||
| -rw-r--r-- | werkstuk.tex | 7 |
21 files changed, 156 insertions, 172 deletions
@@ -3,6 +3,7 @@ We beschrijven een manier om de semantiek van Smurf \cite{safalra} formeel te specificeren, om het makkelijker te maken over de taal te redeneren. Smurf is interessant, omdat het een commando heeft om een string als Smurfprogramma - uit te voeren. We bekijken de gevolgen van dit commando op de semantiek. + uit te voeren. Vervolgens laten we zien hoe de semantiek gebruikt kan worden + om over de taal te redeneren. Hiervoor introduceren we de tool + \emph{CleanSmurf}~\cite{cleansmurf}, een bewijshulp voor Smurf. \end{abstract} - diff --git a/analyse.tex b/analyse.tex index 4ed43f7..fbcf4e5 100644 --- a/analyse.tex +++ b/analyse.tex @@ -5,7 +5,7 @@ Omdat de transities van onze natuurlijke semantiek input meenemen, kunnen we alleen een afleidingsboom maken voor een programma \emph{met} een bepaalde input. Het is dus niet triviaal mogelijk een afleidingsboom te maken voor -willekeurige input. In deze sectie willen we laten zien hoe het toch mogelijk +willekeurige input. In dit hoofdstuk willen we laten zien hoe het toch mogelijk is een bewijs te leveren over een programma met een willekeurige input string, door gebruik te maken van inductie naar de lengte van de input string. We hadden hiervoor initieel een programma op de Esolang wiki gevonden dat een diff --git a/cleansmurf-proofs.tex b/cleansmurf-proofs.tex index c7b073c..1e949e4 100644 --- a/cleansmurf-proofs.tex +++ b/cleansmurf-proofs.tex @@ -18,7 +18,7 @@ zien. De bewijshulp is te vinden in de \texttt{prover} branch van \emph{CleanSmurf}~\cite{cleansmurf}. De oplossing hiervoor is complex. Waar hierboven de stack werd gemodelleerd met -een lijst van Strings, zal dit nu niet meer voldoende zijn: we moeten +een lijst van strings, zal dit nu niet meer voldoende zijn: we moeten onderscheid maken tussen \emph{literals} en \emph{bewijsvariabelen}. Voor de duidelijkheid maken we vanaf nu onderscheid tussen variabelen (elementen op de stack of in de variable store) en bewijsvariabelen (variabelen waar de @@ -30,7 +30,8 @@ bewijsvariabelen ook in een Smurfprogramma terechtkomen, omdat Smurf geen duidelijk onderscheid kent tussen variabelen en Smurfprogramma's (middels $\StmExec$ kan een variabele uitgevoerd worden). Dit laatste moet de bewijshulp ten minste deels ondersteunen: variabelen komen al snel in programma's terecht -op het moment dat iteratie gewenst is. +op het moment dat iteratie gewenst is. Zolang de variabele in een +$\StmPush$-commando wordt gebruikt kan de bewijshulp er mee omgaan. Om variabelen te modelleren definiëren we een nieuw type, \CI{Expr}: @@ -55,7 +56,6 @@ dan zal dit worden opgeslagen als \CI{EHead (Var "s")}, terwijl dit \CI{Lit "x"} zou moeten zijn als \CI{s} leeg is. Dit zijn dingen waar uiteindelijk wel op te controleren valt, maar nog niet volledig geïmplementeerd zijn. -\medskip Helaas werkt de oude functie om een boom te maken, \CI{tree}, niet meer na deze veranderingen: op een gegeven moment zal \CI{step} moeten weten wat de inhoud van een bewijsvariabele is. diff --git a/cleansmurf-rules.tex b/cleansmurf-rules.tex index 2e71c12..a2b08b7 100644 --- a/cleansmurf-rules.tex +++ b/cleansmurf-rules.tex @@ -5,26 +5,30 @@ Iedere semantiekregel vertaalt min of meer direct naar een functiealternatief voor \CI{step}. Echter, omdat we geen \CI{run}- maar een \CI{step}-functie schrijven, moeten we compositie expliciet maken. -Als voorbeeld zullen we de implementatie van $\StmHead$ bekijken. Aangezien -\CI{pop} en \CI{head} allebei een \CI{Maybe} opleveren, kunnen we de resultaten -gemakkelijk binden. Vervolgens wordt de stack geüpdate en wordt de rest van het -programma (\CI{p}) teruggegeven. De IO-toestand wordt zonder gebruik -doorgegeven. Het vierde argument hebben we niet nodig en kan dus worden -genegeerd. +Als voorbeeld zullen we de implementatie van $\StmHead$ bekijken. De +semantiekregel voor dit syntaxelement zag er als volgt uit: +\therheadns + +Aangezien \CI{pop} en \CI{head} allebei een \CI{Maybe} opleveren, kunnen we de +resultaten gemakkelijk monadisch \emph{bind}en. Vervolgens wordt de stack +geüpdatet en wordt de rest van het programma (\CI{p}) teruggegeven. De +IO-toestand wordt zonder gebruik doorgegeven. Het vierde argument hebben we +niet nodig en kan dus worden genegeerd. \lstinputlisting[firstline=213,lastline=215]{CleanSmurf/Smurf.icl} -Andere regels, voor $\StmPush$, $\StmTail$, $\StmCat$, $\StmQuotify$ en ook -$\StmPut$ en $\StmGet$ gaan op soortgelijke wijze. Ook $\StmInput$ en -$\StmOutput$ kunnen op dezelfde manier worden geschreven, afgezien van het feit -dat de IO-toestand en -functies gebruikt moeten worden. +Andere regels, voor $\StmPush$, $\StmTail$, $\StmCat$ en $\StmQuotify$ gaan op +soortgelijke wijze. De commando's $\StmPut$ en $\StmGet$ hebben als enige +verschil dat ze ook op de store werken. Ook $\StmInput$ en $\StmOutput$ kunnen +op eenzelfde manier worden geschreven, afgezien van het feit dat de IO-toestand +en -functies gebruikt moeten worden. -In het geval van $\StmExec$ kunnen we handig gebruik maken van het feit dat -\CI{step} een nieuw programma oplevert: +Alleen $\StmExec$ behoeft nadere toelichting. Bij dit syntaxelement kunnen we +handig gebruik maken van het feit dat \CI{step} een nieuw programma oplevert: \lstinputlisting[firstline=228,lastline=230]{CleanSmurf/Smurf.icl} Zoals te zien wordt een nieuwe toestand gemaakt (\CI{zero}) waarin dit nieuwe programma (\CI{p}) wordt uitgevoerd. De compositie \CI{parse o fromString} -parseert een String van de stack en levert een \CI{Maybe Program} op. Dus ook +parseert een string van de stack en levert een \CI{Maybe Program} op. Dus ook deze wat afwijkende regel levert geen problemen op. diff --git a/cleansmurf-trees.tex b/cleansmurf-trees.tex index 6264697..8a7f7aa 100644 --- a/cleansmurf-trees.tex +++ b/cleansmurf-trees.tex @@ -6,11 +6,11 @@ eigenschappen van afleidingsbomen voor Smurf: \begin{itemize} \item Alle semantiekregels hebben ten hoogste één premisse, waardoor we een - boom als lijst van transities kunnen representeren. + afleidingsboom als lijst van transities kunnen representeren. \item Ieder commando heeft precies één regel. Hierdoor is aan het eerste statement van een programma te herkennen welke regel wordt toegepast. Dit hoeven we dus niet in de types \CI{Transition} en \CI{DerivationTree} op te - slaan. + slaan om het later wel in de output te kunnen tonen. \item Doordat condities van de semantiekregels enkel afhangen van de linkerkant van de conclusie (het programma, de input en de toestand), en deze informatie beschikbaar is op het moment dat de boom gemaakt wordt, @@ -36,5 +36,5 @@ het geval, dan zetten we de $\lambda$-regel zelf in de boom als \CI{([], io.input, st) --> (io.input, [], st)}. Is dit niet het geval, dan maken we recursief een boom voor de premisse -(\CI{tree pgm st io iof}). Lukt dit niet, dan kunnen we geen boom maken. -Anders, dan voegen we de boom en de transitie gevonden met \CI{step} samen. +(\CI{tree pgm st io iof}). Lukt dit niet, dan kunnen we geen boom maken. Lukt +het wel, dan voegen we de boom en de transitie gevonden met \CI{step} samen. diff --git a/cleansmurf-types.tex b/cleansmurf-types.tex index bed29e2..39b8339 100644 --- a/cleansmurf-types.tex +++ b/cleansmurf-types.tex @@ -1,12 +1,12 @@ % vim: set spelllang=nl: \subsection{Types} \label{sec:cleansmurf:types} -Het programma houdt de expressieve syntax uit \autoref{sec:def:syn} aan. Het -type \CI{Stm} is dus: +Het programma houdt de expressieve syntax uit \autoref{sec:def:syn} aan. Dit +geeft de types: \lstinputlisting[firstline=15,lastline=20]{CleanSmurf/Smurf.dcl} -We gebruiken lijsten als stacks en implementeren de store met behulp van een +We modelleren lijsten als stacks en implementeren de store met behulp van een tabel van naam-waarde paren: \lstinputlisting[firstline=22,lastline=27]{CleanSmurf/Smurf.dcl} @@ -16,28 +16,31 @@ premisse hebben, kunnen we een afleidingsboom als lijstje transities zien: \lstinputlisting[firstline=35,lastline=36]{CleanSmurf/Smurf.dcl} -Met deze definities kunnen we een \CI{step :: Program State -> Maybe (Program, -State)} definiëren. Dit komt bijna overeen met de structuur van transities. We -moeten een \CI{Program} teruggeven, omdat we slechts één stap zetten. Wat dit -betreft lijken de regels van \emph{CleanSmurf} meer op regels in structurele -operationele semantiek. We hebben al laten zien dat deze regels erg veel lijken -op die in natuurlijke semantiek. +Met deze definities zouden we een \CI{step :: Program State -> Maybe (Program, +State)} kunnen definiëren. Dit type komt bijna overeen met de structuur van +transities. We moeten echter een \CI{Program} teruggeven, omdat we slechts één +stap zetten. Wat dit betreft lijken de regels van \emph{CleanSmurf} meer op +regels in structurele operationele semantiek. We hebben al laten zien dat deze +regels niet wezenlijk afwijken van die voor de natuurlijke semantiek. -Het type van \CI{step} neemt nog geen Input/Output mee. We maken er een -overloaded functie van, zodat hij voor meerdere inputmethodes kan worden -gebruikt. Het uiteindelijke type is: +In het type van \CI{step} zit nog geen Input/Output. We maken er een overloaded +functie van, zodat hij voor meerdere inputmethodes kan worden gebruikt. Het +uiteindelijke type is dan: \lstinputlisting[firstline=56,lastline=56]{CleanSmurf/Smurf.dcl} -Hoe dit precies werkt is niet belangrijk voor de beschrijving hier. Het derde -argument, van type \CI{io}, is de `IO-toestand'. Het vierde argument, van type -\CI{IO io}, omvat een input-functie die strings oplevert (gegeven de -IO-toestand) en een output-functie die strings opneemt (in de IO-toestand). +Het derde argument, van type \CI{io}, is de `IO-toestand'. Het vierde argument, +van type \CI{IO io}, omvat een input-functie die strings oplevert (gegeven de +IO-toestand) en een output-functie die strings opneemt (in de IO-toestand). Hoe +dit precies werkt is niet belangrijk voor de beschrijving hier. \medskip -Verder definiëren we een aantal hulpfuncties: +Verder definiëren we een aantal hulpfuncties op onze types: \lstinputlisting[firstline=232,lastline=245]{CleanSmurf/Smurf.icl} De partiële functies zijn hier gesimuleerd met het \CI{Maybe}-type. Dit laat -ons monadische operatoren gebruiken in het uitwerken van de interpreter. +ons monadische operatoren gebruiken in het uitwerken van de interpreter. Wilden +we betekenisvolle error messages geven zoals de Perl-interpreter doet, dan +hadden we \CI{Either} kunnen gebruiken. Dit maakt geen verschil voor de +implementatie van de semantiekregels. @@ -2,9 +2,18 @@ \section{Definities} \label{sec:def} +De voorbeelden hierboven zijn niet erg leesbaar, wat het lastig maakt om over +Smurfprogramma's te redeneren. We defini\"eren daarom een alternatieve syntax, +die we in de rest van het werkstuk zullen gebruiken. Dit doen we in +\autoref{sec:def:syn}. Vervolgens defini\"eren we hoe we input en output +modelleren (\ref{sec:def:io}), hoe de toestand van een Smurfprogramma eruit +ziet (\ref{sec:def:state}) en wat voor transities we zullen gebruiken bij het +specificeren van Smurf in de natuurlijke semantiek (\ref{sec:def:trans}). Bij +al definities gebruiken we een aantal metavariabelen die worden beschreven in +\autoref{sec:def:meta}. + \input{defmeta} \input{defsyn} \input{defio} \input{defstate} \input{deftrans} - @@ -2,14 +2,16 @@ \subsection{Input en output} \label{sec:def:io} -Allereerst definiëren we het type $\Stack{a}$, omdat we veel met stacks -doen in onze semantiekregels. Een $\Stack{a}$ (lees: een stack van elementen -van type $a$) is een simpel datatype met de volgende syntax: +Allereerst definiëren we het type $\Stack{a}$. De stack is onmisbaar voor +nagenoeg elk Smurfprogramma en zullen we dus ook veel gebruiken in onze +semantiekregels. Een $\Stack{a}$ (lees: een stack van elementen van type $a$) +is een simpel datatype met de volgende syntax: \def\inbrackets#1{$\mathrm{[}#1\mathrm{]}$} \def\bracka{\inbrackets{a}} +\def\StackA{{\normalfont\textbf{Stack}} \bracka} \begin{grammar} - <Stack \bracka> ::= [<a>:<Stack \bracka>] | \Nil + <\StackA> ::= [<a>:<\StackA>] | \Nil \end{grammar} Op een stack zijn twee instructies gedefinieerd: @@ -21,11 +23,11 @@ Op een stack zijn twee instructies gedefinieerd: \end{gather*} In de documentatie \cite{safalra} wordt niet beschreven wat er gebeurt wanneer -een $\popop$ wordt uitgevoerd op een lege stack. In de -\emph{Perl}-interpreter van de taal wordt ervoor gekozen om het programma -abrupt te termineren met een error. Wij hebben ervoor gekozen om $\popop$ als -een partiële functie te zien waar $\pop\Nil$ ongedefinieerd blijft zodat er -geen afleidingsbomen bestaan voor programma's waar dit gebeurt. +een $\popop$ wordt uitgevoerd op een lege stack. In de Perl-interpreter van de +taal wordt ervoor gekozen om het programma abrupt te termineren met een error. +Wij hebben ervoor gekozen om $\popop$ als een partiële functie te zien waar +$\pop\Nil$ ongedefinieerd blijft zodat er geen afleidingsbomen bestaan voor +programma's waar dit gebeurt. \medskip We zullen de input en output beide als $\Stack{\String}$ modelleren. In feite diff --git a/defmeta.tex b/defmeta.tex index 05a1de1..b319c51 100644 --- a/defmeta.tex +++ b/defmeta.tex @@ -1,7 +1,7 @@ % vim: set spelllang=nl: \subsection{Metavariabelen} \label{sec:def:meta} -We zullen de volgende metavariabelen gebruiken: +We gebruiken de volgende metavariabelen: \begin{description}[labelindent=\parindent] \item[$a$] voor typen, @@ -4,8 +4,7 @@ We definiëren de volgende syntax: \setlength{\grammarindent}{5em} \begin{grammar} - <Pgm> ::= <Stm>:<Pgm> | $\lambda$ %todo over de : moet uitleg komen, waarom - %we die introduceren + <Pgm> ::= <Stm>:<Pgm> | $\lambda$ <Stm> ::= `Push' <String> \alt `Cat' | `Head' | `Tail' | `Quotify' diff --git a/deftrans.tex b/deftrans.tex index a4d5669..cd64ab2 100644 --- a/deftrans.tex +++ b/deftrans.tex @@ -1,9 +1,11 @@ % vim: set spelllang=nl: \subsection{Transities} \label{sec:def:trans} -We hebben gekozen om de semantiek van Smurf in natuurlijke semantiek te definiëren. In principe hadden we er ook voor kunnen kiezen om te gaan voor structurele operationele semantiek, dit zullen we dan ook nog even kort toelichten in \autoref{sec:sos} . Echter zal de verdere uitwerking dus in natuurlijke semantiek zijn. - -\medskip +We hebben ervoor gekozen de semantiek van Smurf in natuurlijke semantiek te +definiëren. In principe hadden we er ook voor kunnen kiezen om structurele +operationele semantiek te gebruiken. In het geval van Smurf komt dit ongeveer +op hetzelfde neer. Hoe regels voor Smurf gedefinieerd zouden kunnen worden in +structurele operationele semantiek wordt toegelicht in \autoref{sec:sos}. Bij het definiëren van de natuurlijke semantiek van Smurf zullen we de verzameling van transities als een relatie $\to$ tussen @@ -17,7 +19,7 @@ en lezen we als de geconsumeerde input.'' \end{quote} -We hebben het hele programma $\Pgm$ nodig voor de pijl, omdat één commando +We hebben het hele programma $\pgm$ nodig voor de pijl, omdat één commando ($\StmExec$) eventuele verdere statements `weggooit'. %todo ander woord Verder gebruiken we $\Input$ voor $\StmInput$ en hebben we natuurlijk de $\State$ nodig voor ieder statement: ieder statement verandert de stack, en @@ -29,10 +29,10 @@ Voordat we alle commando's bespreken is een klein voorbeeld op zijn plaats. (eerst gepushte element eerst) en zet het resultaat op de stack. \item \smurfinline{o} output het element bovenop de stack. \end{itemize} - De output van dit programma is dus `papasmurf'. + De output van dit programma is dus \lit{papasmurf}. - We hebben spaties gebruikt voor de leesbaarheid. Dit is toegestaan maar niet - vereist. Het programma \smurfinline{"papa""smurf"+o} is eveneens geldig. + We hebben spaties toegevoegd voor de leesbaarheid. Dit is toegestaan maar + niet vereist. Het programma \smurfinline{"papa""smurf"+o} is eveneens geldig. \end{exmp} Naast de stack kent Smurf ook een \emph{variable store} die variabelenamen @@ -42,13 +42,14 @@ illustreren met een voorbeeld: \begin{exmp} We bekijken het volgende programma: \begin{smurf}"smurf" "papa" p "papa" g o\end{smurf} - Nadat `smurf' en `papa' op de stack zijn gezet gebruiken we \smurfinline{p} - om de variabele `papa' de waarde `smurf' te geven. Hierna is de stack weer - leeg. Vervolgens zetten we `papa' op de stack en gebruiken we \smurfinline{g} - om het bovenste element als variabele op te zoeken in de variable store en de - waarde ervan op de stack te zetten. Hierbij wordt het bovenste element van de - stack verwijderd. De stack bestaat nu dus uit het element `smurf'. Met - \smurfinline{o} sturen we deze string naar de output. + Nadat \lit{smurf} en \lit{papa} op de stack zijn gezet gebruiken we + \smurfinline{p} om de variabele \lit{papa} de waarde \lit{smurf} te geven. + Hierna is de stack weer leeg. Vervolgens zetten we \lit{papa} op de stack en + gebruiken we \smurfinline{g} om het bovenste element als variabele op te + zoeken in de variable store en de waarde ervan op de stack te zetten. + Hierbij wordt het bovenste element van de stack verwijderd. De stack bestaat + nu dus uit het element \lit{smurf}. Met \smurfinline{o} sturen we deze string + naar de output. \end{exmp} \input{introcoms} diff --git a/introcoms.tex b/introcoms.tex index 638a11e..090e2af 100644 --- a/introcoms.tex +++ b/introcoms.tex @@ -3,26 +3,27 @@ \label{sec:intro:commands} 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. We gebruiken een leesbaardere -variant op de taal zodat het overzichtelijker is om eigenschappen ervan te -bespreken. Alle commando's betekenen nog steeds hetzelfde. +alternatief dat we in de rest van dit werkstuk zullen gebruiken. De commando's +zijn dus niet exact hetzelfde als in de voorbeeldprogramma's en de specificatie +van de taal~\cite{safalra}. Met onze leesbaardere variant is het makkelijker om +over de taal te redeneren. + +Voor ieder commando geldt dat wanneer het elementen op de stack gebruikt, die +elementen worden verwijderd. \begin{description}[style=nextline,font=\normalfont] - \item[\smurfinline{"..."} of $\StmPush~\texttt{...}$] - waarbij `\texttt{...}' een string is. Zet de string \texttt{...} op de - stack. + \item[\smurfinline{"..."} of $\StmPush~\texttt{...}$, waar \lit{...} een + string is] + Zet de string \lit{...} op de stack. \item[\smurfinline{+} of $\StmCat$] Concateneert de bovenste twee strings (laagste eerst) op de stack en zet het resultaat op de stack. \item[\smurfinline{i} of $\StmInput$] Plaatst een string van `user input' op de stack. Hierbij wordt - \texttt{\textbackslash} gebruikt om LF-karakters, dubbele aanhalingstekens - en backslashes te escapen. Het is ook mogelijk LF-karakters in de string te - gebruiken. Afhankelijk van de inputmethode is dit al dan niet mogelijk --- - in deze specificatie abstraheren we van inputmethodes. + \lit{\textbackslash} gebruikt om LF-karakters, dubbele aanhalingstekens en + backslashes te escapen. Afhankelijk van de inputmethode kan het ook + mogelijk zijn dat LF-karakters in de string voorkomen. In deze specificatie + abstraheren we van inputmethodes. \item[\smurfinline{o} of $\StmOutput$] Stuurt het bovenste element van de stack naar `de output'. \item[\smurfinline{p} of $\StmPut$] diff --git a/introexmp.tex b/introexmp.tex index 90ed119..cb12228 100644 --- a/introexmp.tex +++ b/introexmp.tex @@ -4,28 +4,6 @@ Nu we alle commando's hebben gezien bekijken we nog een paar voorbeelden die aangeven hoe conditionele executie kan worden behaald in Smurf. -% Dit is waarschijnlijk te veel anders. -% -%\begin{exmp} -% Het volgende programma implementeert een simpel bestelsysteem: -% \begin{smurf} -% "ijs" "0" p \\ -% "pizza" "1" p \\ -% "Wil je ijs (0) of pizza (1)?\textbackslash{}n" o \\ -% "Ik ga " i g + " voor je maken!" + o -% \end{smurf} -% We zetten de variabelen \verb$0$ en \verb$1$ tot \verb$ijs$ en \verb$pizza$. -% Vervolgens vragen we de gebruiker een keuze te maken. Met \smurfinline{ig} -% kan de gebruiker in feite kiezen welke variabele wordt opgehaald. -% -% De uitvoer kan er dus uitzien als: -% \begin{verbatim} -% Wil je ijs (0) of pizza (1)? -% 1 -% Ik ga pizza voor je maken! -% \end{verbatim} -%\end{exmp} - \begin{exmp} \label{exmp:headortail} Dit programma laat de gebruiker kiezen welke functie er wordt uitgevoerd: @@ -35,29 +13,27 @@ aangeven hoe conditionele executie kan worden behaald in Smurf. "Wil je de head of de tail?\textbackslash{}n"o \\ ig +"o"+ x \end{smurf} - Allereerst zetten we de variabelen \verb$head$ en \verb$tail$ tot \verb$h$ en - \verb$t$, de commando's voor de head en tail van een string. We vragen de + Allereerst zetten we de variabelen \lit{head} en \lit{tail} tot \lit{h} en + \lit{t}, de commando's voor de head en tail van een string. We vragen de gebruiker om een string en zetten die in quotes zodat ze gebruikt kan worden - in een Smurfprogramma. We vragen de gebruiker om `head' of `tail' in te - voeren en halen de bijbehorende functie op. Op dit moment kan de stack eruit - zien als \verb$h$, \verb$"mijn string"$ (bovenste element eerst). Met - \smurfinline{+"o"+} bouwen we hiervan het programma \smurfinline{"mijn - string"ho}, wat we met \smurfinline{x} uitvoeren. De uitvoer van het - programma is dus `m', in dit geval. + in een Smurfprogramma. We vragen de gebruiker om \lit{head} of \lit{tail} in + te voeren en halen de bijbehorende functie op. Op dit moment kan de stack er + bijvoorbeeld uit zien als \lit{h}, \lit{"mijn string"} (bovenste element + eerst). Met \smurfinline{+"o"+} bouwen we hiervan het programma + \smurfinline{"mijn string"ho}, wat we met \smurfinline{x} uitvoeren. De + uitvoer van het programma is dus \lit{m}, in dit geval. - Wat gebeurt er als de gebruiker iets anders dan `head' of `tail' invoert? In - dit geval bestaat er geen variabele met de naam die de gebruiker had - ingevoerd. Het commando \smurfinline{g} levert dan de lege string op. Dit + Wat gebeurt er als de gebruiker iets anders dan \lit{head} of \lit{tail} + invoert? In dit geval bestaat er geen variabele met de naam die de gebruiker + had ingevoerd. Het commando \smurfinline{g} levert dan de lege string op. Dit betekent dat we het programma \smurfinline{"mijn string"o} bouwen. Als de - gebruiker dus geen correcte keuze maakt, dan zal de hele string worden + gebruiker geen correcte keuze maakt, dan zal de hele string dus worden teruggegeven. \end{exmp} \begin{exmp} Het volgende programma is een Smurf interpreter: - \begin{smurf} - ix - \end{smurf} + \begin{smurf}ix\end{smurf} We halen input op van de gebruiker en voeren dit uit als Smurfprogramma. \end{exmp} @@ -76,14 +52,14 @@ voorgedaan: x \end{smurf} Met de eerste twee regels halen we input op en sturen die naar de output. Ook - wordt de input in een variabele \verb$s$ opgeslagen. - De derde regel zet een Smurfprogramma in \verb$c$. - In de vierde regel plakken we dat gequotifiede programma, de gequotifiede - input en het programma aan elkaar vast. Het resultaat voeren we uit. + wordt de input in een variabele \lit{s} opgeslagen. De derde regel zet een + Smurfprogramma in \lit{c}. In de vierde regel plakken we dat gequotifiede + programma, de gequotifiede input en het programma aan elkaar vast. Het + resultaat voeren we uit. Op dit moment voeren we dus het programma uit dat bestaat uit twee keer een - string pushen en vervolgens het programma uit \verb$c$. Dan bekijken we nu - dit programma, wat we in de derde regel hierboven hebben gedefinieerd, in een + string pushen en vervolgens het programma uit \lit{c}. Dan bekijken we nu dit + programma, wat we in de derde regel hierboven hebben gedefinieerd, in een iets makkelijkere opmaak: \begin{smurf} t "s"p "s"g "\textbackslash{}n"+o \\ @@ -93,13 +69,12 @@ voorgedaan: """"p \\ "s"ggx \end{smurf} - Met de eerste regel slaan we de tail van de oude input op in \verb$s$. We + Met de eerste regel slaan we de tail van de oude input op in \lit{s}. We sturen deze tail ook naar de output. Hierna staat alleen nog de eerste string op de stack, d.w.z. het programma waar we naar kijken. Dit slaan we op in - \verb$c$. - De derde regel hier is hetzelfde als de vierde regel hierboven: we maken een - nieuw programma, wat er precies hetzelfde uitziet als dit, behalve dat we van - de tweede string één karakter hebben weggehaald. + \lit{c}. De derde regel hier is hetzelfde als de vierde regel hierboven: we + maken een nieuw programma, wat er precies hetzelfde uitziet als dit, behalve + dat we van de tweede string één karakter hebben weggehaald. Het is verleidelijk op dit moment weer \smurfinline{x} te gebruiken. We moeten echter eerst nog controleren of we niet met de lege string te maken @@ -107,7 +82,7 @@ voorgedaan: is. We maken dus van het nieuwe programma wederom een nieuw programma, wat bestaat uit het pushen van het oude programma en vervolgens \smurfinline{x} aanroepen. Dit programma slaan we op in de variabele met als naam de waarde - van \verb$s$ (de input). + van \lit{s} (de input). Mocht deze input de lege string zijn, dan overschrijft de vijfde regel dit programma met een leeg programma. Vervolgens halen we in de zesde regel het @@ -116,7 +91,7 @@ voorgedaan: \smurfinline{t} uitvoeren op de lege string. \medskip - De uitvoer van dit programma met de input `smurf' is dus: + De uitvoer van dit programma met de input \lit{smurf} is dus: \begin{verbatim} smurf @@ -10,6 +10,6 @@ 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. Hierbij gebruiken we \emph{CleanSmurf}, een zelfgemaakt -programma dat \LaTeX-afleidingsbomen voor Smurfprogramma's kan genereren. Dit -programma wordt in \autoref{sec:cleansmurf} toegelicht. +gedefinieerde regels. Hierbij gebruiken we \emph{CleanSmurf}~\cite{cleansmurf}, +een zelfgemaakt programma dat (\LaTeX-)afleidingsbomen voor Smurfprogramma's +kan genereren. Dit programma wordt in \autoref{sec:cleansmurf} toegelicht. @@ -5,14 +5,14 @@ We zullen nu ieder syntaxelement nader specificeren. Ook zullen regels voor de natuurlijke semantiek van Smurf worden geïntroduceerd. Bij elk van deze regels geldt dat als elementen van de stack worden gebruikt in die regel, de stack -niet leeg mag zijn voor het uitvoeren van de regel. %todo waarom deze keuze? +niet leeg mag zijn voor het uitvoeren van de regel. De documentatie \cite{safalra} beschrijft niet wat er gebeurt wanneer er niet genoeg argumenten op de stack staan om een bepaalde instructie uit te voeren. -In de \emph{Perl}-interpreter van de taal is ervoor gekozen om een dergelijk -programma abrupt te laten termineren met een foutmelding. Wij kiezen er echter -voor om het in zulk soort gevallen onmogelijk te maken een afleidingsboom te -maken (in tegenstelling tot bijvoorbeeld een errorstatus aan de rechterkant van +In de Perl-interpreter van de taal is ervoor gekozen om een dergelijk programma +abrupt te laten termineren met een foutmelding. Wij kiezen er echter voor om +het in zulk soort gevallen onmogelijk te maken een afleidingsboom te maken (in +tegenstelling tot bijvoorbeeld een errorstatus aan de rechterkant van transities toe te voegen), omdat dit het redeneren over Smurfprogramma's makkelijker zal maken. diff --git a/rulesexec.tex b/rulesexec.tex index 0ac3e10..26d264f 100644 --- a/rulesexec.tex +++ b/rulesexec.tex @@ -53,6 +53,5 @@ $$ Het tweede geval van $\parsestrop$ zorgt ervoor dat ge-escapete aanhalingstekens de string niet beëindigen. Hierbij gebruiken we $\unescapeop$ -om bepaalde karakters te unescapen. Zie voor de definitie van deze regel +om bepaalde karakters te unescapen. Deze functie is gedefinieerd in \autoref{sec:rules:push}. - diff --git a/rulespush.tex b/rulespush.tex index 21f332d..8bc94e6 100644 --- a/rulespush.tex +++ b/rulespush.tex @@ -33,10 +33,10 @@ $$ Het laatste alternatief geeft aan dat `ongeldige escape sequences' worden behandeld alsof de backslash er twee keer stond. Dit is in overeenstemming met -het commentaar op de specificatie en met de Perl interpreter: %todo referentie +het commentaar op de specificatie en met de Perl-interpreter: %todo referentie \begin{quote} This [the specification] does not specify the behaviour of invalid escape - sequences. The Perl interpreter treats invalid escape sequences as if the + sequences. The Perl-interpreter treats invalid escape sequences as if the backslash had occured twice - that is, \textbackslash X is treated as \textbackslash\textbackslash X. For maximum compatibility, Smurf programs should not rely on this behaviour and should always ensure valid escape @@ -94,4 +94,3 @@ % Programs \newenvironment{smurf}{\tt\begin{center}}{\end{center}} \let\smurfinline\texttt - diff --git a/sosexamp.tex b/sosexamp.tex index 32e4f2c..5317458 100644 --- a/sosexamp.tex +++ b/sosexamp.tex @@ -5,8 +5,8 @@ We willen ook 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. 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 omdat we hier meer bekend mee zijn. We wilden echter ook graag laten +zien hoe het eruit zou zien als je structurele operationele semantiek zou gebruiken. Bij het definiëren van de structurele operationele semantiek van Smurf zullen @@ -15,16 +15,15 @@ $\Pgm\times\Input\times\Output\times\State$ en $\Gamma$ beschouwen, waarbij $\Gamma$ óf $\Pgm\times\Input\times\Output\times\State$ óf $\Input\times\Output\times\State$ is. Dit schrijven we als -$$\sostransgamma{\stm:\pgm}{\ip}{\op}{\st}{\gamma} - \qquad \text{met\enspace\parbox{36mm}{ - $\gamma = (\pgm',\ip',\op',\st')$ of \\ - $\gamma = (\ip', \op',\st' )$}}$$ +$$ + \sostransgamma{\stm:\pgm}{\ip}{\op}{\st}{\gamma} + \qquad\text{met $\gamma \in \{(\pgm',\ip',\op',\st'), (\ip', \op',\st')\}$}. +$$ -De reden dat we hier spreken over $\pgm'$ is omdat de $\StmExec$-regel het programma -dat je gaat uitvoeren verandert. In de meeste gevallen zal $\pgm$ = $\pgm'$ -gelden maar dat hoeft dus niet. +De reden dat rechts van de pijl $\pgm'$ gebruikt wordt (en niet gewoon $\pgm$) +is dat in het geval van $\StmExec$ de rest van het programma niet zal worden +uitgevoerd. In de meeste gevallen zal $\pgm=\pgm'$ echter wel gelden. -\medskip Het is mogelijk om in de structurele operationele semantiek, zoals bij de natuurlijke semantiek, compositie in te bouwen in iedere regel en een $\lambda$-regel toe te voegen. In dit geval kiezen we er echter voor om gebruik @@ -47,7 +46,6 @@ $$ \end{prooftree} $$ -\bigskip We geven twee voorbeelden van regels in de structurele operationele semantiek. Het doel is hier niet om een precieze beschrijving van de semantiek te geven zoals we dat in \autoref{sec:rules} voor natuurlijke semantiek hebben gedaan, @@ -57,15 +55,11 @@ lijken. 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')$.} -\end{prooftree} + \enspace\rtailsos + \quad\text{met $\pop{\stk} = (c~s,\stk')$.} $$ Afgezien van de compositie, die bij de natuurlijke semantiek in iedere regel is @@ -74,17 +68,13 @@ ingebouwd, verschilt dit niet erg van $\rtailns$ in \autoref{sec:rules:tail}. Dit geldt voor bijna alle andere commando's net zo. Een apart geval is $\StmExec$, omdat we hier de compositieregel niet kunnen gebruiken. Wat na het $\StmExec$-commando volgt wordt immers niet uitgevoerd. We definiëren deze -regels als volgt: +regel als volgt: $$ -\begin{prooftree} -\axjustifies \sostrans {\StmExec:\pgm}{\ip}{\op}{(\stk,\str)} {\pgm'}{\ip'}{\op'}{(\stk',\str')} - \using{\rexecsos} - \qquad - \text{met $\pop{\stk} = ( \pgm', \stk'')$.} -\end{prooftree} + \enspace\rexecsos + \quad\text{met $\pop{\stk} = ( \pgm', \stk'')$.} $$ Hier wordt gebruik gemaakt van een ander soort transitie, waarbij een programma aan de rechterkant voorkomt. Hierdoor is $\rexecsos$ niet te gebruiken als diff --git a/werkstuk.tex b/werkstuk.tex index 6935ea0..b719ce9 100644 --- a/werkstuk.tex +++ b/werkstuk.tex @@ -34,7 +34,7 @@ % Settings, fixes \setlist{itemsep=0pt} \addto\extrasdutch{% - \renewcommand{\sectionautorefname}{Sectie} + \renewcommand{\sectionautorefname}{Hoofdstuk} \renewcommand{\subsectionautorefname}{Paragraaf} \renewcommand{\figureautorefname}{Figuur} } @@ -43,9 +43,8 @@ \declaretheoremstyle[ title=Voorbeeld, parent=section, - spacebelow=1em, - preheadhook=\nobreak\noindent\hrulefill, - prefoothook=\vspace*{\dimexpr-\baselineskip+\topsep\relax}\endgraf\nobreak\noindent\hrulefill% + preheadhook=\framed, + prefoothook=\endframed, ]{lined} \declaretheorem[style=lined]{exmp} |