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.2 required=5.0 tests=BAYES_00,INVALID_MSGID, REPLYTO_WITHOUT_TO_CC 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: 1108a1,9a0ff0bffdf63657 X-Google-Attributes: gid1108a1,public X-Google-Thread: f43e6,9a0ff0bffdf63657 X-Google-Attributes: gidf43e6,public X-Google-Thread: 103376,4b06f8f15f01a568 X-Google-Attributes: gid103376,public From: "John G. Volan" Subject: Mid-Loop 'Until' Proposal [was: Software landmines (loops)] Date: 1998/09/03 Message-ID: <35EF3DCD.CC060E37@ac3i.dseg.ti.com>#1/1 X-Deja-AN: 387679373 Content-Transfer-Encoding: 7bit References: <902934874.2099.0.nnrp-10.c246a717@news.demon.co.uk> <6r1glm$bvh$1@nnrp1.dejanews.com> <6r9f8h$jtm$1@nnrp1.dejanews.com> <6renh8$ga7$1@nnrp1.dejanews.com> <6rf59b$2ud$1@nnrp1.dejanews.com> <6rfra4$rul$1@nnrp1.dejanews.com> <35DBDD24.D003404D@calfp.co.uk> <6sbuod$fra$1@hirame.wwa.com> <35f51e53.48044143@ <904556531.666222@miso.it.uq.edu.au> <6sgror$je8$3@news.indigo.ie> <6sh3qn$9p2$1@hirame.wwa.com> <6simjo$jnh$1@hirame.wwa.com> <6sjk3p$4tc$1@hirame.wwa.com> <9hdH1.464$08.176350@news.giganews.com> Followup-To: comp.lang.eiffel Content-Type: text/plain; charset=us-ascii Organization: Raytheon Systems Company, Advanced C3I Systems Mime-Version: 1.0 Reply-To: johnvolan@sprintmail.com Newsgroups: comp.lang.eiffel,comp.object,comp.software-eng,comp.lang.ada Date: 1998-09-03T00:00:00+00:00 List-Id: [Followups trimmed to comp.lang.eiffel since this is an Eiffel-specific language extension proposal. If folks in the other groups want to echo their followups there, they can do so on their own nickel. :-) ] On Wed, 2 Sep 1998 10:20:28 -0500, Dan Higdon wrote: > ... > As an aside, a valid (IMHO) Eiffel extension would be to allow loops a > little more freedom (yeah, I know, "everyone's a language designer" :-): > > -- standard > from until loop > > end > > -- post test > from loop > > until end > > -- in test > from loop > > until else > > end > > Ignoring {in}variants for simplicity. (I suppose {in}variants would need to > hold > true at the "until".) > > so, our example becomes > from > > loop > Get (N) > until > not N > else > > end > Hey, great minds think alike! ;-) On Tue, 01 Sep 1998 20:23:47 -0700, John Volan wrote: > ... > However, suppose Eiffel allowed mid-body loop exits, say with the > following sort of syntax: > > equal (l, r: LIST): BOOLEAN is > require > l /= Void and r /= Void > do > Result := (l.count = r.count) > if Result then > from > l.start; r.start > until > l.off > loop > Result := (l.item = r.item) > until > not Result > then > l.forth; r.forth > end > end > end ... > > out: STRING is > do > Result := "{" > if not empty then > from > start > loop > Result.append (item.out) > forth > until > after > then > Result.append (", ") > end > end > Result.append ("}") > end > I like Dan's 'else' better than my 'then' -- makes more sense. Note that Dan's proposal is to have only one 'until' clause per loop, but my first example above suggests that there could be more than one. Semi-formally, the syntax would be: from Compound [invariant Assertion] [variant [Tag_mark] Integer_expression] [until Boolean_expression] -- standard exit loop Compound {until Boolean_expression -- mid-body exit else Compound} [until Boolean_expression] -- end-of-body exit end [] = optional (0 or 1) {} = multiple (0 or more) If this syntax were allowed, then the postcondition for the loop would be the logical 'or' of all the Boolean_expressions appearing in the 'until' clauses. Would that be sufficiently well-defined to satisfy the principles of Design By Contract? Note that this syntax would make 'until' optional. Omitting 'until' would yield an infinite loop. Perhaps a validity constraint might be imposed requiring at least one 'until' somewhere in the loop (though not necessarily at the top of the body). On the other hand, there are some legitimate applications for deliberately infinite loops, so perhaps this constraint would be unnecessary. Then again, the Self-Documenting Code principle would suggest that "deliberate infinity" should be a highly conspicuous property for a loop. So it may be desirable to force a programmer to say 'until False' on such a loop. Dan alludes to the problem of what to do about loop invariants and variants. If a loop contained multiple 'until' clauses, my guess is that the invariant would have to hold at each 'until', since the loop could potentially exit at those points. As for the variant, that is somewhat more ticklish. At what point should the variant be tested for non-negativity and for monotonic decrease? Perhaps at the "top" (at the start of the first Compound after 'loop'). That way, a given iteration of the loop isn't obligated to satisfy the variant until it's had a chance to execute all of its Compounds without exiting on an 'until'. Thoughts, folks? -- indexing description: "Signatures for John Volan" self_plug: "Ex Ada guru", "Java 1.1 Certified", "Eiffelist wannabe" two_cents: "Java would be even cooler with Eiffel's generics, % %assertions/DBC, true MI, feature adaptation, % %selective export, uniform access, etc., etc..." class JOHN_VOLAN_SIGNATURE inherit SIGNATURE invariant disclaimer: not (opinion implies employer.opinion) end -- class JOHN_VOLAN_SIGNATURE