# 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.