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.3 required=5.0 tests=BAYES_00,INVALID_MSGID 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: f43e6,9a0ff0bffdf63657 X-Google-Attributes: gidf43e6,public X-Google-Thread: 103376,4b06f8f15f01a568 X-Google-Attributes: gid103376,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/03 Message-ID: <6slbvl$be5@flatland.dimensional.com>#1/1 X-Deja-AN: 387392455 References: <6siqo0$hiv@flatland.dimensional.com> Organization: Dimensional Communications NNTP-Posting-Date: Thu, 03 Sep 1998 00:12:20 MDT Newsgroups: comp.lang.eiffel,comp.object,comp.software-eng,comp.lang.ada Date: 1998-09-03T00:00:00+00:00 List-Id: In article , Richard Melvin wrote: >In article <6siqo0$hiv@flatland.dimensional.com>, Jim Cochrane > writes >> 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 > >I'm not a fan of this line - if I was to translate it it into english, >it would come out as something like 'which exit path did I take from the >loop?'. In order to work this out, you have to reverse-engineer the >loop. > >To me, i is an implementation detail of the loop - referring to it >outside the loop almost seems to break encapsulation. Well, i is an essential component of the loop invariant, which must be true when the loop has finished, as well as at the beginning of each iteration of the loop. It may be helpful to add the following predicate to the check statement at the end of the loop, which defines the postcondition of the loop (in comments because it is not codable): -- (i - 1 = count) = for_all j member_of {1..count} it_holds -- Current @ j = other @ j In other words, if and only if the loop has iterated over the entire array, such that i = count + 1, then each element of Current is equal to the corresponding element of other (since we know that Current.count = other.count). This is precisely the loop's job, to determine if the two arrays are equal. The substitution of {1..count} for {1..i - 1} is an important step that shows how the loop invariant brings about the loop postcondition. Therefore i must be available outside of the loop. It is no more internal to the loop than the array variables Current or other. > >Perhaps it would work better with more descriptive variable names? >Perhaps numTested and numFoundEqual? >(Although that makes the -1 problematic). > >-- >Richard Melvin -- Jim Cochrane jtc@dimensional.com