Prev: More Ada in Cryptography.
Next: What Ada can do for Cryptography.
From: Warren on 21 Jun 2010 09:31
=?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= expounded in
news:op.vegih2owule2fv(a)garhos:

> 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

> 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.

Agreed and I was not promoting exceptions per se (to start with,
they are clumsy in C (with longjmp) due to the need to intercept
and do your own "cleanup" (effectively destructors).

> 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.

Exceptions are ok for things that rarely occur, IMO. In Ada they
can be convenient, but it depends upon your application. For
example, a Not_Found exception is sufficient for my use, if I am
looking up a symbol table (map container in a wrapper) and it
does not exist. I realize that it can incur overhead, depending
upon build options. This works because the invoking program
already has the context info (it knows the symbol it tried to
look up).

> By the way, you are talking about propagated exceptions (as you talked
> about callers). I did not already set up a strategy for this.

Like I said above, I was not really considering exceptions.
But exceptions can be tricky if they unwind through several
layers. For example, in my current project, I usually need to
intercept them to make sure that certain reference counts are
properly unreferenced. This applies only to objects that do
not have a Finalize method.

...
> CPU status registers), but I'm afraid this may not be safe (while
> luckily, SPARK can help a lot to properly use global variables ;) ).

Does SPARK even permit exceptions? I'm too lazy to
look it up.

Warren
From: Alexandre K on 21 Jun 2010 10:10
> Does SPARK even permit exceptions? I'm too lazy to
> look it up.
>
> Warren

Hi Warren,
Spark doesn't permit exception.
The program that checks your code will complain about it. We can "use"
exception in a
package that is hidden for Spark (so not parsed by the Examiner), but
as it is hidden, we can't proove this body part.
It is the case when you need to call an existing program that is not a
Spark one (Ada.Text_IO ...).

Alex

From: Phil Clayton on 22 Jun 2010 13:01
On Jun 18, 9:06 am, Phil Thornley <phil.jpthorn...(a)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
From: Claude on 22 Jun 2010 19:14
On Jun 17, 8:33 am, Yannick Duchêne (Hibou57)
<yannick_duch...(a)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  
> design style in mind (even with Pascal which I still use), I have like any  
> one else, to forget about exceptions.

Exceptions are not the best way to process error. (i.e., Not just a
SPARK topic).

Who even remember having already tested the exception error handling
as the software behaviour alternative?
That is about falling within shortcuts, verifications and rescue
processing all about unpredictable/uncompleted states/operations/tasks
to not being left behind - (risks are about remaining inconsistencies
triggering blockages or instability).

Usually, large critical software applications shall process a
"Semantic Response", with "add error" or "add warning" annotation
methods and "is complete" or "is successful" checking operations. And
generally speaking, the goal is no much about to abort something, but
let it go and collect as many errors or warnings to trace the
vulnerabilities. Indeed, the functional behaviour would rely on
"semantic response" as a part of the system requirements, in terms of
fault tolerance: (Because, faults or failures happen, whether
internally or within interactions).

Semantic responses shall trigger a selective processing in case of
error or eventually a complementary processing in case of warning
only.

In such a case, better to use a formal language like Ada and testing
as a software development approach.


Claude Defour
From: Warren on 23 Jun 2010 12:22
Claude expounded in
news:93966134-a285-41c5-a7f6-8c59151718a7(a)k39g2000yqb.googlegroups.com:

> On Jun 17, 8:33�am, Yannick Duch�ne (Hibou57)
> <yannick_duch...(a)yahoo.fr> wrote:
...
>> design style in mind (even with Pascal which I still use), I have
>> like any one else, to forget about exceptions.
>
> Exceptions are not the best way to process error. (i.e., Not just a
> SPARK topic).

This is an area of "contraversy". So much disagreement
will be the norm here.

> Usually, large critical software applications shall process a
> "Semantic Response", with "add error" or "add warning" annotation
> methods and "is complete" or "is successful" checking operations.
> Claude Defour

This is certainly "one way" to check a "returned result". The
problem with this approach however is to make certain
you test _all_ possible return cases. This can be done in Ada
with strict use of enumerated types, provided that:

1) the case statement(s) don't use the "with other" clause,
allowing the compiler to warn you about missing cases.
2) the enumerated set isn't huge leading to obscurity, or
a tendency to use "case ... with other" clause.
3) the enumerated type is suitable (i.e. isn't overloaded thru
re-use from other calls, providing other status cases that
don't apply to the current one).

I see two problems with this:

1) _may_ lead to many enumerated types
2) if not strictly followed, unhandled cases are silently accepted.
3) when a problem is noticed (unhandled case), it is very difficult
to track it down (debugging time).

Exceptions have the advantage that:

1) they get reported and "noticed" _immediately_ when unhandled.
2) they usually report the origin of the problem in the code.

The downside of exceptions though, is that it requires
extensive testing to provoke them (or to prove they
don't occur). So in a life-critical application, there
may be the requirement that it not throw its hands in
the air and give up (per exception). On the other hand,
proceeding incorrectly may be equally disasterous.

So my point is that there are two valid approaches and
that "one size does not fit all".

Warren
First  |  Prev  |  Next  |  Last
Pages: 1 2 3 4 5
Prev: More Ada in Cryptography.
Next: What Ada can do for Cryptography.