Re: Problems with SPARK 2015 and XMLAda

[Bob Duff <bobduff@theworld.com>]

"G.B." <bauhaus@futureapps.invalid> writes:

> Design by Contract™, which wasn't defined by your or me, has
> the "retry" facility as part of the "rescue"(*); ...

Eiffel is a pretty good language design, but "retry" is probably my
least favorite feature of that language.  It's just a disguised "goto".
I'm not 100% opposed to goto's in all cases, but they should normally be
avoided, and this is the worst kind of goto -- a goto that jumps
backward, thus forming a loop.

Meyer's examples have kludgy flags to indicate "how did I get here?"
As in "If I got here from the exception handler, then do the exceptional
case, else do the normal case".  He even has examples where there's a
counter of the number of times the exception handler was entered.
Yuck.

And the disguised goto is worse than a goto, because there's no label
saying "beware!, somebody jumps here from elsewhere!".

In Ada syntax, this seems clear enough:

procedure P (...) is
begin
   Do_Something;
exception
   when Some_Error =>
      Do_Something_Else;
end P;

But Meyer prefers this:

procedure P (...) is
   Flag : Boolean := False;
begin
   <<Retry>>
   if Flag then
      Do_Something_Else;
   else
      Do_Something;
   end if;
exception
   when Some_Error =>
      Flag := True;
      goto Retry; -- Illegal in Ada, for good reason!
end P;

Except the label is implicit in Eiffel, and the "goto Retry" is just
"retry".  (Oh, and the initialization to False is also implicit in
Eiffel -- another bad design decision, but unrelated to "retry".)

His complaint about the first version of P is that Do_Something_Else
might violate contracts (because at that time, Ada didn't have any way
to express contracts).  But the second version of P has the same
problem, for the same reason (Ada didn't have any way to express
contracts).

It boils down to "Ada exception handlers might have bugs".  Well, yeah,
but any code might have bugs.  Moving the bugs from the handler to
the main body of code doesn't prevent bugs.

>...both, exceptions as
> assertion failures and exceptions as other failures are parts of
> the definitions surrounding DbC. But not in the way imagined
> here. I'm sure that this imagination of "design by contract" has
> somehow definitions of something quite reasonable. It would be
> nice, though, if the number of naming conflicts could be small.

- Bob