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=0.1 required=5.0 tests=BAYES_00,PDS_OTHER_BAD_TLD autolearn=no autolearn_force=no version=3.4.4 X-Google-Language: ENGLISH,ASCII-7-bit X-Google-Thread: fac41,9a0ff0bffdf63657 X-Google-Attributes: gidfac41,public X-Google-Thread: 103376,4b06f8f15f01a568 X-Google-Attributes: gid103376,public X-Google-Thread: f43e6,9a0ff0bffdf63657 X-Google-Attributes: gidf43e6,public X-Google-Thread: 1108a1,9a0ff0bffdf63657 X-Google-Attributes: gid1108a1,public From: jtc@dimensional.com (Jim Cochrane) Subject: Re: Software landmines (loops) Date: 1998/09/02 Message-ID: <6siqo0$hiv@flatland.dimensional.com> X-Deja-AN: 387048972 References: <6sf4gl$hb6@flatland.dimensional.com> Organization: Dimensional Communications NNTP-Posting-Date: Wed, 02 Sep 1998 01:05:47 MDT Newsgroups: comp.lang.eiffel,comp.object,comp.software-eng,comp.lang.ada Date: 1998-09-02T00:00:00+00:00 List-Id: In article , Matthew Heaney wrote: >jtc@dimensional.com (Jim Cochrane) writes: > >> class STACK [G] ... >> is_equal (other: STACK [G]): BOOLEAN is >>... (See below for entire original article.) You have provided a good, thorough analysis supporting the argument that my version is more complex, and I think you've convinced me. It is difficult to determine what the loop is doing when the exit condition is so complex. Also, I agree with your argument for separating the test of the two stack sizes being unequal into a separate statement from the loop body, since this does make the code easier to understand, as well as more efficient. I would like to now propose an algorithm that separates the equality check from the loop and that also returns only at the end of the function. I will include a loop invariant in the code, and I'll then copy your algorithm, inserting a loop invariant. The point of this exercise will be to see if how each idiom affects the traditional technique of analyzing a loop by means of the loop invariant. (In my version I have changed the type from STACK to ARRAY, since this operation is not really compatible with the STACK abstraction and because it makes expressing the loop invariant easier - using indexes instead of iterators. [Of course, a stack internally implemented as an array will be able to use this algorithm.]) My new version: class ARRAY [G] ... is_equal (other: ARRAY [G]): BOOLEAN is require arg_not_void: other /= Void local i: INTEGER do if count /= other.count then Result := false else from i := 1 invariant -- for_all j member_of {1..i - 1} it_holds -- Current @ j = other @ j until i > count or Current @ i /= other @ i loop i := i + 1 end check (i - 1 /= count) implies (Current @ i /= other @ i) count = other.count end Result := i - 1 = count end ensure -- Result = (count = other.count and for_all j member_of -- {1..count} it_holds Current @ j = other @ j) end Your version: function "=" (L, R : Stack_Type) return Boolean is begin if L.Top /= R.Top then return False; end if; for Index in Positive range 1 .. L.Top loop -- INV: for_all j member_of {1..Index - 1} it_holds -- L.Items (j) = R.items (j) if L.Items (Index) /= R.Items (Index) then -- not (Index - 1 = L.Top) return False; end if; end loop; -- L.Top = R.Top and Index - 1 = L.Top return True; -- Postcondition: Result = (L.Top = R.Top and for_all j member_of -- {1..L.Top} it_holds Current @ j = other @ j) end "="; When we compare these two implementations, your earlier comments (comparing your implementation with an implementation someone else proposed [I believe it was Loryn] that is very similar to mine) mostly still apply - especially the point that your loop termination condition is simpler than mine. But since you include what is in essence a hidden loop termination condition [L.Items (Index) /= R.Items (Index)], as someone else pointed out, the complexity of two termination conditions is still there. My routine does nest the loop within an else statement; but yours nests an if within a loop. Which is better? I don't know - I'm not sure it matters that much. In addition to the loop invariant, I have added a postcondition to both routines (which is the same for both routines; also, the loop invariant is the same for both routines). I have also added a couple other assertions to document program state at those points. Looking at my routine, you can easily determine that the loop invariant is correct and that, as a result, if i - 1 /= count then (although the loop invariant is true), Current @ i /= other @ i and the result will be false; otherwise, the result will be true. The postcondition of the routine follows straightforwardly from that. Looking at your routine, you need to check 3 different places to check that the postcondition is upheld, the 3 return statements: In the first if statement, in the second if statement in the middle of the loop, and at the end of the routine. This is a pretty straightforward process, but I think it makes it a little more difficult in that you need to check 3 separate locations, including in the middle of the loop. My conclusion at this point is that I don't see a noticable advantage to either idiom. I prefer the one that only exits at the end of the routine, but I don't think I would object to seeing your version in a code inspection. (Of course, if the code was written in Eiffel, your version would not be possible.) The one remaining question I have is: How will the two idioms compare with a more complex algorithm? I have a suspicion that having multiple return points with a more complex algorithm will make the routine postcondition and the loop invariant harder to verify than with the return-at-the-end idiom. Of course, I can't confirm that until I examine some examples. I think this has been a good discussion and (contrary to another poster's implication that this is simply a loop structuring war) I (and I would hope others) have learned from it. For comparison, here is my original version with loop invariant and postcondition added (and using indexes instead of iterators) (I also changed the "or else" term to "or", since they are semantically equivalent and the latter is easier to understand for those who don't know Eiffel well): class ARRAY [G] ... is_equal (other: ARRAY [G]): BOOLEAN is require arg_not_void: other /= Void local i: INTEGER do from i := 1 invariant -- for_all j member_of {1..i - 1} it_holds Current @ j = other @ j until i > count or i > other.count or Current @ i /= other @ i loop i := i + 1 end check i - 1 = count and i - 1 = other.count or count /= other.count or Current @ i /= other @ i end Result := i - 1 = count and i - 1 = other.count ensure -- Result = (count = other.count and for_all j member_of -- {1..count} it_holds Current @ j = other @ j) end In article , Matthew Heaney wrote: >jtc@dimensional.com (Jim Cochrane) writes: > >> class STACK [G] ... >> is_equal (other: STACK [G]): BOOLEAN is >> -- Are all items in Current equal to all item in other? >> require >> other /= Void >> local >> i1, i2: STACK_ITERATOR >> do >> !!i1.make (Current); !!i2.make (other) >> from >> i1.start; i2.start >> until >> i1.after or i2.after or else i1.item /= i2.item >> loop >> i1.forth; i2.forth >> end >> Result := i1.after and i2.after >> end >> >> I don't think this is particularly hard to understand or maintain, >> plus it is simpler than the algorithm below - it eliminates the if >> statement at the beginning. (STACK_ITERATOR behavior is, hopefully, >> obvious - i.item means the value of item at the current cursor >> position of i.) I threw this together just for this post, so >> apologies if there are any bugs (and bonus points to those that find >> them :-) ). > >I think this is a real brain teaser. Let me show you how I try to >unravel it. > >Let's start by making a decision table for the loop predicate: > > 1 2 3 4 5 6 7 8 >i1.after T T T T F F F F > >i2.after T T F F T T F F > >i1.item /= i2.item T F T F T F T F > >As you can see, there are 8 rules, which just exceeded the cognitive >limits of most of human population. Already, we're in trouble. But >there's more trouble ahead. > >The last part of the predicate uses a short-circuit form, so we're going >to have to prune the table, by removing the rules in which i1.after and >i2.after are both false. > >Or is it both true??? As I'm writing this post, I've already spent >several minutes trying to figure out when the last part of the predicate >actually gets executed. > >And I don't even know what the evaluation order rules are in Eiffel. >Does > > i1.after or i2.after or else i1.item /= i2.item > >mean > > (i1.after or i2.after) or else i1.item /= i2.item > >or > > i1.after or (i2.after or else i1.item /= i2.item) > >Hmmm? Maybe these expressions both have the same value. I don't know, >but I'm obligated to find out. This is mental work I shouldn't have to >do, and I'll probably get it wrong. > >So I gotta ask: Is this a program, or an IQ test? > >I'll just use my little decision table friend again, to help me crack >the secret of what result the predicate acually delivers. > > 1 2 3 4 5 6 7 8 >i1.after T T T T F F F F > >i2.after T T F F T T F F > >i1.item /= i2.item - - - - - - T F > >The dash (-) means "does not matter." > >So the item test only influences the result (I think) when i1.after and >i2.after are both false. (Gee, that's what I originally thought. A >miracle happened, and I guessed right! But how many other times will I >be this lucky?) > >Now I have to actually figure out what the result of the predicate is: > > 1 2 3 4 5 6 7 8 >i1.after T T T T F F F F > >i2.after T T F F T T F F > >i1.item /= i2.item - - - - - - T F > >predicate has value T T T T T T T F > >Ah, so that's the secret! The loop teriminates (I think) when all >sub-predicates yield false. > >Revealed at last, after several minutes of careful analysis, which I >probably screwed up. > >But wait, I did screw up! Loop termination in Eiffel has opposite the >traditional sense, which is to terminate when the predicate is false. >So the loop terminates when the predicate is true. Whew! > >How many programmers do you think will take the time to figure all this >out? How many programmers even know how to use a decision table? > >One more issue with this example. Following termination, calculating >the result, > > Result := i1.after and i2.after > >means i1.after and i2.after get tested again. Why? They were tested >already, in the loop. Why test them twice? > >Maybe I get bonus points for being able to decipher this, but is that >how we should write software? Be rewarding those who perform mental >gymnastics? > >I hope not. -- Jim Cochrane jtc@dimensional.com