Update inleiding opdracht 8; update inleiding paper

3 files changed, 75 insertions, 1 deletions

diff --git a/paper/intro-while.tex b/paper/intro-while.tex
index 5824d0e..e35c07a 100644
--- a/paper/intro-while.tex
+++ b/paper/intro-while.tex
@@ -1,3 +1,60 @@
 \subsection{The language While}
 \label{sec:intro:while}
-%todo
+We will use the language While described by~\cite{proganal} as a running
+example. In its definition, we use the following meta-variables:
+
+\begin{tabbing}
+	\qquad \= $n$ \enspace\= denotes an integer; \\
+	\> $x$ \> a variable name; \\
+	\> $a$ \> an arithmetical expression (\synt{AExpr}); \\
+	\> $b$ \> a boolean expression (\synt{BExpr}); and \\
+	\> $S$ \> a statement (\synt{Stm}).
+\end{tabbing}
+
+The syntax we will use is:
+
+\grammarindent=6em
+\begin{grammar}
+	<AExpr> ::= $n$
+		| $x$
+		| $a_1 + a_2$
+		| $a_1 \times a_2$
+		| $a_1 - a_2$
+
+	<BExpr> ::= `true'
+		| `false'
+		| $a_1 = a_2$
+		| $a_1 \le a_2$
+		| $\lnot b$
+		| $b_1 \land b_2$
+
+	<Stm> ::=
+		  $x$ `:=' $a$
+		| $S_1$ `;' $S_2$
+		| `skip'
+		| `if' $b$ `then' $S_1$ `else' $S_2$ `endif'
+		| `while' $b$ `do' $S$ `done'
+\end{grammar}
+
+The syntax of statements has been adapted slightly to make it deterministic.
+The grammar for \<Aexpr> and \<BExpr> has not been made deterministic for
+brevity's sake; standard operator precedence applies.
+
+We assume that composition (\whcomp{$S_1$}{$S_2$}) is right associative. We
+ignore all whitespace, and do not allow variable names that are reserved
+keywords such as \whskip.
+
+The semantics of these syntax constructs should be intuitive. As an example,
+after executing the following program \verb$x$ will approximate \verb$y$
+divided by $2$:
+
+\begin{while}
+	\whcomp%
+		{\whass{x}{0}}
+		{\whwhile{y > 0}%
+			{\whcomp%
+				{x := x + 1}%
+				{y := y - 2}%
+			}
+		}
+\end{while}
diff --git a/paper/paper.tex b/paper/paper.tex
index 1cb89cd..d036bda 100644
--- a/paper/paper.tex
+++ b/paper/paper.tex
@@ -5,6 +5,16 @@
 \usepackage[hidelinks]{hyperref}
 \usepackage{natbib}
 
+\usepackage{enumitem}
+
+\usepackage{syntax}
+\renewcommand\litleft{\bgroup\tt}
+\renewcommand\litright{\egroup}
+\def\<#1>{\synt{#1}}
+\def\`#1'{\lit{#1}}
+
+\usepackage{while}
+
 \title{Imperative code interpretation in a functional style}
 \author{Camil Staps}
 
diff --git a/paper/while.sty b/paper/while.sty
new file mode 100644
index 0000000..1c61164
--- /dev/null
+++ b/paper/while.sty
@@ -0,0 +1,7 @@
+\newenvironment{while}{\medskip}{\medskip}
+
+\def\whskip{\texttt{skip}}
+\def\whass#1#2{\texttt{#1 := #2}}
+\def\whcomp#1#2{#1\texttt{;} #2}
+\def\whif#1#2#3{\texttt{if #1 then #2 else #3 endif}}
+\def\whwhile#1#2{\texttt{while #1 do #2 done}}