* Strategies with SPARK which does not support exceptions
@ 2010-06-17 15:33 Yannick Duchêne (Hibou57)
2010-06-17 17:11 ` Warren
` (4 more replies)
0 siblings, 5 replies; 22+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2010-06-17 15:33 UTC (permalink / raw)
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).
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-17 15:33 Strategies with SPARK which does not support exceptions Yannick Duchêne (Hibou57)
@ 2010-06-17 17:11 ` Warren
2010-06-17 18:19 ` Yannick Duchêne (Hibou57)
2010-06-17 19:54 ` Pascal Obry
` (3 subsequent siblings)
4 siblings, 1 reply; 22+ messages in thread
From: Warren @ 2010-06-17 17:11 UTC (permalink / raw)
=?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= expounded in
news:op.vegat3qjule2fv@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
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-17 17:11 ` Warren
@ 2010-06-17 18:19 ` Yannick Duchêne (Hibou57)
2010-06-21 13:31 ` Warren
0 siblings, 1 reply; 22+ messages in thread
From: Yannick Duchêne (Hibou57) @ 2010-06-17 18:19 UTC (permalink / raw)
Le Thu, 17 Jun 2010 19:11:29 +0200, Warren <ve3wwg@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.
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-17 15:33 Strategies with SPARK which does not support exceptions Yannick Duchêne (Hibou57)
2010-06-17 17:11 ` Warren
@ 2010-06-17 19:54 ` Pascal Obry
2010-06-17 22:47 ` Peter C. Chapin
2010-06-18 6:07 ` Claude
` (2 subsequent siblings)
4 siblings, 1 reply; 22+ messages in thread
From: Pascal Obry @ 2010-06-17 19:54 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-17 19:54 ` Pascal Obry
@ 2010-06-17 22:47 ` Peter C. Chapin
0 siblings, 0 replies; 22+ messages in thread
From: Peter C. Chapin @ 2010-06-17 22:47 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-17 15:33 Strategies with SPARK which does not support exceptions Yannick Duchêne (Hibou57)
2010-06-17 17:11 ` Warren
2010-06-17 19:54 ` Pascal Obry
@ 2010-06-18 6:07 ` Claude
2010-06-18 8:06 ` Phil Thornley
2010-06-22 23:14 ` Claude
4 siblings, 0 replies; 22+ messages in thread
From: Claude @ 2010-06-18 6:07 UTC (permalink / raw)
On Jun 17, 8:33 am, Yannick Duchêne (Hibou57)
<yannick_duch...@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.
>
> So, let us talk and comment about design strategies in this area (if
> someones wish to).
Hello Yannick
You are talking about Ada. Just add annotation and you get SPARK and
static analysis.
SPARK is about
- Data and information flow analysis annotations ensure that data
are used in the expected way.
- Proof of absence of run-time errors that can spare exception error
handling and defensive programming.
Just have a look on the Phil Torney web site (SparkSure) and download
his Proof of Absence of Run-Time Error tutorial
http://www.sparksure.com/resources/Proof_Annotations.zip
It worth to have a glance at it...
Claude
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-17 15:33 Strategies with SPARK which does not support exceptions Yannick Duchêne (Hibou57)
` (2 preceding siblings ...)
2010-06-18 6:07 ` Claude
@ 2010-06-18 8:06 ` Phil Thornley
2010-06-18 8:49 ` Martin
2010-06-22 17:01 ` Phil Clayton
2010-06-22 23:14 ` Claude
4 siblings, 2 replies; 22+ messages in thread
From: Phil Thornley @ 2010-06-18 8:06 UTC (permalink / raw)
On 17 June, 16:33, Yannick Duchêne (Hibou57)
<yannick_duch...@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.
>
> 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).
(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;
:-)
Cheers,
Phil
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-18 8:06 ` Phil Thornley
@ 2010-06-18 8:49 ` Martin
2010-06-18 17:16 ` mockturtle
2010-06-22 17:01 ` Phil Clayton
1 sibling, 1 reply; 22+ messages in thread
From: Martin @ 2010-06-18 8:49 UTC (permalink / raw)
On Jun 18, 9:06 am, Phil Thornley <phil.jpthorn...@gmail.com> wrote:
> On 17 June, 16:33, Yannick Duchêne (Hibou57)
>
>
>
> <yannick_duch...@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.
>
> > 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).
>
> (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;
>
> :-)
>
> Cheers,
>
> Phil
No there's a fancy 'goto'! :-)
-- Martin
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-18 8:49 ` Martin
@ 2010-06-18 17:16 ` mockturtle
2010-06-18 21:51 ` Alexandre K
0 siblings, 1 reply; 22+ messages in thread
From: mockturtle @ 2010-06-18 17:16 UTC (permalink / raw)
On Jun 18, 10:49 am, Martin <martin.do...@btopenworld.com> wrote:
> (snip)
> > 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;
>
> > :-)
>
> > Cheers,
>
> > Phil
>
> No there's a fancy 'goto'! :-)
>
> -- Martin
Well, I do not know if 'goto's are allowed in SPARK, but that is the
solution that sometimes I use when I need to write code in the-
language-whose-name-is-a-single-letter :-). I know that it could
sound heretical, but this is one of the two cases where, I believe,
using goto is not so bad. I am thinking something like
procedure Very_Complex_Stuff (OK : out Boolean) is
begin
OK := True; -- Be optimistic :-)
Open_some_file (OK);
if not OK then
goto Exit_now;
end if;
Allocate_Some_Memory (OK);
if not OK then
goto Undo_Open;
end if;
Contact_DB (OK);
if not OK then
goto Undo_Mem;
end if;
goto Exit_Now;
<<Undo_Mem>>
Deallocate_Memory;
<<Undo_Open>>
Close_File;
<<Exit_Now>>
end;
I agree that this will not win the prize for the best code ever, but
if you choose your labels with care it can turn out an acceptable
solution.
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-18 17:16 ` mockturtle
@ 2010-06-18 21:51 ` Alexandre K
0 siblings, 0 replies; 22+ messages in thread
From: Alexandre K @ 2010-06-18 21:51 UTC (permalink / raw)
> Well, I do not know if 'goto's are allowed in SPARK, but that is the
> solution that sometimes I use when I need to write code in the-
> language-whose-name-is-a-single-letter :-). I know that it could
> sound heretical, but this is one of the two cases where, I believe,
> using goto is not so bad. I am thinking something like
Hi everyone,
Well, Goto are, as exceptions, not allowed in Spark.
To answer to Yannick, the way to replace exception is to use Boolean,
or Enumerates in an "out" parameter.
It is the case when you need to use an Ada program that uses
exceptions, and you have to write
a package specification with Spark and hide the implementation in the
body. (--# hide).
The Spark_IO package is an example of hiding the use of Ada.Text_IO,
and of course File exception.
Also, I think we should not use exception to control the flow of the
program.
Alex.
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-17 18:19 ` Yannick Duchêne (Hibou57)
@ 2010-06-21 13:31 ` Warren
2010-06-21 14:10 ` Alexandre K
0 siblings, 1 reply; 22+ messages in thread
From: Warren @ 2010-06-21 13:31 UTC (permalink / raw)
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 2218 bytes --]
=?utf-8?Q?Yannick_Duch=C3=AAne_=28Hibou57?= =?utf-8?Q?=29?= expounded in
news:op.vegih2owule2fv@garhos:
> Le Thu, 17 Jun 2010 19:11:29 +0200, Warren <ve3wwg@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
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-21 13:31 ` Warren
@ 2010-06-21 14:10 ` Alexandre K
0 siblings, 0 replies; 22+ messages in thread
From: Alexandre K @ 2010-06-21 14:10 UTC (permalink / raw)
> 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
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-18 8:06 ` Phil Thornley
2010-06-18 8:49 ` Martin
@ 2010-06-22 17:01 ` Phil Clayton
1 sibling, 0 replies; 22+ messages in thread
From: Phil Clayton @ 2010-06-22 17:01 UTC (permalink / raw)
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
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-17 15:33 Strategies with SPARK which does not support exceptions Yannick Duchêne (Hibou57)
` (3 preceding siblings ...)
2010-06-18 8:06 ` Phil Thornley
@ 2010-06-22 23:14 ` Claude
2010-06-23 16:22 ` Warren
4 siblings, 1 reply; 22+ messages in thread
From: Claude @ 2010-06-22 23:14 UTC (permalink / raw)
On Jun 17, 8:33 am, Yannick Duchêne (Hibou57)
<yannick_duch...@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
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-22 23:14 ` Claude
@ 2010-06-23 16:22 ` Warren
2010-06-24 3:24 ` Claude
0 siblings, 1 reply; 22+ messages in thread
From: Warren @ 2010-06-23 16:22 UTC (permalink / raw)
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 2157 bytes --]
Claude expounded in
news:93966134-a285-41c5-a7f6-8c59151718a7@k39g2000yqb.googlegroups.com:
> On Jun 17, 8:33�am, Yannick Duch�ne (Hibou57)
> <yannick_duch...@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
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-23 16:22 ` Warren
@ 2010-06-24 3:24 ` Claude
2010-06-28 13:14 ` Warren
2010-06-29 20:05 ` Randy Brukardt
0 siblings, 2 replies; 22+ messages in thread
From: Claude @ 2010-06-24 3:24 UTC (permalink / raw)
On Jun 23, 9:22 am, Warren <ve3...@gmail.com> wrote:
Exceptions are not the best way to process error. (i.e., Not just a
SPARK topic).
> 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 disastrous.
>
> So my point is that there are two valid approaches and
> that "one size does not fit all".
>
> Warren
Warren, you got quite the point, proceeding incorrectly may be
disastrous.
But not equally, because when the exception handler doesn't proceed
correctly and gets another exception, what's going to happen next?
Getting a third exception in a row, and so on ...
Processing anything within an exception handler is not recommended.
(That can even requires extra procedures to correct state/data which
could become out of context/visibility).
Safety critical system won't like any exception...
That's one of the SPARK advantage, it can assess about the absence of
run-time errors.
But about operational hazards, that's another story (worst: the
semantic responses are used to be generic!)
Claude Defour
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-24 3:24 ` Claude
@ 2010-06-28 13:14 ` Warren
2010-06-29 8:39 ` Stephen Leake
2010-06-29 20:05 ` Randy Brukardt
1 sibling, 1 reply; 22+ messages in thread
From: Warren @ 2010-06-28 13:14 UTC (permalink / raw)
[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 2186 bytes --]
Claude expounded in news:d90f60dd-b74f-4eff-b9d8-803ebb64c9d2
@z8g2000yqz.googlegroups.com:
> On Jun 23, 9:22�am, Warren <ve3...@gmail.com> wrote:
> Exceptions are not the best way to process error. (i.e., Not just a
> SPARK topic).
Well, I still think this is debatable (for run of the mill
code). I haven't seen conclusive arguments for either side.
>> 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 disastrous.
>
> Warren, you got quite the point, proceeding incorrectly may be
> disastrous.
> But not equally, because when the exception handler doesn't proceed
> correctly and gets another exception, what's going to happen next?
I could counter that the non-exception code can continue
on blithely as if nothing went wrong. What then?
At some point, you just have to accept some level of code
responsibility (as a practical matter). With either
approach, you cannot entirely avoid disasters.
> Safety critical system won't like any exception...
> That's one of the SPARK advantage, it can assess about the absence of
> run-time errors.
> But about operational hazards, that's another story (worst: the
> semantic responses are used to be generic!)
>
> Claude Defour
I can see some definite advantage for "proving" that
a system works under all expected cases. But the
responsibility then just shifts to the proof testing,
making sure that you've covered all possible real life
conditions. The Arian disaster comes to mind. ;-)
But you're right in that if you can prove that all the
bases are covered, you are ahead of the game. You don't
have to worry that some unanticipated exception (and
possible mishandling) may occur.
So I suppose that I do agree with you, provided you
are rigourous in your proofs. But for run of the mill
stuff (that I work on), where that kind of testing is
not done, then exceptions are in my mind "good enough",
and perhaps even preferred.
Warren
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-28 13:14 ` Warren
@ 2010-06-29 8:39 ` Stephen Leake
0 siblings, 0 replies; 22+ messages in thread
From: Stephen Leake @ 2010-06-29 8:39 UTC (permalink / raw)
Warren <ve3wwg@gmail.com> writes:
> So I suppose that I do agree with you, provided you
> are rigourous in your proofs. But for run of the mill
> stuff (that I work on), where that kind of testing is
> not done, then exceptions are in my mind "good enough",
> and perhaps even preferred.
In an ideal world, SPARK could handle programs with exceptions, and we'd
have both proofs and localized well-designed exception handling.
--
-- Stephe
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-24 3:24 ` Claude
2010-06-28 13:14 ` Warren
@ 2010-06-29 20:05 ` Randy Brukardt
2010-06-29 20:49 ` Georg Bauhaus
` (2 more replies)
1 sibling, 3 replies; 22+ messages in thread
From: Randy Brukardt @ 2010-06-29 20:05 UTC (permalink / raw)
"Claude" <claude.defour@orange.fr> wrote in message
news:d90f60dd-b74f-4eff-b9d8-803ebb64c9d2@z8g2000yqz.googlegroups.com...
>
>Exceptions are not the best way to process error. (i.e., Not just a
>SPARK topic).
There is an extra "not" in your statement. :-) You must have meant
"Exceptions are the best way to process error."
Result codes are dangerous, as ignoring of result codes is one of the major
problems in programming, and the resulting bugs are very, very hard to find.
(That's because of the difficulty of finding errors of omission.)
Perhaps you are too young to remember, but early versions of Windows (3.0,
3.1) had a reputation for being unstable and crashing often. But the
problems were mostly not with Windows but rather with programs that tended
to ignore the error returns from the Windows API. As such, they tended to
continue running but using non-existent Windows handles and the like. Given
the lack of memory protection on 16-bit computers, these errors tended to
take the entire Windows subsystem with them.
We developed a "middle-level" binding for programming Windows, which used
exceptions rather than error codes, and programs developed with it tended to
be much more stable than the commercial programs we were using at the
time --- probably because even when they failed, they didn't take the entire
OS with them (just popped up a message box and terminated properly).
I understand the problems with safety-critical systems and the need to test
to check exceptions, but I believe that the proper solution to those
problems is on the line of exception contracts and proving exception absence
when necessary to fufill those contracts. In particular, if a routine is
declared to not propagate Constraint_Error, then the routine is incorrect if
it in fact could propagate that exception. (I'm mildly annoyed that we
didn't have time in Ada 2012 to pursue those sorts of contracts seriously.)
There is no technical reason that tools like SPARK couldn't support
exceptions if they wanted to do so. Compiler optimizers are a form of proof
tool, and they have no problem dealing with exceptions. (That's because the
control flow caused by exceptions is quite limited, and is generally out of
blocks -- outbound flow has little effect on proofs within a block).
Returning to the dark ages of programming (that is BE - Before Exceptions)
and reintroducing all of the problems of early C code just because of
inadequate tools seems like a horrible step backwards to me.
This is exactly why I'm not much interested in SPARK itself: because it
forces programs back into the style that I originally learned for Fortran IV
in 1976: no dynamic allocation, no dynamic calls, no exceptions -- no
interest! I'm interested in what SPARK brings to the table in proof
capabilities, but I see no reason to give up 3/4rds of Ada to get it.
(Remember that Ada allocators, Ada O-O dispatching, Ada access-to-subprogram
calls, are all type-safe and provide plenty of opportunity for reasoning).
Randy Brukardt.
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-29 20:05 ` Randy Brukardt
@ 2010-06-29 20:49 ` Georg Bauhaus
2010-06-30 5:08 ` Simon Wright
2010-06-30 8:17 ` stefan-lucks
2 siblings, 0 replies; 22+ messages in thread
From: Georg Bauhaus @ 2010-06-29 20:49 UTC (permalink / raw)
On 6/29/10 10:05 PM, Randy Brukardt wrote:
> Result codes are dangerous, as ignoring of result codes is one of the major
> problems in programming, and the resulting bugs are very, very hard to find.
> (That's because of the difficulty of finding errors of omission.)
>
> Perhaps you are too young to remember, but early versions of Windows (3.0,
> 3.1) had a reputation for being unstable and crashing often. But the
> problems were mostly not with Windows but rather with programs that tended
> to ignore the error returns from the Windows API.
The result code situation in Windows 6.0 (Vista) seems even
worse today, even inside Windows OS software. The example is
this: When a file in NTFS is encrypted (green in explorer) and an
existing program tries to open it (not knowing that it might be
encrypted), the system returns "Access Denied". MS says that they
don't have the OS return a more descriptive code because they know that
many old programs will start failing and behave erratically:
the old programs are not prepared to handle return codes that did
not exist when the program was written.
I Learned this when trying to install driver files extracted from
a recent official ZIP archive by Linksys/Cisco, using Windows's own
driver installation program. The files had ended up encrypted in
the file system. Windows's standard installation stops with
"Access Denied" ...
Georg
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-29 20:05 ` Randy Brukardt
2010-06-29 20:49 ` Georg Bauhaus
@ 2010-06-30 5:08 ` Simon Wright
2010-06-30 8:17 ` stefan-lucks
2 siblings, 0 replies; 22+ messages in thread
From: Simon Wright @ 2010-06-30 5:08 UTC (permalink / raw)
"Randy Brukardt" <randy@rrsoftware.com> writes:
> This is exactly why I'm not much interested in SPARK itself: because
> it forces programs back into the style that I originally learned for
> Fortran IV in 1976: no dynamic allocation, no dynamic calls, no
> exceptions -- no interest! I'm interested in what SPARK brings to the
> table in proof capabilities, but I see no reason to give up 3/4rds of
> Ada to get it.
Complete agreement here!
^ permalink raw reply [flat|nested] 22+ messages in thread
* Re: Strategies with SPARK which does not support exceptions
2010-06-29 20:05 ` Randy Brukardt
2010-06-29 20:49 ` Georg Bauhaus
2010-06-30 5:08 ` Simon Wright
@ 2010-06-30 8:17 ` stefan-lucks
2 siblings, 0 replies; 22+ messages in thread
From: stefan-lucks @ 2010-06-30 8:17 UTC (permalink / raw)
On Tue, 29 Jun 2010, Randy Brukardt wrote:
> Returning to the dark ages of programming (that is BE - Before Exceptions)
> and reintroducing all of the problems of early C code just because of
> inadequate tools seems like a horrible step backwards to me.
I agree that error returns in code that isn't statically checked is a
first-class flight into the world of severe errors and bugs.
But for SPARK, if a subprogram can return an error code and you forget to
handle the error code, SPARK will remind you -- your program will not pass
the static verification. So the kind of errors introduced by error returns
can easily be avoided in SPARK.
So long
Stefan
--
------ Stefan Lucks -- Bauhaus-University Weimar -- Germany ------
Stefan dot Lucks at uni minus weimar dot de
------ I love the taste of Cryptanalysis in the morning! ------
^ permalink raw reply [flat|nested] 22+ messages in thread
end of thread, other threads:[~2010-06-30 8:17 UTC | newest]
Thread overview: 22+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2010-06-17 15:33 Strategies with SPARK which does not support exceptions Yannick Duchêne (Hibou57)
2010-06-17 17:11 ` Warren
2010-06-17 18:19 ` Yannick Duchêne (Hibou57)
2010-06-21 13:31 ` Warren
2010-06-21 14:10 ` Alexandre K
2010-06-17 19:54 ` Pascal Obry
2010-06-17 22:47 ` Peter C. Chapin
2010-06-18 6:07 ` Claude
2010-06-18 8:06 ` Phil Thornley
2010-06-18 8:49 ` Martin
2010-06-18 17:16 ` mockturtle
2010-06-18 21:51 ` Alexandre K
2010-06-22 17:01 ` Phil Clayton
2010-06-22 23:14 ` Claude
2010-06-23 16:22 ` Warren
2010-06-24 3:24 ` Claude
2010-06-28 13:14 ` Warren
2010-06-29 8:39 ` Stephen Leake
2010-06-29 20:05 ` Randy Brukardt
2010-06-29 20:49 ` Georg Bauhaus
2010-06-30 5:08 ` Simon Wright
2010-06-30 8:17 ` stefan-lucks
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox