diff options
| -rw-r--r-- | analyse.tex | 11 | ||||
| -rw-r--r-- | defio.tex | 5 | ||||
| -rw-r--r-- | defstate.tex | 2 | ||||
| -rw-r--r-- | defsyn.tex | 4 | ||||
| -rw-r--r-- | deftrans.tex | 6 | ||||
| -rw-r--r-- | intro.tex | 5 | ||||
| -rw-r--r-- | introcoms.tex | 10 | ||||
| -rw-r--r-- | introexmp.tex | 2 | ||||
| -rw-r--r-- | rules.tex | 2 | ||||
| -rw-r--r-- | rulescat.tex | 3 | ||||
| -rw-r--r-- | rulesexec.tex | 4 | ||||
| -rw-r--r-- | rulesget.tex | 6 | ||||
| -rw-r--r-- | ruleshead.tex | 4 | ||||
| -rw-r--r-- | rulesinput.tex | 6 | ||||
| -rw-r--r-- | rulesoutput.tex | 3 | ||||
| -rw-r--r-- | rulespush.tex | 2 | ||||
| -rw-r--r-- | rulesput.tex | 4 | ||||
| -rw-r--r-- | rulesquotify.tex | 4 | ||||
| -rw-r--r-- | rulestail.tex | 2 |
19 files changed, 43 insertions, 42 deletions
diff --git a/analyse.tex b/analyse.tex index 3c5c343..2f49080 100644 --- a/analyse.tex +++ b/analyse.tex @@ -1,4 +1,13 @@ % vim: set spelllang=nl: \section{Analyse} \label{sec:analyse} -Als analyse willen we graag een stuk code bekijken aan de hand van onze semantiek regels. 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 semantiek regels.
\ No newline at end of file +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} + \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} + +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 @@ -2,8 +2,7 @@ \subsection{Input en output} \label{sec:def:io} -Allereerst definiëren we het type $\Stack{a}$, omdat stacks veel voorkomen in -Smurf. Een $\Stack{a}$ (lees: een stack van elementen van type $a$) is een +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} @@ -19,7 +18,7 @@ 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 gedefinieerd is. +$\popop$ is een partiële functie omdat $\pop\Nil$ niet gebruikt mag worden in onze semantiekregels. \medskip We zullen de input en output beide als $\Stack{\String}$ modelleren. In feite diff --git a/defstate.tex b/defstate.tex index 135aeea..f60297d 100644 --- a/defstate.tex +++ b/defstate.tex @@ -17,7 +17,7 @@ $\lambda$ in overeenstemming met de documentatie \cite{safalra}: \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 +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$. @@ -1,12 +1,10 @@ % vim: set spelllang=nl: \subsection{Syntax} \label{sec:def:syn} - We definiëren de volgende syntax: - \setlength{\grammarindent}{5em} \begin{grammar} - <Pgm> ::= <Stm>:<Pgm> | $\lambda$ + <Pgm> ::= <Stm> <Pgm> | $\lambda$ <Stm> ::= `Push' <String> \alt `Cat' | `Head' | `Tail' | `Quotify' diff --git a/deftrans.tex b/deftrans.tex index aae4239..67b5323 100644 --- a/deftrans.tex +++ b/deftrans.tex @@ -1,16 +1,16 @@ % 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, 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. Dit schrijven we als -$$\trans{\pgm}{\ip}{\st}{\ip}{\op}{\st}$$ +$$\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$ met output $\op$ waarbij de input $\ip$ niet geconsumeerd is.'' + 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.'' \end{quote} We hebben het hele programma $\Pgm$ nodig voor de pijl, omdat één commando @@ -11,8 +11,7 @@ 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 -hiervan die we 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 @@ -47,7 +46,7 @@ illustreren met een voorbeeld: 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. De stack bestaat nu dus uit het element + waarde ervan op de stack te zetten. Hierbij wordt het bovenste element van de stack verwijdert. De stack bestaat nu dus uit het element `smurf'. Met \smurfinline{o} sturen we deze string naar de output. \end{exmp} diff --git a/introcoms.tex b/introcoms.tex index edbae5b..34e76f8 100644 --- a/introcoms.tex +++ b/introcoms.tex @@ -16,21 +16,19 @@ 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. + 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$] - Zet de waarde van de variabelenaam bovenop de stack tot de string daaronder - op de stack. - \item[\smurfinline{h} of $\StmHead$] - Zet het eerste karakter van de string bovenop de stack als string op de + 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$] Zet alles behalve de head van de string bovenop de stack op de stack. \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 backslashes 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 e372889..33a922b 100644 --- a/introexmp.tex +++ b/introexmp.tex @@ -95,7 +95,7 @@ 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. We maken dus van het nieuwe programma wederom een nieuw programma, + 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). @@ -3,7 +3,7 @@ \label{sec:rules} We zullen nu ieder syntaxelement nader specificeren. Ook zullen regels voor de -natuurlijke semantiek van Smurf worden geïntroduceerd. +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. 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 a54b508..95269e1 100644 --- a/rulescat.tex +++ b/rulescat.tex @@ -25,8 +25,7 @@ $$ \using{\rcatns} \qquad \text{met\enspace - \parbox{36mm}{$(s_2,\stk') = \pop{\stk}$,\\$(s_1,\stk'') = \pop{\stk'}$.} - } + \parbox{36mm}{$\pop{\stk} = (s_2,\stk') $,\\$ \pop{\stk' = (s_1,\stk'')}$.} \end{prooftree} $$ diff --git a/rulesexec.tex b/rulesexec.tex index 4d3e1a7..bebf0e9 100644 --- a/rulesexec.tex +++ b/rulesexec.tex @@ -8,7 +8,7 @@ \end{quote} We halen een string van de stack en gebruiken $\parsepgmop$ om dit in een -programma om te zetten. Dit wordt het nieuwe programma om uitgevoerd te worden. +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. @@ -25,7 +25,7 @@ $$ \using{\rexecns} \qquad \text{met\enspace - \parbox{36mm}{$(\var,\stk') = \pop{\stk}$,\\ + \parbox{36mm}{$ \pop{\stk} =(\var,\stk')$,\\ $\pgm' = \parsepgm{\var'}$.} } \end{prooftree} diff --git a/rulesget.tex b/rulesget.tex index bc38d5b..2fec68c 100644 --- a/rulesget.tex +++ b/rulesget.tex @@ -8,9 +8,7 @@ \end{quote} De regel voor dit statement spreekt voor zich. In het geval dat $\stk$ leeg is, -is $\pop\stk$ niet gedefinieerd en kunnen we de regel dus niet toepassen. Omdat -$\StmGet$ geen IO gebruikt kunnen we $\ip$, $\ip'$ en $\op$ direct doorgeven. - +is $\pop\stk$ niet gedefinieerd en kunnen we de regel dus niet toepassen. $$ \begin{prooftree} \trans @@ -22,7 +20,7 @@ $$ {\ip'}{\op}{\st} \using{\rgetns} \qquad - \text{met $(\var,\stk') = \pop{\stk}$.} + \text{met $\pop{\stk}= (\var,\stk')$.} \end{prooftree} $$ diff --git a/ruleshead.tex b/ruleshead.tex index 53b4bf2..d45bee3 100644 --- a/ruleshead.tex +++ b/ruleshead.tex @@ -3,7 +3,7 @@ \label{sec:rules:head} \begin{quote} - h - Pops a string from the stack, and pushes its head, ie the first + h - Pops a string from the stack, and pushes its head, that is the first character. This causes an error if used on the empty string. \end{quote} @@ -24,7 +24,7 @@ $$ {\ip'}{\op}{\st} \using{\rheadns} \qquad - \text{met $(c~s,\stk') = \pop{\stk}$.} + \text{met $\pop{\stk} = (c~s,\stk')$.} \end{prooftree} $$ diff --git a/rulesinput.tex b/rulesinput.tex index 2e59ddf..10b3312 100644 --- a/rulesinput.tex +++ b/rulesinput.tex @@ -6,7 +6,7 @@ i - takes a string from user input, and places it on the stack. \end{quote} -In het bijzonder dit commando is erg slecht gedefinieerd. Mag deze input +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 @@ -22,7 +22,7 @@ bestaan. We gaan er verder van uit dat de gebruiker zijn programma volledig wil uitvoeren en dus voldoende input zal geven, waardoor $\pop\ip$ altijd gedefinieerd is. Geeft de gebruiker niet genoeg input, dan hoeven we dus geen -afleidingsboom maken (en we zullen dit ook onmogelijk maken). +afleidingsboom te maken (en we zullen dit ook onmogelijk maken). Dit geeft de volgende regel: @@ -37,7 +37,7 @@ $$ {\ip''}{\op}{\st} \using{\rinputns} \qquad - \text{met $(\val,\ip')=\pop\ip$.} + \text{met $\pop\ip = (\val,\ip')$.} \end{prooftree} $$ diff --git a/rulesoutput.tex b/rulesoutput.tex index 96c806e..f55b374 100644 --- a/rulesoutput.tex +++ b/rulesoutput.tex @@ -22,10 +22,11 @@ $$ {\ip'}{[\op:[s:\Nil]]}{\st} \using{\routputns} \qquad - \text{met $(s,\stk') = \pop{\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. diff --git a/rulespush.tex b/rulespush.tex index c14feae..230cace 100644 --- a/rulespush.tex +++ b/rulespush.tex @@ -11,7 +11,7 @@ \verb$\\$ = the \verb$\$ character. \end{quote} -De string tussen de aanhalingstekens word op de stack gezet, nadat escape +De string tussen de aanhalingstekens wordt op de stack gezet, nadat escape sequences eruit zijn gehaald middels de hulpfunctie $\unescapeop$. Het is, zoals het commentaar op de specificatie \cite{safalra} aangeeft, niet gedefinieerd wat er met ongeldige escape sequences gebeurt. diff --git a/rulesput.tex b/rulesput.tex index 959fec8..3a8fd05 100644 --- a/rulesput.tex +++ b/rulesput.tex @@ -24,8 +24,8 @@ $$ \using{\rputns} \qquad \text{met\enspace - \parbox{36mm}{$(\var,\stk') = \pop{\stk}$,\\$(\val,\stk'') = \pop{\stk'}$.} - } + \parbox{36mm}{$\pop{\stk} = (\var,\stk')$, + \\$\pop{\stk'}= (\val,\stk'')$.}} \end{prooftree} $$ diff --git a/rulesquotify.tex b/rulesquotify.tex index d218fd6..5c1d090 100644 --- a/rulesquotify.tex +++ b/rulesquotify.tex @@ -26,14 +26,14 @@ $$ {\ip}{\op}{\st} \using{\rquotifyns} \qquad - \text{met $(s, stk') = \pop{\stk}$.} + \text{met $ \pop{\stk} = (s, stk')$.} \end{prooftree} $$ $$ \escape{c~s} = \begin{cases} - \texttt{\textbackslash}~c~s & \text{als + \texttt{\textbackslash}~c~\escape{s} & \text{als $c\in\{\texttt{"},\texttt{\textbackslash},\text{het LF-karakter}\}$} \\ c~\escape{s} & \text{anderszins} \end{cases} diff --git a/rulestail.tex b/rulestail.tex index 156d6b6..dc93a3b 100644 --- a/rulestail.tex +++ b/rulestail.tex @@ -23,6 +23,6 @@ $$ {\ip'}{\op}{\st} \using{\rtailns} \qquad - \text{met $(c~s,\stk') = \pop{\stk}$.} + \text{met $ \pop{\stk} = (c~s,\stk') $.} \end{prooftree} $$
\ No newline at end of file |