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.9 required=5.0 tests=BAYES_00,FORGED_GMAIL_RCVD,
	FREEMAIL_FROM autolearn=no autolearn_force=no version=3.4.4
X-Google-Thread: 103376,e646052dc594401f
X-Google-NewGroupId: yes
X-Google-Attributes: gida07f3367d7,domainid0,public,usenet
X-Google-Language: ENGLISH,CP1252
Path: 
 g2news2.google.com!postnews.google.com!y11g2000yqm.googlegroups.com!not-for-mail
From: Phil Thornley <phil.jpthornley@gmail.com>
Newsgroups: comp.lang.ada
Subject: Re: Strategies with SPARK which does not support exceptions
Date: Fri, 18 Jun 2010 01:06:40 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <bb33c110-b0d6-4d7a-b8b0-ab03d91562f3@y11g2000yqm.googlegroups.com>
References: <op.vegat3qjule2fv@garhos>
NNTP-Posting-Host: 80.177.171.182
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1276848400 28302 127.0.0.1 (18 Jun 2010 08:06:40
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Fri, 18 Jun 2010 08:06:40 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: y11g2000yqm.googlegroups.com; posting-host=80.177.171.182;
	posting-account=Fz1-yAoAAACc1SDCr-Py2qBj8xQ-qC2q
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/4.0 (compatible; MSIE 8.0; Windows NT 6.1; WOW64;
	Trident/4.0; SLCC2; .NET CLR 2.0.50727; .NET CLR 3.5.30729; .NET CLR
	3.0.30729; Media Center PC 6.0),gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:12783
Date: 2010-06-18T01:06:40-07:00
List-Id: <comp.lang.ada>

On 17 June, 16:33, Yannick Duch=EAne (Hibou57)
<yannick_duch...@yahoo.fr> wrote:
> Hello,
>
> (This topic will probably not be the most exiting topic to some people).
>
> When I use SPARK, or even when I don't use SPARK while I still have SPARK=
 =A0
> design style in mind (even with Pascal which I still use), I have like an=
y =A0
> one else, to forget about exceptions.
>
> The only one thing which seems simple and clean enough I could figure, is=
 =A0
> to use a Boolean variable, named =93OK=94, and a sequence of =93if OK the=
n=94 =A0
> statements. That is, execution of one sequence of statements, which set O=
K =A0
> to False is something goes wrong, and execute clean-up statements by the =
=A0
> way. Then a next sequence of statements wrapped in a =93if OK then=94 whi=
ch do =A0
> the same, and so on with next statements groups which are also wrapped in=
 =A0
> a =93if OK then=94 (as many as needed).
>
> Although this seems clean and maintainable enough to me so far, I was =A0
> still wondering how other people deal with this (and may be by the way, I=
 =A0
> may have comment about why my way could be bad in some way).
>
> Note: a similar strategy may also obviously applies to fulfill the =93onl=
y =A0
> one single exit point=94 requirement.
>
> So, let us talk and comment about design strategies in this area (if =A0
> someones wish to).

(Perhaps not an entirely serious suggestion, but...)
The only way of interrupting a code sequence in SPARK is the exit
statement for a loop, so one possibility might be to create a 'single
pass' loop with an unconditional exit at the end.

Unfortunately such an unconditional exit is illegal, so you have to
use 'exit when True;'

Also there may be flow errors for some or all of the 'exit when'
statements (if the OK values only depend on the program inputs) - but
here we can put an accept statement - which will usefully document
that the loop is a not a real loop.

--# accept F, 40, "This is a single pass loop.";
OK :=3D True;
loop
   Some complicated code that might set OK;
   exit when not OK;
   Some more complicated code that might set OK;
   exit when not OK;
   Some more code;
   exit when True;
end loop;

:-)

Cheers,

Phil