diff options
| -rw-r--r-- | analyse.tex | 24 | ||||
| -rw-r--r-- | defio.tex | 8 | ||||
| -rw-r--r-- | defstate.tex | 9 | ||||
| -rw-r--r-- | defsyn.tex | 3 | ||||
| -rw-r--r-- | deftrans.tex | 4 | ||||
| -rw-r--r-- | intro.tex | 3 | ||||
| -rw-r--r-- | introcoms.tex | 10 | ||||
| -rw-r--r-- | introexmp.tex | 9 | ||||
| -rw-r--r-- | rules.tex | 4 | ||||
| -rw-r--r-- | rulescat.tex | 2 | ||||
| -rw-r--r-- | rulesexec.tex | 9 | ||||
| -rw-r--r-- | rulesinput.tex | 10 | ||||
| -rw-r--r-- | rulesoutput.tex | 12 | ||||
| -rw-r--r-- | rulesquotify.tex | 2 | ||||
| -rw-r--r-- | werkstuk.tex | 1 |
15 files changed, 66 insertions, 44 deletions
diff --git a/analyse.tex b/analyse.tex index 2f49080..da359ea 100644 --- a/analyse.tex +++ b/analyse.tex @@ -1,13 +1,21 @@ % 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 semantiek regels. Deze code ziet er als volgt uit. - \begin{smurf} +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"\backslash"\backslash"p\backslash"i\backslash"gh\backslash"o\backslash"g+\backslash"o\backslash"p\backslash"i\backslash"gt\backslash"i\backslash"p\backslash"\backslash\backslash\backslash"+\backslash\backslash\backslash"\backslash\backslash\backslash\backslash\backslash\backslash"\backslash\backslash\backslash"p - \backslash"\backslash"i\backslash"gq+\backslash"tg\backslash"+\backslash"i\backslash"gq+\backslash"\backslash\backslash\backslash"i\backslash\backslash\backslash"p\backslash"+\backslash"o\backslash"gq+\backslash"\backslash\backslash\backslash"o\backslash\backslash\backslash"p\backslash"+\backslash"\backslash"gq+\backslash"\backslash"g+\backslash"\backslash" - p\backslash"o\backslash"gq\backslash"o\backslash"+\backslash"+\backslash"pgx"""p"\backslash"+\backslash"\backslash"\backslash"p""i"gq+"tg"+"i"gq+"\backslash"i\backslash"p\backslash"\backslash""+""gq+""g+""p - """+""i"g+pgx - \end{smurf} + "+"i+ ""p ""gtg ""gt "i"p\\ + %todo layout, dit loopt over de regel heen (maar geeft wel aan waar de + %commando's liggen + "\textbackslash{}"\textbackslash{}"p\textbackslash{}"i\textbackslash{}"gh\textbackslash{}"o\textbackslash{}"g+\textbackslash{}"o\textbackslash{}"p\textbackslash{}"i\textbackslash{}"gt\textbackslash{}"i\textbackslash{}"p\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"+\textbackslash{}\textbackslash{}\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}\textbackslash{}\textbackslash{}\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}"\textbackslash{}"i\textbackslash{}"gq+\textbackslash{}"tg\textbackslash{}"+\textbackslash{}"i\textbackslash{}"gq+\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"i\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}"+\textbackslash{}"o\textbackslash{}"gq+\textbackslash{}"\textbackslash{}\textbackslash{}\textbackslash{}"o\textbackslash{}\textbackslash{}\textbackslash{}"p\textbackslash{}"+\textbackslash{}"\textbackslash{}"gq+\textbackslash{}"\textbackslash{}"g+\textbackslash{}"\textbackslash{}"p\textbackslash{}"o\textbackslash{}"gq\textbackslash{}"o\textbackslash{}"+\textbackslash{}"+\textbackslash{}"pgx"\\ + ""p "\textbackslash{}"+\textbackslash{}"\textbackslash{}"\textbackslash{}"p" "i"gq+ "tg"+ "i"gq+\\ + "\textbackslash{}"i\textbackslash{}"p\textbackslash{}"\textbackslash{}""+ ""gq+ ""g+ ""p "" "+" "i"g+ pgx +\end{smurf} -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 interpetaties 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.
\ No newline at end of file +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. @@ -2,8 +2,9 @@ \subsection{Input en output} \label{sec:def:io} -Allereerst definiëren we het type $\Stack{a}$, omdat stacks we veel met stacks doen in onze semantiek regels. 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}$, omdat stacks we veel met stacks +doen in onze semantiek regels. Een $\Stack{a}$ (lees: een stack van elementen +van type $a$) is een simpel datatype met de volgende syntax: \begin{grammar} <Stack[a]> ::= [<a>:<Stack[a]>] | `Nil' @@ -18,7 +19,8 @@ Op een stack zijn twee instructies gedefinieerd: \pop{[e:s]} \isdef (e,s) \\ \end{gather*} -$\popop$ is een partiële functie omdat $\pop\Nil$ niet gebruikt mag worden in onze semantiekregels. +$\popop$ is een partiële functie omdat $\pop\Nil$ niet gebruikt mag worden in +onze semantiekregels. %todo waarom niet? \medskip We zullen de input en output beide als $\Stack{\String}$ modelleren. In feite diff --git a/defstate.tex b/defstate.tex index f60297d..e54c888 100644 --- a/defstate.tex +++ b/defstate.tex @@ -16,10 +16,11 @@ $\lambda$ in overeenstemming met de documentatie \cite{safalra}: variable values are initially set to the empty string. \end{quote} -Een toewijzing van $\val$ aan $\var$ noteren we als $\var\mapsto\val$, zodat we -bijvoorbeeld $\texttt{x}\mapsto\texttt{hello world}$ noteren voor de store -die \texttt{x} naar ``hello world'' stuurt. We laten de strings die naar -$\lambda$ sturen normaal gesproken weg. De initiële store schrijven we dus als +Een toewijzing van $\val$ aan $\var$ noteren we als $\var\mapsto\val$. Een +store is een verzameling zulke toewijzingen, zodat we bijvoorbeeld +$\{\texttt{x}\mapsto\texttt{hello world}\}$ noteren voor de store die +\texttt{x} naar ``hello world'' stuurt. We laten de strings die naar $\lambda$ +sturen normaal gesproken weg. De initiële store schrijven we dus als $\emptystore$. Om de waarde van een key $k$ uit store $\str$ te halen gebruiken we simpelweg @@ -4,7 +4,8 @@ We definiëren de volgende syntax: \setlength{\grammarindent}{5em} \begin{grammar} - <Pgm> ::= <Stm> <Pgm> | $\lambda$ + <Pgm> ::= <Stm>:<Pgm> | $\lambda$ %todo over de : moet uitleg komen, waarom + %we die introduceren <Stm> ::= `Push' <String> \alt `Cat' | `Head' | `Tail' | `Quotify' diff --git a/deftrans.tex b/deftrans.tex index 67b5323..2a9fb34 100644 --- a/deftrans.tex +++ b/deftrans.tex @@ -2,6 +2,7 @@ \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, echter denk wij dat we door het gebruik van natuurlijke semantiek meer kunnen in onze analyse. + Bij het definiëren van de natuurlijke semantiek van Smurf zullen we de verzameling van transities als een relatie $\to$ tussen $\Pgm\times\Input\times\State$ en $\Input\times\Output\times\State$ beschouwen. @@ -10,7 +11,8 @@ $$\trans{\pgm}{\ip}{\st}{\ip'}{\op}{\st'}$$ en lezen we als \begin{quote} ``het programma $\pgm$ zal in toestand $\st$ gegeven input $\ip$ leiden tot - toestand $\st'$, waarbij als de toestand niet verandert geldt $\st'$ = $\st$, met output $\op$ waarbij de input $\ip'$ met $\ip'$ = $\ip$ als $\ip$ niet geconsumeerd is.'' + toestand $\st'$, met output $\op$ waarbij $\ip'$ gelijk is aan $\ip$ zonder + de geconsumeerde input.'' \end{quote} We hebben het hele programma $\Pgm$ nodig voor de pijl, omdat één commando @@ -11,7 +11,8 @@ Westcott. In de specificatie \cite{safalra} beschrijft hij kort wat Smurf is: The only native data type is the string, and operations are carried out on strings in a forty manner. \end{quote} -We hebben dus te maken met een Forth-achtige programmeertaal. De eigenschappen die we hiervan terugzien in Smurf zijn voornamelijk reflection, +We hebben dus te maken met een Forth-achtige programmeertaal. De eigenschappen +die we hiervan terugzien in Smurf zijn voornamelijk reflection, stackgeörienteerd en `geconcateneerd programmeren'. We kunnen het programma dus dynamisch aanpassen, werken met een stack en schrijven een programma als één grote functiecompositie (zonder met functieapplicaties te werken). Voordat we diff --git a/introcoms.tex b/introcoms.tex index 34e76f8..7295922 100644 --- a/introcoms.tex +++ b/introcoms.tex @@ -16,11 +16,15 @@ elementen op de stack doet, worden die elementen altijd verwijderd. \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.Echt mag je in de string linefeeds gebruiken. Hierbij is het niet van belang om te weten hoe de user input word afgesloten. + en backslashes te escapen. Echt mag je in de string linefeeds gebruiken. + Hierbij is het niet van belang om te weten hoe de user input word + afgesloten. \item[\smurfinline{o} of $\StmOutput$] Stuurt het bovenste element van de stack naar `de output'. \item[\smurfinline{p} of $\StmPut$] - Hierbij word ervoor gezorgd dat de waarde van de variablenaam bovenop de stack verwijst naar de string die daaronder staat. \item[\smurfinline{h} of $\StmHead$] + Hierbij word ervoor gezorgd dat de waarde van de variablenaam bovenop de + stack verwijst naar de string die daaronder staat. + \item[\smurfinline{h} of $\StmHead$] Zet het eerste karakter van de string bovenop de stack op de stack. \item[\smurfinline{t} of $\StmTail$] @@ -28,7 +32,7 @@ elementen op de stack doet, worden die elementen altijd verwijderd. \item[\smurfinline{q} of $\StmQuotify$] Manipuleert de string bovenop de stack zodat die als $\StmPush$-commando in een Smurfprogramma kan worden gebruikt: escapet LF-karakters, dubbele - aanhalingstekens en back- slashes met een backslash, en plaatst dubbele + aanhalingstekens en back\-slashes met een backslash, en plaatst dubbele aanhalingstekens om de hele string. Het resultaat wordt op de stack gezet. \item[\smurfinline{x} of $\StmExec$] Voert de string bovenop de stack uit als Smurfprogramma. Het programma diff --git a/introexmp.tex b/introexmp.tex index 33a922b..94c0afc 100644 --- a/introexmp.tex +++ b/introexmp.tex @@ -95,10 +95,11 @@ voorgedaan: 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 - hebben. Het is namelijk niet mogelijk om x uit te voeren als de stack leeg 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). + hebben. Het is namelijk niet mogelijk om x uit te voeren als de stack leeg + 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). 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 @@ -3,7 +3,9 @@ \label{sec:rules} 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 er een pop gebeurd in die regel de stack niet leeg mag zijn voor het uitvoeren van de regel. +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? 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. diff --git a/rulescat.tex b/rulescat.tex index 95269e1..48dcddf 100644 --- a/rulescat.tex +++ b/rulescat.tex @@ -25,7 +25,7 @@ $$ \using{\rcatns} \qquad \text{met\enspace - \parbox{36mm}{$\pop{\stk} = (s_2,\stk') $,\\$ \pop{\stk' = (s_1,\stk'')}$.} + \parbox{36mm}{$\pop{\stk} = (s_2,\stk') $,\\$ \pop{\stk'} = (s_1,\stk'')$.}} \end{prooftree} $$ diff --git a/rulesexec.tex b/rulesexec.tex index bebf0e9..9f4a60a 100644 --- a/rulesexec.tex +++ b/rulesexec.tex @@ -8,10 +8,11 @@ \end{quote} We halen een string van de stack en gebruiken $\parsepgmop$ om dit in een -programma om te zetten. Waarbij we $\parsepgmop$ later in de beschrijving zullen definiëren. Dit wordt het nieuwe programma om uitgevoerd te worden. -Als de $\stk$ leeg is is deze regel niet toepasbaar, omdat $\pop\stk$ dan niet -gedefinieerd is. Ook is deze regel niet toepasbaar als de gepopte string zelf -geen geldig Smurf-programma is, omdat $\parsepgmop$ dan niet gedefinieerd is. +programma om te zetten. Hieronder zullen we $\parsepgmop$ definiëren. Dit wordt +het nieuwe programma om uitgevoerd te worden. Als de $\stk$ leeg is is deze +regel niet toepasbaar, omdat $\pop\stk$ dan niet gedefinieerd is. Ook is deze +regel niet toepasbaar als de gepopte string zelf geen geldig Smurf-programma +is, omdat $\parsepgmop$ dan niet gedefinieerd is. $$ \begin{prooftree} diff --git a/rulesinput.tex b/rulesinput.tex index 10b3312..9d8985c 100644 --- a/rulesinput.tex +++ b/rulesinput.tex @@ -6,11 +6,11 @@ i - takes a string from user input, and places it on the stack. \end{quote} -Dit commando is erg slecht gedefinieerd. Mag deze input -bijvoorbeeld line feeds bevatten? Een naïeve implementatie die van stdin -gebruik maakt zou standaard splitsen op line feeds en dit dus niet toestaan. -Een andere implementatie zou gebruik kunnen maken van grafische prompts waarin -het wél mogelijk is meerdere regels input te geven. +Dit commando is erg slecht gedefinieerd. Mag deze input bijvoorbeeld line feeds +bevatten? Een naïeve implementatie die van stdin gebruik maakt zou standaard +splitsen op line feeds en dit dus niet toestaan. Een andere implementatie zou +gebruik kunnen maken van grafische prompts waarin het wél mogelijk is meerdere +regels input te geven. Om bij het redeneren over de semantiek geen last te hebben van zulk soort implementatiedetails hebben we ervoor gekozen hier tot op een hoog niveau van diff --git a/rulesoutput.tex b/rulesoutput.tex index f55b374..c6a1f66 100644 --- a/rulesoutput.tex +++ b/rulesoutput.tex @@ -15,19 +15,19 @@ $$ \prooftree \trans {\pgm}{\ip}{(\stk',\str)} - {\ip'}{[\op:\Nil]}{\st} + {\ip'}{\op}{\st} \justifies \trans {\StmOutput:\pgm}{\ip}{(\stk,\str)} {\ip'}{[\op:[s:\Nil]]}{\st} \using{\routputns} \qquad - \text{met $\pop{\stk} = (s,\stk') $.} + \text{met $\pop{\stk} = (s,\stk') $,} \endprooftree $$ -Waarbij [o:Nil] in de bovenste regel de gehele stack weergeeft. -Merk op dat eenzelfde regel waar $s$ niet achteraan maar vooraan zou komen te -staan, even geldig is. Geen van beide opties is beter dan de ander omdat we -geen aannames doen over hoe de $\Output$-stack wordt verwerkt. +waarbij $\op$ in de bovenste regel de gehele outputstack weergeeft. Merk op +dat eenzelfde regel waar $s$ niet achteraan maar vooraan zou komen te staan, +even geldig is. Geen van beide opties is beter dan de ander omdat we geen +aannames doen over hoe de $\Output$-stack wordt verwerkt. diff --git a/rulesquotify.tex b/rulesquotify.tex index 5c1d090..e0bdd4c 100644 --- a/rulesquotify.tex +++ b/rulesquotify.tex @@ -26,7 +26,7 @@ $$ {\ip}{\op}{\st} \using{\rquotifyns} \qquad - \text{met $ \pop{\stk} = (s, stk')$.} + \text{met $\pop{\stk} = (s, stk')$.} \end{prooftree} $$ diff --git a/werkstuk.tex b/werkstuk.tex index f844637..632d685 100644 --- a/werkstuk.tex +++ b/werkstuk.tex @@ -52,4 +52,3 @@ \input{refs} \end{document} - |