### 6.4. The `while` loop rule

Designing with `while` loops is more involved than the other three proof rules. Such loops are treacherous because they can become infinite loops. Hardly ever is that the desired functioning of your program.

The general form:

```# [ `A` ]
while `C`:
# [ `X` ]
...
```

There are three parts to the proof rule for `while` loops.

1. You must prove that the loop terminates.

2. When the condition `C` is false, you must prove that doing nothing accomplishes the intended function `A`.

3. When the condition `C` is true, you must prove that doing intended function `X`, followed by doing intended function `A`, accomplishes the overall intended function `A`.

Here is an example that implements the same function as the `joiner` function in Section 6.3, “The definite iteration rule”. Note that we use the Python slice operator “`[:]`” to make a copy of the `pieceList` argument. If we used `pieceList` instead of the copy inside the `while` loop, the overall intended function for `joiner()` would have to specify that the value of `pieceList` becomes empty.

```def joiner2(connector, pieceList):
'''Join the pieces of pieceList with the connector.

[ (connector is a string) and
(pieceList is a list of strings) ->
return a string containing the elements of (pieceList)
separate by (connector) ]
'''
#-- 1
# [ prefix  :=  an empty string
#   result  :=  an empty string
#   L  :=  a copy of pieceList ]
prefix = ''
result = ''
L = pieceList[:]

#-- 2
# [ if L is empty ->
#     I
#   else ->
#     result  :=  result + prefix + (elements of L separated
#                 by copies of connector)
#     prefix  :=  connector
#     L  :=  empty ]
while len(L) > 0:
#-- 2 body
# [ result  :=  result + prefix + (first element of L)
#   prefix  :=  connector
#   L  :=  L minus its first element ]

#-- 2.1
# [ result  :=  result + prefix + (first element of L) ]
result += prefix + L[0]

#-- 2.2
# [ prefix  :=  connector
#   L  :=  L minus its first element ]
prefix = connector
del L[0]

#-- 3
return result
```

To prove that the `while` loop implements the correct semantics, we first prove that the loop terminates. Because each pass through the loop deletes one element of `L`, and because the loop runs until `L` is empty, it is clear that the loop cannot run forever.

The next step is to prove that the `while` loop does the right thing when `L` is empty. This also is quite clear: if `L` is empty, then `len(L)` is not greater than zero, so the loop never executes. This satisfies the special identity intended function “`I`”.

The final step is to prove the true case, when `L` is not empty.

1. First we execute the intended function for the body of the loop. This accomplishes the following state changes:

 `result` `result+prefix+L[0]` `prefix` `connector` `L` `L[1:]`
2. Then we execute the intended function for the entire `while` loop. Assuming there is at least one more element remaining in L, the new states of the three variables are:

 `result` ```result+prefix+L[0]+connector+(elements of L[1:] separated by connector)``` `prefix` `connector` `L` empty

If `L` contained only one element initially, the value of `result` in the above table becomes “`result+prefix+L[0]`”, which is the desired final state in that case.

Generally you may find yourself preferring definite iterations to indefinite (`while`) iterations, because they are easier to prove correct.