\subsection{The language While}
\label{sec:intro:while}
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}