Semantics of while loops (Programming Languages)
Contents
Fixpoint equations
In the lecture, I said that all treatments of the meaning of while
loops are based on the idea that the loop W = while B do S
is equivalent to the unrolled form
if B then (S; while B do S) else skip,
where skip
is the empty statement. Thus W
is (in some sense) a solution to the fixpoint equation W = F(W)
, where F(X) = if B then (S; X) else skip
.
However, this equation may have more than one solution. If we take the program,
while x <> 0 do x := x1,
then we are interested in solutions to the equation F(W) = W
, where
F(X) = if x <> 0 then (x := x1; X) else skip.
Both of the following programs represent solutions to this equation:

P1 = (x := 0)

P2 = if x >= 0 then x := 0 else abort
where abort
stands for an infinite loop. We can check this by considering the behaviour of F(Pi) when it is started with x > 0
, with x = 0
, and with x < 0
. For instance, if we start the program F(P1)
with x = 4
, then it first sets x
to 5
, then sets x
to 0
, and the overall effect is to set x
to 0
, and that is the same as what P1
itself would do. If we start F(P2)
in the same state, then it also decreases x
to 5
, then enters an infinite loop, and P2
itself also enters an infinite loop.
Since there are multiple solutions to the equation W = F(W)
, we have to ask which solution we get if we write a while
loop. The answer is plainly P2
in this instance, and generally speaking, we get the worst solution to the equation: the solution that goes into an infinite loop whenever that is possible.