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].
- The body condition must be initialized properly.
- At the end of the suite, the body condition is just as true
as it was after initialization. This is called the
invariant, because it is always true during the
loop.
- When this body condition is true and the while condition is
false, the loop will have completed properly.
- When the while condition is true, there are more iterations
left to do. If we wanted to, we could define a mathematical function
based on the current state that computes how many iterations are left
to do; this function must have a value greater than zero when the
while condition is true.
- Each time through the loop we change the state of our
variables so that we are getting closer to making the while condition
false; we reduce the number of iterations left to do.
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
n
.
This says that if x is a power of 2, for example 64,
we'd find 26. If x is
another number, for example 66, we'd find 26
< 66 ≤ 27, 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.
21-1=20=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.
