From: Yannick Duchêne (Hibou57) on
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
design style in mind (even with Pascal which I still use), I have like any
one else, to forget about exceptions.

The only one thing which seems simple and clean enough I could figure, is
to use a Boolean variable, named “OK”, and a sequence of “if OK then”
statements. That is, execution of one sequence of statements, which set OK
to False is something goes wrong, and execute clean-up statements by the
way. Then a next sequence of statements wrapped in a “if OK then” which do
the same, and so on with next statements groups which are also wrapped in
a “if OK then” (as many as needed).

Although this seems clean and maintainable enough to me so far, I was
still wondering how other people deal with this (and may be by the way, I
may have comment about why my way could be bad in some way).

Note: a similar strategy may also obviously applies to fulfill the “only
one single exit point” requirement.

So, let us talk and comment about design strategies in this area (if
someones wish to).
From: Warren on
=?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= expounded in
news:op.vegat3qjule2fv(a)garhos:

> When I use SPARK, or even when I don't use SPARK while I still have
> SPARK design style in mind (even with Pascal which I still use), I
> have like any one else, to forget about exceptions.
>
> The only one thing which seems simple and clean enough I could figure,
> is to use a Boolean variable, named "OK", and a sequence of "if
> OK then" statements. ...
>
> Although this seems clean and maintainable enough to me so far, I was
> still wondering how other people deal with this (and may be by the
> way, I may have comment about why my way could be bad in some way).

While I'm not a SPARK user, a similar issue exists when writing
C code (although you can implement an exception with longjmp()).

In C, the best approach seems to be to have a defined set of
error/status codes to return. Often the errno values (e.g. EINVAL)
are used. But you can define a better enum set dedicated to
your application's specific needs.

In Ada, you can vastly improve upon that using a "real" enumerated
type. You can then define as many enum types as you need for
each class of function/procedures.

I suggest this because the calling program usually needs to
know "why" the call failed.

It is often not sufficient to simply know that OK is false.
For example, wouldn't it be nice for the user to know that
the open failed because of permissions, instead of the file
not existing.

Warren
From: Yannick Duchêne (Hibou57) on
Le Thu, 17 Jun 2010 19:11:29 +0200, Warren <ve3wwg(a)gmail.com> a écrit:
> It is often not sufficient to simply know that OK is false.
> For example, wouldn't it be nice for the user to know that
> the open failed because of permissions, instead of the file
> not existing.
>
> Warren

Hillo Warren

I see what you mean (I like the C analogy for this, that is meaningful),
while I don't fully agree with this later point : an exception typically
do not holds such details. The exception says “If fails”, and don't say
why (or just sightly, via its ID). Don't confuse Ada exception mechanism
with other OO exception mechanisms, which comes with many and too much
(because unusable in real life) members to hold informations about the
exception occurence.

By the way, you are talking about propagated exceptions (as you talked
about callers). I did not already set up a strategy for this. The way I
was talking about just applies to exception raised and caught inside the
same subprogram. I suppose this way could be extended to propagated
exceptions, but I'm afraid of bloating doing so. I though about something
looking like “software register” (analogy with CPU status registers), but
I'm afraid this may not be safe (while luckily, SPARK can help a lot to
properly use global variables ;) ).

Have a nice day

--
There is even better than a pragma Assert: a SPARK --# check.
--# check C and WhoKnowWhat and YouKnowWho;
--# assert Ada;
-- i.e. forget about previous premises which leads to conclusion
-- and start with new conclusion as premise.
From: Pascal Obry on
Yannick,

> The only one thing which seems simple and clean enough I could figure,
> is to use a Boolean variable, named “OK”, and a sequence of “if OK then”
> statements. That is, execution of one sequence of statements, which set
> OK to False is something goes wrong, and execute clean-up statements by
> the way. Then a next sequence of statements wrapped in a “if OK then”
> which do the same, and so on with next statements groups which are also
> wrapped in a “if OK then” (as many as needed).

I don't understand. SPARK code cannot raise exception, so why should the
code deal with exceptional code????

There is no exception, so not error to check... I don't see the point of
the Ok variable.

I'm probably missing something, can you clarify?

Pascal.
Hum, while writing this I see one case where this can be used... It
is if exceptions are used as control flow. To me this is just very
bad practice.

--

--|------------------------------------------------------
--| Pascal Obry Team-Ada Member
--| 45, rue Gabriel Peri - 78114 Magny Les Hameaux FRANCE
--|------------------------------------------------------
--| http://www.obry.net - http://v2p.fr.eu.org
--| "The best way to travel is by means of imagination"
--|
--| gpg --keyserver keys.gnupg.net --recv-key F949BD3B

From: Peter C. Chapin on
Pascal Obry wrote:

> There is no exception, so not error to check... I don't see the point of
> the Ok variable.
>
> I'm probably missing something, can you clarify?

I think what Yannick is talking about is something like this:

-- Full Ada:
procedure Complicated_Operation(X : in Some_Type);
-- Raises Operation_Failed if there is an error.

-- SPARK:
procedure Complicated_Operation(X : in Some_Type; Ok : out Boolean);
-- Writes True into 'Ok' if successful, otherwise False.

Now instead of having a nice exception handler you have to do things like

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

Of course this gets a bit ugly if you do lots of operations that might fail.

One thing I've done is something like this

--SPARK:
procedure Complicated_Operation(X : in Some_Type; Ok : in out Boolean);
-- Writes False into 'Ok' if failed; otherwise no change to 'Ok'.

Now I can do

Ok : Boolean := True;
....
Complicated_Operation(Argument_1, Ok);
Complicated_Operation(Argument_2, Ok);
Complicated_Operation(Argument_3, Ok);
if not Ok then
-- A failure occurred somewhere above.
end if;

Of course this only works if it's acceptable to continue the program after a
failure of one of the earlier operations. Obviously that's not always going
to be the case.

Peter