Re: No Go To's Forever!

[ka@exit109.com (Kenneth Almquist)]

Robert Dewar wrote:
> But there really is a very fundamental point here. If you want
> to study it further, try generating the full denotational
> semantics and in fact try generating the full proof conditions.
> That will make things clearer I think.

Here is the "one loop" version of the algorithm, with statement
numbers added for reference:

1      J := D'first;
2      while J < D'last loop
3          if D (J) >= D (J + 1) then  -- sorted so far
4            J := J+1;                 -- continue
5          else
6            Swap (D (J), D (J + 1));  -- out of order, move item
7            J := D'first;             -- and start over
8          end if;
9      end loop;

To avoid special cases in the rest of the analysis, we first consider
the case where D'last < D'first.  To prove termination in this case,
we observe that when the loop is first encountered, J = D'first, which
is greater than D'last, so the loop is never executed.  Since the
loop is never executed, it cannot be an infinite loop.  To prove
correctness, we observe that  if D'last < D'first, then D has only
one possible value, which is sorted by definition.  Therefore the
value of D is unchanged by this algorithm, and D is sorted when the
algorithm terminates.

When D'first <= D'last, the loop invariant is
	(1) J in D'range and
	(2) D(D'first .. J) is sorted and
	(3) D is a permutation of the original D.

Condition (1) holds on initial entry to the loop because statement 1
makes it true.  Considition (2) holds on initial entry to the loop
because J = D'first, and a one element array is sorted by definition.
Condition (3) holds because D has not yet been modified.

The loop preserves condition (1) because the only statements that
modify J are statements 4 and 7.  The condition on the while loop
ensures means that J < D'last is a precondition to statement 4.
After adding 1 to J, J will be less than or equal to  D'last.
Statement 7 preserves condition (1) because D'first is in D'range.

The loop preserves condition (2).  Presonditions of statement 4 are
D(D'first .. J) is sorted and D(J) >= D(J+1).  Since we are sorting
in descending order (largest element first), these preconditions
imply that D(D'first .. J+1) is sorted.  Thus D(D'first .. J) is
sorted after J is incremented.  Condition (2) is true after
statement 7 because a one elment arrary is sorted by definition.

The loop preserves condition (3) because the only modifications to
D are due to the swap operation in statement 6.  A swap operation
always results in the value of D being a permuation of the previous
value of D.

On exit from the loop, we have J <= D'last (due to condition 1 of
the loop invariant) and J >= D'last due to the condition on the
while loop.  Thus J = D'last and condition 2 assures us that D is
sorted.  Condition 3 assures us that the sorted values correspond
to the original values of D.  Therefore the algorithm sorts D.

To prove termination, we observe that the variables which change
while the loop is executing are D and J.  Let S be the set of all
ordered pairs <D1, J1>, where D1 is a permutation of D and J is in
D'range.  Let Out_Of_Order(D) be the number of pairs <I, J> such
that I < J and D(I) < D(J).  (If D is sorted, then Out_Of_Order(D)
will be zero.)  We define a partial ordering on the possible values
of D by sayiung that D1 > D2 if Out_Of_Order(D1) < Out_Of_Order(D2).
The possible values of J are already ordered by the integer ">".
We now order S lexographically.  In other words, <D1, J1> > <D2, J2>
iff D1 > D2 or (D1 = D2 and J1 > J2).

Each iteration of the while loop will change the state from some state
S1 to some new state S2.  We observe that S2 > S1.  If the condition
tested on line 3 is true, then statement 4 will be executed, which
increments J and so S2 > S1.  If the condition is false, then
statement 6 will be executed.  Let M be the mapping <I1, K1> ->
<I2, K2> where
    I2 = if I1 = J then J+1 else if I1 = J+1 then J else I1
    K2 = if J1 = J then J+1 else if K1 = J+1 then J else K1
For all <I, K> such that I < K and <I, K> /= <J, J+1>, the pair
D(I) and D(K) are out of order after statement 6 is executed iff
D(I2) and D(K2) are out of order before statement 6 is executed,
order, where <I2, K2> = M(I, K).  Since M is bijective, the
number of out of order pairs, exclusive of <J, J+1>, is not
changed by the execution of statement 6.  The conditional on
line 3 ensures that the pair D(J), D(J+1) is out of order before
statement 6 is executed.  After the swap operation in statement 6
is performed, this pair will no longer be out of order, so the
number of out of order pairs will be decreased by one and again
we have S2 > S1.

The number of elements in S is finite, because S is the cross product
of a finite set of permutations (Ada does not permit an array with
an infinite number of elements to be declared) and a finite set of
integer values (again, D'range must be finite).  Since the program
state inside the loop consists of a series of nonrepeating values
chosen from a finite set, the loop must terminate.  This concludes
the proof.

Now consider the two loop version, rewritten using the 'first and
'last attributes to match the previous code:

1   <<Do_It_Again>>
2      for J in D'first .. D'last - 1 loop
3          if D (J) < D (J + 1) then
4            Swap (D (J), D (J + 1));
5            goto Do_It_Again;
6          end if;
7      end loop;

As with the previous algorithm, we cover the case where D'first >
D'last separately.  By the same argument, the algorithm terminates
with the correct result in this case.

To handle the normal case (D'first <= D'last), we start with the
"for" loop on line 2.  Rather than define a loop invariant, we
define a condition that will hold on entry to the loop and will
be preserved by the loop unless conditional on line 3 becomes true.
This "semi-invariant" is:
	(1) J in D'range, and
	(2) D(D'first .. J) is sorted

Condition (1) holds on entry to the loop because D'first is in
D'range.  Condition (2) holds on entry to the loop because a one
element array is sorted by definition.

The loop preserves condition (1) because the loop will exit when J =
(D'last - 1) + 1.  The loop preserves condition (2) unless the
conditional on line 3 becomes true.  Since we are sorting in
descending order, if the conditional on line 3 is false then when we
increment J at the end of the loop condition (2) remains true.

The program terminates when the "for" loop exits normally (as opposed
to via the goto statement).  When this happens, the "semi-invariant"
for the "for" loop will be true becase if the conditional on line 3
had become true the "for" loop would have exited via the goto statement
instead of exiting normally.  The loop conditional implies that J =
(D'last - 1) + 1 = D'last.  Thus D(D'first .. D'last) is sorted.

To complete the proof of correctness, we need to add a global
invariant to the program:
	The value of D is a permuation of the original value of D.

This invariant is true at the start of the program because the
original value of D is a permuation of itself.  The program preserves
this invariant because the only statement that modifies D is the
swap operation at line 4, and swaping preserves the invariant.

Thus the final value of D is a sorted permutation of the original
value of D, which proves partial correctness.

To prove termination, we first observe that the "for" loop on line 2
will terminate because all "for" loops terminate.  We then define an
ordering on the set of all possible values of D using the same
definition as we used for the other algorithm.  Using an argument
similar to the one we used for the "one loop" algorithm, we prove that
the value of D after statement 4 is executed will be greater than the
value of D before statement 4 is executed (using the ordering on the
values of D specified in the preceding sentence).  Since the number of
possible values of D is finite, and since no statements other than
statement 4 modify D, statement 4 can only be executed a finite number
of times.  Therefore the goto at line 5 can only be executed a finite
number of times, and both loops in the program will terminate.
Therefore, the program will terminate, which completes the proof.

This is considerably shorter than the proof for the "one loop"
algorithm, but most of the difference is because I haven't repeated
details that were spelled out in the first proof.  The proof of
termination is simpler because we don't have to worry about J; it
is now the control variable of a "for" loop.  On the other hand,
the second algorithm has a more complicated flow of control, which
complicates the proof in various small ways.  Overall I don't see
much difference in the complexity of the proofs.

What does differ, at least for me, is the difficulty of finding the
proofs.  The first proof is basicly a "fill in the blanks" proof.  I
know the overall structure of a correctness proof for a "while" loop;
the work consists of filling in the details.  The second algorithm
consists of two overlapping loops.  I've never tried to prove
correctness of an algorithm with this structure before, and thus had
no idea of how to begin to construct the proof.

I suppose that this is a matter of inexperience; if I had done more
work with correctness proofs I might have found both proofs about
equally easy to construct.  I expect that many people besides myself
lack experience in proving correctness of programs containing goto
statements, because goto statements are used infrequently in modern
software, and even less frequently in computer science texts.
				Kenneth Almquist