Iteration in programming-language semantics requires a more sophisticated approach than the other constructs we have seen so far: once loops are introduced, we are forced to describe the meaning of a loop’s failing to terminate, in the most extreme case for example WHILE TRUE DO SKIP.
