# Semantics of while loops (Programming Languages)

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.