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.9 required=5.0 tests=BAYES_00 autolearn=ham
	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,ASCII
Path: 
 g2news2.google.com!postnews.google.com!x27g2000yqb.googlegroups.com!not-for-mail
From: Phil Clayton <phil.clayton@lineone.net>
Newsgroups: comp.lang.ada
Subject: Re: Strategies with SPARK which does not support exceptions
Date: Tue, 22 Jun 2010 10:01:30 -0700 (PDT)
Organization: http://groups.google.com
Message-ID: 
 <f4df32f6-909e-4fd2-b13f-7bfde1eb56d8@x27g2000yqb.googlegroups.com>
References: <op.vegat3qjule2fv@garhos>
 <bb33c110-b0d6-4d7a-b8b0-ab03d91562f3@y11g2000yqm.googlegroups.com>
NNTP-Posting-Host: 91.110.167.231
Mime-Version: 1.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
X-Trace: posting.google.com 1277226091 28456 127.0.0.1 (22 Jun 2010 17:01:31
 GMT)
X-Complaints-To: groups-abuse@google.com
NNTP-Posting-Date: Tue, 22 Jun 2010 17:01:31 +0000 (UTC)
Complaints-To: groups-abuse@google.com
Injection-Info: x27g2000yqb.googlegroups.com; posting-host=91.110.167.231;
	posting-account=v7gx3AoAAABfjb9m5b7l_Lt2KVEgQBIe
User-Agent: G2/1.0
X-HTTP-UserAgent: Mozilla/5.0 (X11; U; Linux i686; en-GB; rv:1.9.0.15)
	Gecko/2009102704 Fedora/3.0.15-1.fc10 Firefox/3.0.15,gzip(gfe)
Xref: g2news2.google.com comp.lang.ada:12839
Date: 2010-06-22T10:01:30-07:00
List-Id: <comp.lang.ada>

On Jun 18, 9:06=A0am, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
>
> (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
> =A0 =A0Some complicated code that might set OK;
> =A0 =A0exit when not OK;
> =A0 =A0Some more complicated code that might set OK;
> =A0 =A0exit when not OK;
> =A0 =A0Some more code;
> =A0 =A0exit when True;
> end loop;

Great example!

This got me wondering why SPARK doesn't allow return statements in a
subprogram body in the same way that unconditional exit statements are
allowed in a loop body because there seems to be very little
difference when your single-iteration loop is the entire subprogram
body.

Consider e.g.

begin
  loop
    ...
    if Cond then
      ...
      exit;
    end if;
    ...
    exit when True;
  end loop;
end ...;

then, surely, it is no worse to just return instead of using exit to
jump to the return point, e.g.

begin
  ...
  if Cond then
    ...
    return;
  end if;
  ...
end ...;

and there could be benefits.  This would give limited support for
multiple return points from a subprogram.  Whilst not giving the
flexibility of exceptions, Peter's example could at least be:

  Complicated_Operation(Argument, Success);
  if not Success then
    -- Deal with failure here.
    return;
  end if;
  -- Continue with the program here.

which avoids the potentially ugly nesting in the non-error case.

The reasons for a single return point at the end of a subprogram are
(according to John Barnes, yellow SPARK book, section 6.4) that it 1.
simplifies analysis and 2. makes it clearer for the reader because a
return statement can't be buried in the middle of the code.  I would
have thought that relaxing the rules on the return statement, as
described above, does not cause extra analysis or readability
problems, given existing support for the exit statement...?

Phil Clayton