\subsection{The language While}
\label{sec:intro:while}
We use the language While described by~\cite{proganal} as a running example. In
its definition, the following meta-variables are used:

\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'
		\alt $a_1 = a_2$
		| $a_1 \le a_2$
		| $\lnot b$
		| $b_1 \land b_2$

	<Stm> ::=
		  $x$ `:=' $a$
		| `skip'
		| `while' $b$ `do' $S$
		\alt `if' $b$ `then' $S_1$ `else' $S_2$
		| $S_1$ `;' $S_2$
\end{grammar}

Since we do not discuss parsing in this paper, we need not modify the syntax to
make it deterministic. Standard operator precedence applies for \<AExpr> and
\<BExpr>; for \`while' and \`if' we let it be clear from the context where the
block ends. Lastly, 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 the syntax constructs should be intuitive. As an example,
after executing the following program, \verb$y$ will have been divided by $2$:

\begin{while}
	\whcomp%
		{\whass{x}{y}}
		{\whwhile{\whnotp{\whle{x}{0}}}%
			{(\whcomp%
				{\whass{x}{x-2}}
				{\whass{y}{y-1}})
			}
		}
\end{while}

Programs in While are executed in a \emph{state} which maps variables to
integers.