Re: Software landmines (loops)

[Jean-Marc Jezequel <Jean-Marc.Jezequel@irisa.fr>]

IMHO, Dijkstra's point with se/se loops is first on *correctness*, that
is linked with provability. This is the most important thing from a
software engineering point of view. Maintenability comes second.
Readability comes third (but is actualy linked to maintenability).
Easyness of writing comes *last*.
(well, in the real world issues such as efficiency or more often costs
and delay sinterfere at any level in this hierarchy;-). I agree with Bob
Martin's point of view on the role of engineers: making trade-offs).

According to this point of view, the point is not to craft a piece of
code and throw it to the tester in a kind of simulated annealing until
it works. IMHO the professional engineer should design a piece of code
as trivial as a loop *in such a way that it can be proven correct*.
At least one systematic way of doing this have been documented by the
structured programming folks (Dijkstra, Hoare...).
Let me recall it in the context of the current thread on list equality
implemented with a loop:

equal (l,r: LIST): BOOLEAN is
        require l /= Void; r /=Void

This is a six steps process:

1. Design the loop invariant. It should provide a concise and
preferably formal description of the properties of the loop.
But even if it's not formal, it is usefull since it outline the intent.
Here, it is simply that the two list r and l are equal so far (which
could be made more formal saying that foreach i such as
0<i<l.current_index r.item(i) = l.item(i))

[For those who need refreshing on loop invariant:
It is a Boolean expression that must be true on initialization of the
loop variables, maintained with each iteration of the loop, and held to
be true at the termination of the loop. A loop invariant can be used to
reason about the correctness of a loop. see below]

2. Find the termination condition.
Here it is: either we find 2 differing elements or we reach the end of
one of the lists. That is, if Result contains the comparison result:
until not Result or l.off or r.off

So now, if the loop terminates, then the loop invariant is true and the
termination condition holds (by definition), which means that either the
lists are equal or Result=false. This property is called *partial
correctness*. Let us see how to prove total correctness.

Total correctness is just partial correctness {\em and} the proof that
the loop terminates (i.e., the termination condition eventually will 
hold). The idea of a loop variant is to characterize how each iteration
can bring the loop closer to its termination.


3. Find the variant (how the loop can advance toward its
termination).
[A loop variant is a non-negative integer expression that is decreased
by at least one at each iteration. By definition, it cannot go below
zero, thus the number of iterations of a loop with a variant is
bounded and then the loop eventually terminates.]
A suitable variant for this example is:
variant l.count-l.current_index+1

In writing the loop body, we must ensure that it is a strictly
decreasing function that takes non-negative values only.
This proof completes the partial correctness to give
the total correctness of the loop. In other words, the loop terminates
and computes the right result.


4. Write the body of the loop:

4a) First deduce from the variant the progression instruction,
4b) Then write the code corresponding to the restoration of the
invariant.

loop
   Result := l.item /= r.item -- establish invariant
   l.forth; r.forth -- progression for the variant
end

5. Write the initialization part to set up the loop invariant.

Result := True; l.start; r.start

6. Optimize, and/or modify to make it more readable
e.g., initialize Result to something less trivial:

        Result := l.first /= r.first
        from l.start; r.start
	invariant equal_so_far: --foreach i such as 0<i<l.current_index 
					-- r.item(i) = l.item(i)
        variant l.count-l.current_index+1
        until not Result or l.off --r.off omitted since l.off=>r.off
        loop
              Result := l.item /= r.item
              l.forth; r.forth
        end

7. Check your proof. Test (it's as easy to make an error in the proof as
it is in the code. Eiffel helps here by checking invariants and variants
at runtime. But the method is valid and usefull for *any* language).
Ship.

To sum up my point, when there is a documented way of doing something
(here building loops) the engineer should follow it (albeit not blindly:
she must still make appropriate trade-offs). Doing it elseway for no
good reason is not engineering: it is handcrafting (which is not
necessarily pejorative in my mouth).

-- 
Jean-Marc Jezequel               Tel : +33 299 847 192         
IRISA/CNRS                       Fax : +33 299 847 171         
Campus de Beaulieu               e-mail : jezequel@irisa.fr 
F-35042 RENNES (FRANCE)          http://www.irisa.fr/prive/jezequel