From mboxrd@z Thu Jan 1 00:00:00 1970 X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me X-Spam-Level: X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00 autolearn=ham autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: 103376,14f7200925acb579 X-Google-Attributes: gid103376,public From: ka@exit109.com (Kenneth Almquist) Subject: Re: No Go To's Forever! Date: 2000/04/16 Message-ID: X-Deja-AN: 611995401 References: <8bdbof$t19$1@nnrp1.deja.com> <8berdq$j2p$1@nnrp1.deja.com> Organization: Posted via Supernews, http://www.supernews.com Newsgroups: comp.lang.ada Originator: ka@exit109.com (Ken Lamquist) X-Complaints-To: newsabuse@supernews.com Date: 2000-04-16T00:00:00+00:00 List-Id: 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 , where D1 is a permutation of D and J is in D'range. Let Out_Of_Order(D) be the number of pairs 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, > 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 -> 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 such that I < K and /= , 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 = M(I, K). Since M is bijective, the number of out of order pairs, exclusive of , 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 <> 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