1 files changed, 58 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}