Semantics of while loops

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 := x-1,

then we are interested in solutions to the equation F(W) = W, where

F(X) = if x <> 0 then (x := x-1; 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.