For those new to programming, here's a short digression, adapted from chapter 8 of Edsger Dijkstra's book, A Discipline of Programming [Dijkstra76].

Let's say we need to set a variable, m, to the larger of two input values, a and b. We start with a state we could call “m undefined”. Then we want to execute a statement after which we are in a state of “(m==a or m==b) and m≥a and m≥b”.

Clearly, we need to choose correctly between two different assignment statements. We need to do either m=a or m=b. How do we make this choice? With a little logic, we can derive the condition by taking each of these statement's effects out of the desired end-state.

For the statement m=a to be the right statement to use, we show the effect of the statement by replacing m with the value a, and examining the end state: (a==a or a==b) and a≥a and a≥b. Removing the parts that are obviously true, we're left with a≥b. Therefore, the assignment m=a is only useful when a≥b.

For the statement m=b to be the right statement to establish the necessary condition, we do a similar replacement of b for m and examine the end state: (b==a or b==b) and b≥a and b≥b. Again, we remove the parts that are obviously true and we're left with b≥a. Therefore, the assignment m=b is only useful when b≥a.

Each assignment statement can be “guarded” by an appropriate condition.

if a>=b: m=a
elif b>=a: m=b

Is the correct statement to set m to the larger of a or b.

Note that the hard part is establishing the post condition. Once we have that stated correctly, it's relatively easy to figure the basic kind of statement that might make some or all of the post condition true. Then we do a little algebra to fill in any guards or loop conditions to make sure that only the correct statement is executed.

Successful Loop Design. There are several considerations when using the while statement. This list is taken from David Gries', The Science of Programming [Gries81].

While these conditions seem overly complex for something so simple as a loop, many programming problems arise from missing one of them.

Gries recommends putting comments around a loop showing the conditions before and after the loop. Since Python provides the assert statement; this formalizes these comments into actual tests to be sure the program is correct.

Designing a Loop. Let's put a particular loop under the microscope. This is a small example, but shows all of the steps to loop construction. We want to find the least power of 2 greater than or equal to some number greater than 1, call it x. This power of 2 will tell us how many bits are required to represent x, for example.

We can state this mathematically as looking for some number, n, such that 2^n-1 < x ≤ 2ⁿ. This says that if x is a power of 2, for example 64, we'd find 2⁶. If x is another number, for example 66, we'd find 2⁶ < 66 ≤ 2⁷, or 64 < 66 ≤ 128.

We can start to sketch our loop already.

assert x > 1
... initialize ...
... some loop ...
assert 2**(n-1) < x <= 2**n

We work out the initialization to make sure that the invariant condition of the loop is initially true. Since x must be greater than or equal to 1, we can set n to 1. 2^1-1=2⁰=1 < x. This will set things up to satisfy rule 1 and 2.

assert x > 1
n= 1
... some loop ...
assert 2**(n-1) < x <= 2**n

In loops, there must be a condition on the body that is invariant, and a terminating condition that changes. The terminating condition is written in the while clause. In this case, it is invariant (always true) that 2**(n-1) < x. That means that the other part of our final condition is the part that changes.

assert x > 1
n= 1
while not ( x <= 2**n ):
    n= n + 1
    assert 2**(n-1) < x
assert 2**(n-1) < x <= 2**n

The next to last step is to show that when the while condition is true, there are more than zero trips through the loop possible. We know that x is finite and some power of 2 will satisfy this condition. There's some n such that n-1 < log2 (x) < = n that limits the trips through the loop.

The final step is to show that each cycle through the loop reduces the trip count. We can argue that increasing n gets us closer to the upper bound of log2 (x).

We should add this information on successful termination as comments in our loop.