Re: Strategies with SPARK which does not support exceptions

[Phil Clayton <phil.clayton@lineone.net>]

On Jun 18, 9:06 am, 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 := 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;

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