A small imperative programming language whose programs are based on a signature Σ and are made from assignments, sequential composition, conditional statements, and while statements. Programs in the language are defined, using an abbreviated BNF notation, by
where
x is any variable,
t is any term over the signature Σ
b is a Boolean term, and
S, S1, and
S2 are
while programs. The role of the signature is to define the data types (and hence the types of variables needed) and the basic operations on data (and hence the terms that appear in assignments). The
while programming language can compute functions and sets on any algebra with signature Σ. When applied to the simple algebra
of natural numbers, the
while programs compute all partial recursive functions. The
while language is an important language for the theoretical analysis of ideas about imperative languages. It is easily extended by adding constructs, such as the concurrent assignment,
repeat and
for statements, and nondeterministic constructs (like the random assignment
x ≔ ?).