Given a Boolean expression B and a command C, the command
specifies a computation that repeatedly executes C, as long as B is satisfied. Such a computation need not terminate. It might in fact be defined as a countable sequence of if-commands :
If after finitely many steps a state is reached satisfying 
, then that
state is the result of the computation, otherwise the result is the state 
.
The given constructs suffice to specify all functions that are computable over a given data structure. Moreover, by structural induction it is not hard to see that every program C may be transformed into an equivalent program containing only a single while-loop, i.e. into a program of the form
where I is a sequence of assignments and D is a straight-line program.