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: 1108a1,9a0ff0bffdf63657
X-Google-Attributes: gid1108a1,public
X-Google-Thread: 103376,4b06f8f15f01a568
X-Google-Attributes: gid103376,public
From: Matthew Heaney <matthew_heaney@acm.org>
Subject: Re: Software landmines (loops)
Date: 1998/09/17
Message-ID: <m3vhmn6hl8.fsf@mheaney.ni.net>#1/1
X-Deja-AN: 391898127
Sender: matt@mheaney.ni.net
References: <m3ogt3qgca.fsf@mheaney.ni.net> <35f23ce2.7649859@news.erols.com>
 <6snn1b$c90$1@hirame.wwa.com> <35ef7dff.24318728@news.erols.com>
 <EyrHEC.My1@ecf.toronto.edu> <35f79e53.98130474@news.erols.com>
 <slrn6v1k5p.1lb.jdege@jdege.visi.com> <m3emtq4vhd.fsf@mheaney.ni.net>
 <m34sum4pyy.fsf@mheaney.ni.net> <35F56A3B.8DEA51A7@draper.com>
NNTP-Posting-Date: Wed, 16 Sep 1998 18:19:04 PDT
Newsgroups: comp.lang.eiffel,comp.object,comp.software-eng,comp.lang.ada
Date: 1998-09-17T00:00:00+00:00
List-Id: <comp.lang.ada>

Tim McDermott <mcdermott@draper.com> writes:

> Matthew Heaney wrote:
> 
> > (start of quote)
> > The dowhiledo structure has general form
> >
> >   do1
> >     dopart1
> >   while
> >     whiletest
> >   do2
> >     dopart2
> >   od
> 
> snip
> 
> > Conclusion: Feel free to exit from the middle of a loop.
> 
> As defined, you can exit from the middle of a dowhiledo, but not from the top
> or bottom.  This is still a se/se structure.  You can't use this structure to
> justify multiple returns.

But if dopart1 or dopart2 is just a "skip" statement, then it reduces to
a top or bottom exit.  For example, making the dopart2 part a "skip" is
just our old friend dountil (except for the sense of the predicate).

Remember: the goal is to satisfy the postcondition, and to be able to
prove that you do.  I can and do justify multiple returns, by proving
that the postcondition is indeed satisfied.