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,
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
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
x = -4, then it first sets
-5, then sets
0, and the overall effect is to set
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
-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.