diff options
| -rw-r--r-- | def.tex | 8 | ||||
| -rw-r--r-- | defio.tex | 31 | ||||
| -rw-r--r-- | defstate.tex | 10 | ||||
| -rw-r--r-- | defsyn.tex | 24 | ||||
| -rw-r--r-- | deftrans.tex | 21 | ||||
| -rw-r--r-- | smurf.sty | 50 | ||||
| -rw-r--r-- | werkstuk.tex | 28 |
7 files changed, 172 insertions, 0 deletions
@@ -0,0 +1,8 @@ +\section{Definities} +\label{sec:def} + +\input{defsyn} +\input{defio} +\input{defstate} +\input{deftrans} + diff --git a/defio.tex b/defio.tex new file mode 100644 index 0000000..f3196ee --- /dev/null +++ b/defio.tex @@ -0,0 +1,31 @@ +% vim: set spelllang=nl: +\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 +simpel datatype met de volgende syntax: + +\begin{grammar} + <Stack[a]> ::= [<a>:<Stack[a]>] | `Nil' + %todo formatting +\end{grammar} + +Op een stack zijn twee instructies gedefinieerd: +\begin{gather*} + \pushop : \Stack{a} \times a \to \Stack{a} \\ + \push{s}{e} \isdef [e:s] \\[1em] + \popop : \Stack{a} \to a \times \Stack{a} \\ + \pop{[e:s]} \isdef (e,s) \\ +\end{gather*} + +\medskip +We zullen de input en output beide als $\Stack{\String}$ modelleren. In feite +zal zelfs blijken dat we op $\Input$ de operatie $\pushop$ niet nodig hebben, +en op $\Output$ de operatie $\popop$ niet zullen gebruiken. Informeel +beschouwen we $\Input$ als een `bron' van $\String$s en $\Output$ als een `put' +van $\String$s. Formeel: +\begin{align*} + \Input &\isdef \Stack{\String} \\ \Output &\isdef \Stack{\String} +\end{align*} + diff --git a/defstate.tex b/defstate.tex new file mode 100644 index 0000000..caa4880 --- /dev/null +++ b/defstate.tex @@ -0,0 +1,10 @@ +% vim: set spelllang=nl: +\subsection{Toestanden} +\label{sec:def:state} + +Een state $s\in\State$ van Smurf bevat zowel een stack als een variable store. +Hieruit volgt de voor de hand liggende definitie voor $\State$ +$$\State \isdef \Stack{\String} \times (\String \to \String)$$ +waarbij we $s=(\stk,\str)\in\State$ lezen als de toestand $s$ met stack $\stk$ +en variable store $\str$. + diff --git a/defsyn.tex b/defsyn.tex new file mode 100644 index 0000000..6623c1e --- /dev/null +++ b/defsyn.tex @@ -0,0 +1,24 @@ +% 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$ + + <Stm> ::= `Push' <String> + \alt `Cat' | `Head' | `Tail' | `Quotify' + \alt `Put' | `Get' + \alt `Input' | `Output' + \alt `Exec' + + <String> ::= <Char><String> | $\lambda$ +\end{grammar} + +Een karakter, $\SynChar$, is een symbool uit de ASCII tabel. + +Programma's zijn lijsten van statements. Compositie van statements is +impliciet. + diff --git a/deftrans.tex b/deftrans.tex new file mode 100644 index 0000000..0ff04e5 --- /dev/null +++ b/deftrans.tex @@ -0,0 +1,21 @@ +% vim: set spelllang=nl: +\subsection{Transities} +\label{sec:def:trans} + +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}{\i}{\st}{\i}{\o}{\st}$$ +en lezen we als +\begin{quote} + ``het programma $\pgm$ zal in toestand $\st$ gegeven input $\i$ leiden tot + toestand $\st$ met output $\o$ waarbij de input $\i$ niet geconsumeerd is.'' +\end{quote} + +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 +sommige statements veranderen bovendien de variable store. + diff --git a/smurf.sty b/smurf.sty new file mode 100644 index 0000000..eee1b26 --- /dev/null +++ b/smurf.sty @@ -0,0 +1,50 @@ +% General +\def\isdef{\stackrel{\text{def}}{=}} + +% Types +\def\Pgm{\mathit{Pgm}} +\def\Stm{\mathit{Stm}} +\def\Input{\mathit{Input}} +\def\Output{\mathit{Output}} +\def\State{\mathit{State}} +\def\String{\mathit{String}} +\def\Char{\mathit{Char}} + +% Stacks +\def\Stack#1{\mathbf{Stack}\left[\mathit{#1}\right]} +\def\pushop{\mathit{push}} +\def\popop{\mathit{pop}} +\def\push#1#2{\pushop\left(#1, #2\right)} +\def\pop#1{\popop\left(#1\right)} + +% Syntax +\def\SynPgm{\langle\Pgm\rangle} +\def\SynStm{\langle\Stm\rangle} +\def\SynString{\langle\String\rangle} +\def\SynChar{\langle\Char\rangle} + +% Statements +\let\statement\texttt +\def\StmPush{\statement{Push}} +\def\StmCat{\statement{Cat}} +\def\StmHead{\statement{Head}} +\def\StmTail{\statement{Tail}} +\def\StmQuotify{\statement{Quotify}} +\def\StmPut{\statement{Put}} +\def\StmGet{\statement{Get}} +\def\StmInput{\statement{Input}} +\def\StmOutput{\statement{Output}} +\def\StmExec{\statement{Exec}} + +% Transitions +\def\trans#1#2#3#4#5#6{\left\langle#1,#2,#3\right\rangle\to\left(#4,#5,#6\right)} + +% Common names +\def\stk{\mathit{stk}} +\def\str{\mathit{str}} +\def\i{\mathit{i}} +\def\o{\mathit{o}} +\def\pgm{\mathit{pgm}} +\def\stm{\mathit{stm}} +\def\st{\mathit{st}} + diff --git a/werkstuk.tex b/werkstuk.tex new file mode 100644 index 0000000..2853bdb --- /dev/null +++ b/werkstuk.tex @@ -0,0 +1,28 @@ +\documentclass[a4paper]{article} + +\title{De semantiek van Smurf} %todo working title +\author{Ward Theunisse, Evi Sijben en Camil Staps} + +% Standaard packages +\usepackage[hidelinks]{hyperref} +\usepackage[utf8]{inputenc} +\usepackage[dutch]{babel} +\usepackage{geometry} + +% Taakspecifieke packages +\usepackage{amsmath} +\usepackage{stackrel} +\usepackage{syntax} + +% Eigen packages +\usepackage{smurf} + +\begin{document} + +\maketitle + +% todo intro +\input{def} + +\end{document} + |