Strategies with SPARK which does not support exceptions

Strategies with SPARK which does not support exceptions

[Yannick Duchêne (Hibou57)]

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

Re: Strategies with SPARK which does not support exceptions

[Warren]

=?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

Re: Strategies with SPARK which does not support exceptions

[Yannick Duchêne (Hibou57)]

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.

Re: Strategies with SPARK which does not support exceptions

[Pascal Obry]

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

Re: Strategies with SPARK which does not support exceptions

[Peter C. Chapin]

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

Re: Strategies with SPARK which does not support exceptions

[Claude]

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

Re: Strategies with SPARK which does not support exceptions

[Phil Thornley]

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

Re: Strategies with SPARK which does not support exceptions

[Martin]

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

Re: Strategies with SPARK which does not support exceptions

[mockturtle]

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.

Re: Strategies with SPARK which does not support exceptions

[Alexandre K]

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

Re: Strategies with SPARK which does not support exceptions

[Warren]

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

Re: Strategies with SPARK which does not support exceptions

[Alexandre K]

> 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

Re: Strategies with SPARK which does not support exceptions

[Phil Clayton]

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

Re: Strategies with SPARK which does not support exceptions

[Claude]

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

Re: Strategies with SPARK which does not support exceptions

[Warren]

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

Re: Strategies with SPARK which does not support exceptions

[Claude]

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

Re: Strategies with SPARK which does not support exceptions

[Warren]

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

Re: Strategies with SPARK which does not support exceptions

[Stephen Leake]

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

Re: Strategies with SPARK which does not support exceptions

[Randy Brukardt]

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

Re: Strategies with SPARK which does not support exceptions

[Georg Bauhaus]

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

Re: Strategies with SPARK which does not support exceptions

[Simon Wright]

"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!

Re: Strategies with SPARK which does not support exceptions

[stefan-lucks]

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