Re: Help with Exceptions!

Re: Help with Exceptions!

[Robert Dewar]

Steve said

"Unfortunately perhaps, but you can't go back... the exception
terminates the current frame. The best that your exception
handler can do is recover from the error by resetting to some
default conditions, or re-raise the exception, as well as
possibly logging the error somehow."

Robert replies:

I don't think this is unfortunate at all. Replacement semantics for
exceptions are MUCH cleaner than continuation semntics. You can program
exactly what you want by narrowing the scope of the exception handler
to the desired degree of granularity -- e.g. if you want to resume at
the next statement, then put the handler round a single statement.

Help with Exceptions!

[Robert Gelb]

I am doing a homework assignment in ADA and I am confused by the
exceptions.  My question is this: when I catch an error with the
exception, how can I go back to statement where the error occured (or the
statement next to it)? 
I know in Visual Basic you can do a 'resume next' statement which returns
you to the statement next to the one where the error occured

VB:
sub test()
	dim x as integer
	on error goto ErrHandler
	x = 1000000	'error occurs here
	x = 3		'resume next returns the 	
			'execution here
	Exit sub			
ErrHandler:
resume next	'return execution
end sub

ADA:
procedure test is
	x:integer;
begin
	x:=10000000;
	x:=3;
exception
	when CONSTRAINT_ERROR=>
		put("Error");
		--how can I go back to 'x:=3' statement
end test;


--
Robert Gelb
Senior Systems Analyst
Data Express
Garden Grove, California USA
(714)895-8832

Re: Help with Exceptions!

[Vincent Smeets]

Robert Gelb wrote:
> 
> procedure test is
>         x:integer;
> begin
>         x:=10000000;
>         x:=3;
> exception
>         when CONSTRAINT_ERROR=>
>                 put("Error");
>                 --how can I go back to 'x:=3' statement
> end test;
> 

with Text_IO;
procedure Test is
   X : Integer;
begin
   begin
      X := 10000000;
   exception
     when Constraint_Error =>
        Text_IO.Put_Line ("Error");
   end;
   X := 3;
end Test;

--      Vincent Smeets              Competence Center Informatik GmbH
--      Tel. : +49-5931-805461      Postfach 1225
--      Fax  : +49-5931-842461      49702 Meppen, Germany
--      EMail: smeets@cci.de        http://www.cci.de/

Re: Help with Exceptions!

[Steve Howard]

Robert Gelb wrote:

> My question is this: when I catch an error with the
> exception, how can I go back to statement where the error occured (or the
> statement next to it)?

Unfortunately perhaps, but you can't go back... the exception 
terminates the current frame. The best that your exception 
handler can do is recover from the error by resetting to some 
default conditions, or re-raise the exception, as well as 
possibly logging the error somehow.

-- 
E. Steve Howard                | Lockheed Martin
                               | Ocean, Radar, & Sensor Systems        
mailto:howard@mtm.syr.ge.com   | Syracuse, NY

Re: Help with Exceptions!

[John Herro]

rgelb@csulb.edu (Robert Gelb) asks:
> ...when I catch an error with [an exception
> handler], how can I go back to statement
> where the error occured (or the statement
> next to it)?
     In Ada an exception handler is executed *instead of* the rest of the
procedure, function, block, etc. that raised the exception.  There's no
counterpart of Basic's RESUME or RESUME NEXT, and even a goto from an
exception handler back to the unit that raised the exception is forbidden!
 Therefore, place your exception handler in a small block, so that only a
small amount of code is skipped when the exception is raised, and place
the entire block in a loop that runs until the code executes correctly. 
For example, this program fragment will keep getting input until the user
types a valid integer; then it will go on:

Valid     : Boolean := False;
Input     : String(1 .. 80);
Input_Len : Integer;
Answer    : Integer;
...
while not Valid loop
   Put("Type an integer: ");
   Get_Line(Input, Input_Len);
   begin
      Answer := Integer'Value(Input(1 .. Input_Len));
      Valid  := True;
   exception
      when others => Put_Line("Invalid.  Please try again.");
   end;
end loop;

     Things are a bit more complicated for exceptions raised in a
*declarative* region, but most exceptions are raised in an executable
region.  There's a more detailed explanation of exceptions and exception
handlers in the Ada Tutor program, available for download at the Web and
ftp sites below my signature.
     I hope this helps.
- John Herro
Software Innovations Technology
http://members.aol.com/AdaTutor
ftp://members.aol.com/AdaTutor
     If a vegetarian is a person who eats vegetables, what does a
humanitarian eat?

Re: Help with Exceptions!

[Robert L. Spooner, AD3K]

In <4mqio5$a8b@news.sanders.lockheed.com>, John Cupak <jcupak@isd99.sanders.lockheed.com> writes:
>Well, I just *have* to put in my $0.02 worth....
>
>In some cases, you *do* want to re-execute the same statement. For example,
>if you query the user for a number, and you get something else: 
>
>function Response (Prompt : in String) return Integer is
>   Line : String(1..80);
>   Size : Natural;
>begin
>   Try_Again: loop
>      Error_Handler: begin
>         Put(Prompt);                         -- Ask user for input
>         Get_Line(Line,Size);                 -- Get user input
>         return Integer'Value(Line(1..Size)); -- Raise exception if bad input
>      exception
>          when others =>
>             Put_Line("""" & Line(1..Size) & """ is not a valid value.");
>             -- Stay in Try_Again loop
>      end Error_Handler;
>   end loop Try_Again;
>end Response;
>
>I trust my Ada83 code is correct, as I didn't compile it for this response.
>
>Hope this helps!

Another way to reexecute a statement is to have the function call itself from the 
exception handler, after outputting an error message.  Once the user enters valid 
input, the function willrecursively return with the proper value.  For user input 
from a keyboard, any performance differences between the loop and the recursive function 
call will be negligible.

function Response (Prompt : String) return integer is

   line : ...
   Size : ...

begin
   Put (Prompt);
   Get_Line (...;
   return ...
exception
   when others =>
      Put_Line (...;  -- error message
      return Response(Prompt);
end Response;

>-- 
>John J. Cupak, Jr., CCP     Internet       : jcupak@isd99.sanders.lockheed.com
>Lockheed Sanders, Inc.      Lockheed LAN   : jcupak@mailgw.sanders.lockheed.com
>95 Canal Street/MER15-2403  Lockheed DECNet: NHQVAX::CUPAK 
>Nashua, NH 03061-0868       Work Telephone : 603 885-2142 FAX: 603 885-1480
>

Bob

Robert L. Spooner             Applied Research Laboratory
(814) 863-4120                             PO Box 30
RLS19@PSUVM.PSU.EDU      State College, PA 16804-0030

Re: Help with Exceptions!

[tmoran]

>In some cases, you *do* want to re-execute the same statement. For example,
>if you query the user for a number, and you get something else:
  If the user still enters 'something else' after being asked for a number
17 times, it should be clear that the prompt is not sufficiently clear,
and one might expect the next input to be the user's foot through the
screen.  The recursive solution has the advantage over a loop that it
might give a storage_error or something beforehand, thus saving the cost
of a monitor.
  Or one could abandon the 're-execute the same statement' approach for:
for p in prompt'range loop
  begin
    Put(prompt(p));
    Get ...
    return;
  exception
    when data_error =>
      if p = prompt'last then raise User_Doesnt_Get_It;end if;
  end;
end loop;
with ever more explicit and simple prompts till you give up on the user.

Re: Help with Exceptions!

[George F.Rice]

Dave Jones wrote:

: procedure test is
:         x:integer ;
: begin
:         begin
:                 x := 10000000 ;
:         exception
:                 when CONSTRAINT_ERROR =>
:                         goto Next_Block ;
:         end ;
: <<Next_Block>>
:         begin
:                 x := 3 ;
:         exception
:                 when CONSTRAINT_ERROR =>
:                         RETURN ;
:         end ;
:         RETURN ;
: end test;

The goto is unnecessary; when the exception handler completes,
control will pass to the next statement anyway.

In general, the lack of a RESUME or RESUME NEXT could be considered
a feature rather than an omission.  Basic (my first language) doesn't
support structured exception handling like Ada or C++, an unfortunate 
omission on its part.

-- 
George

Quality means never having to use a sorry tool (tm)

Re: Help with Exceptions!

[Jon S Anthony]

In article <4mt0um$dgu@hearst.cac.psu.edu> RLS@psu.edu    (Robert L. Spooner, AD3K) writes:


> Another way to reexecute a statement is to have the function call
> itself from the exception handler, after outputting an error
> message.  Once the user enters valid input, the function
> willrecursively return with the proper value.  For user input from a
> keyboard, any performance differences between the loop and the
> recursive function call will be negligible.

This is a nice trick which allows you to approximate Eiffel style
exception capabilities.

> function Response (Prompt : String) return integer is
> 
>    line : ...
>    Size : ...
> 
> begin
>    Put (Prompt);
>    Get_Line (...;
>    return ...
> exception
>    when others =>
>       Put_Line (...;  -- error message
>       return Response(Prompt);
> end Response;


/Jon
-- 
Jon Anthony
Organon Motives, Inc.
1 Williston Road, Suite 4
Belmont, MA 02178

617.484.3383
jsa@organon.com

Re: Help with Exceptions!

[Robert A Duff]

In article <JSA.96May10151348@organon.com>,
Jon S Anthony <jsa@organon.com> wrote:
>This is a nice trick which allows you to approximate Eiffel style
>exception capabilities.

I don't like Eiffel's exception capabilities.  The "retry" feature is
just a loop implemented with a goto (i.e. "retry" is really a backward
goto).  I much prefer the Ada style, where you explicitly code a loop
statement, and put a block-statement-with-exception-handler inside that.

Eiffel has some nice features for asserting things about loops (loop
invariants, and loop variants -- the latter helps prove that the loop
terminates in a finite number of steps).  But the retry construct seems
to by-pass all that -- how does one prove that a retry will ever
terminate?

Of course, the example below is *intentionally* an infinite loop, which
is fine.  If the user never types the right answer, it loops forever (or
recurs forever, until stack is exhausted, unless the compiler is clever
enough to turn the tail recursion into a jump).  (Is it "recurs" or
"recurses"?.  ;-) )

Whether or not this is user-friendly is a different question.

>> function Response (Prompt : String) return integer is
>> 
>>    line : ...
>>    Size : ...
>> 
>> begin
>>    Put (Prompt);
>>    Get_Line (...;
>>    return ...
>> exception
>>    when others =>
>>       Put_Line (...;  -- error message
>>       return Response(Prompt);
>> end Response;

- Bob

Re: Help with Exceptions!

[Dave Jones]

George F.Rice wrote:
> 
> Dave Jones wrote:
> 
> : procedure test is
> :         x:integer ;
> : begin
> :         begin
> :                 x := 10000000 ;
> :         exception
> :                 when CONSTRAINT_ERROR =>
> :                         goto Next_Block ;
> :         end ;
> : <<Next_Block>>
> :         begin
> :                 x := 3 ;
> :         exception
> :                 when CONSTRAINT_ERROR =>
> :                         RETURN ;
> :         end ;
> :         RETURN ;
> : end test;
> 
> The goto is unnecessary; when the exception handler completes,
> control will pass to the next statement anyway.
> 
That's very true.  I was just trying to show what could be done
with regard to jumping out of a block where an exception has 
occured.  

In any case, like I said in my post, I don't recommed this way of 
approaching the problem.  In fact, I actually regret making
that post because, every time I have seen an Ada program with a 
"goto", I have always been able to find a better way to write the
program; so I suppose that I really should not be gently encouraging
people to use "goto".  

Most others seem to have an experience similar to mine:  "goto" means 
you need to change your approach.  So I was wondering, has anyone out
there ever encountered a situation where "goto" was actually necessary?

-- Dave Jones

Re: Help with Exceptions!

[Robert I. Eachus]

In article <319764DA.3A8C@io.com> Dave Jones <davedave@io.com> writes:

  > Most others seem to have an experience similar to mine: "goto"
  > means you need to change your approach.  So I was wondering, has
  > anyone out there ever encountered a situation where "goto" was
  > actually necessary?

   The only two cases in which I have used gotos in are:

   1) Testing the compiler's implementation of gotos for correctness.

   2) Implementation of table driven finite-state machines.

    The latter requires a bit of explanation.  Machine generated FSMs
can use lots of gotos, but I have never seen an Ada FSM generator
which does that. Implementing the entire FSM by hand with gotos is
heap bad juju.  But often you want a state table entry to have the
form (in pseudo-code):

    table-identifier table-type number-of-entries = 3
    when input = x goto state yyy
      "    "   = y goto state zzz
    when others => continue with state abc.

    This allows parse tables to be stored more compactly, and is best
implemented by having a loop over the table entries that contains a
goto back to the code for reading to table headers when the default
case is encountered.

    The code structure is:

    <<label>> ...
              for I in ... loop
                ...
                if entry_type = continue
                then
                  ...
                  goto label; 
                end if;
              end loop;

    Now those of you with academic backgrounds will cleverly realize
that this can be "fixed" with a recursive call. Those with compiler
experience will understand that I have seen parsers in states with
several hundred (often large) frames on the stack.  Doubling the
number of stack frames for stylistic reasons is very unappealing.

     Are there any other known cases where a goto "makes sense" in
Ada?  The only one I can come up with is for teaching gotos!
--

					Robert I. Eachus

with Standard_Disclaimer;
use  Standard_Disclaimer;
function Message (Text: in Clever_Ideas) return Better_Ideas is...

Re: Help with Exceptions!

[Michel Gauthier]

In article <EACHUS.96May13172506@spectre.mitre.org>,
eachus@spectre.mitre.org (Robert I. Eachus) wrote:

>>  In article <319764DA.3A8C@io.com> Dave Jones <davedave@io.com> writes:
>>  
>>    > Most others seem to have an experience similar to mine: "goto"
>>    > means you need to change your approach.  So I was wondering, has
>>    > anyone out there ever encountered a situation where "goto" was
>>    > actually necessary?
>>  
>>     The only two cases in which I have used gotos in are:
>>  
>>     1) Testing the compiler's implementation of gotos for correctness.
>>  
>>     2) Implementation of table driven finite-state machines.

In the mainlines, I agree. When the design (before any language implementation)
is a finite-state machine, a direct implementation of this design can be more
sensible than any workaround suitable only to fit a priori style rules.

Three useful comments :

 - implementing a finite-state machine with gotos requires accurate
documentation of the initial design,
 - blocks are a worthwhile feature to compile-check some bad uses,
and local variables are also a valid choice :
     <<State_1>> declare ... end ;
     <<State_2 >> declare ... end ;
     ...
 - a rule may not be applied if it is cheaper to convince the project
technical manager than to apply the rule.

>>      Now those of you with academic backgrounds will cleverly realize
>>  that this can be "fixed" with a recursive call. Those with compiler
>>  experience will understand that I have seen parsers in states with
>>  several hundred (often large) frames on the stack.  Doubling the
>>  number of stack frames for stylistic reasons is very unappealing.

It is difficult enough to teach recursivity, please do not add useless
complexity. I agree with your conclusion.

>>       Are there any other known cases where a goto "makes sense" in
>>  Ada?  The only one I can come up with is for teaching gotos!

The only two uses of gotos I have ever written in "structured" languages are :
 - implementing a report in a lexical parser in Pascal (a raise of later
languages),
 - coding the read of a date using reading a year, a month and a day. Every
internal read has four exits : read the next item (exit the current loop),
retry the current item (a normal loop), cancel the whole operation (raise)
and retry the whole operation (how to do without a goto or great complexity?).
But... this looks really like a finite-state machine.

ADVICE :
A good way to assess the use of gotos (and in fact of any kind of reports,
exceptions or any other), is to identify that the complexity arises from the
convergence of program flows. Exactly like loops require invariants, gotos,
program returns and report handling require an invariant, too (this is why 
Eiffel "retry" works well). Unfortunately, loop start has exactly two possible 
origins, whereas gotos and report handlers can have much more (especially 
for predefined exceptions) and that they are too often implicit. So, I
teach the 
rule : for a label, a program end or an exception handler, always establish a 
complete list of all gotos or raises and attach the corresponding assertion.

----------          ----------          ----------          ---------- 
Michel Gauthier / Laboratoire d'informatique
123 avenue Albert Thomas / F-87060 Limoges
telephone +33 () 55457335 [or ~ 7232]
fax +33 ()  55457315  [or ~7201]
----------          ----------          ----------          ----------
La grande equation de la fin du siecle : windows-X = Mac-Y
The main end-of-century equation : windows-X = Mac-Y
----------          ----------          ----------          ----------
Si l'an 2000 est pour vous un mysticisme stupide, utilisez la base 9
If you feel year 2000 a stupid mystic craze, use numeration base 9
----------          ----------          ----------          ----------

Re: Help with Exceptions!

[John Herro]

eachus@spectre.mitre.org (Robert I. Eachus) writes:
>    <<label>> ...
>              for I in ... loop
>                ...
>                if entry_type = continue
>                then
>                  ...
>                  goto label; 
>                end if;
>              end loop;
>... this could be "fixed" with a recursive call.
     I'm not saying that the following is any "better" than the above, but
here's how I would do it, without recursion.
Retry : Boolean := True;
I     : ...     := ...;
...
while Retry loop
   Retry := False;
   while I < ... and not Retry loop
      ...
      if entry_type = continue then
         ...
         Retry := True;
      end if;
      I := ...; -- e.g., I + 1 or ...'Succ(I)
   end loop;
end loop;
     Again, I'm not saying this is better, but my point is that you could
"fix" the goto without recursion.
- John Herro
Software Innovations Technology
http://members.aol.com/AdaTutor
ftp://members.aol.com/AdaTutor
     How many Americans does it take to change a light bulb?  Five.  One
to turn the bulb, and four to file an Environmental Impact Statement.

Re: Help with Exceptions!

[Robert A Duff]

In article <gauthier-1405960958270001@164.81.60.62>,
Michel Gauthier <gauthier@unilim.fr> wrote:
>...So, I
>teach the 
>rule : for a label, a program end or an exception handler, always establish a 
>complete list of all gotos or raises and attach the corresponding assertion.

This makes good sense for labels/goto's, but I don't think it is
reasonable for exception handlers.  The whole point of exception
handling is that the code detecting the error, and the code handling the
error are separated from each other, and need not know about each other.

- Bob

Re: Help with Exceptions!

[Theodore E. Dennison]

Robert I. Eachus wrote:
> 
> In article <319764DA.3A8C@io.com> Dave Jones <davedave@io.com> writes:
> 
>   > Most others seem to have an experience similar to mine: "goto"
>   > means you need to change your approach.  So I was wondering, has
>   > anyone out there ever encountered a situation where "goto" was
>   > actually necessary?
> 
>    The only two cases in which I have used gotos in are:
> 
>    1) Testing the compiler's implementation of gotos for correctness.
> 
>    2) Implementation of table driven finite-state machines.
> 
>     The latter requires a bit of explanation.  Machine generated FSMs
> can use lots of gotos, but I have never seen an Ada FSM generator
> which does that. Implementing the entire FSM by hand with gotos is
> heap bad juju.  But often you want a state table entry to have the

This question came up here about a year ago (inadvertantly raised by
myself), and kicked up quite a ---- storm. I think the general consensus
at the end was that there are situations where a FSM algorithm may 
be implemented more clearly with goto's that without. Personally, I'd 
rather write the unclear non-goto code. The Goto is one genie I'm not
about to release from the bottle.

However, I remember vividly the ferocity of Robert Dewar's arguments in 
favor of goto's for FSM's in compilers. Thus I'd be willing to wager
that if you look through GNAT's source code, you will find gotos. I
don't KNOW this, its just a (perhaps poorly) edjucated guess on my part.

-- 
T.E.D.          
                |  Work - mailto:dennison@escmail.orl.mmc.com  |
                |  Home - mailto:dennison@iag.net              |
                |  URL  - http://www.iag.net/~dennison         |

Re: Help with Exceptions!

[Robert A Duff]

In article <31987FF6.2781E494@escmail.orl.mmc.com>,
Theodore E. Dennison <dennison@escmail.orl.mmc.com> wrote:
>...Personally, I'd 
>rather write the unclear non-goto code. The Goto is one genie I'm not
>about to release from the bottle.

Interesting way to put it.  ;-)

>However, I remember vividly the ferocity of Robert Dewar's arguments in 
>favor of goto's for FSM's in compilers. Thus I'd be willing to wager
>that if you look through GNAT's source code, you will find gotos. I
>don't KNOW this, its just a (perhaps poorly) edjucated guess on my part.

I count 56 goto statements in my copy of the gnat sources.  So, the
coders are obviously not goto-phobes, but they are obviously not
creating heaps of spaghetti out of gotos, either.  Of those, 31 are in
the parser, and 6 in the scanner.

- Bob

Re: Help with Exceptions!

[Robert I. Eachus]

In article <4n9uas$pq0@newsbf02.news.aol.com> johnherro@aol.com (John Herro) writes:

  >	I'm not saying that the following is any "better" than the above, but
  > here's how I would do it, without recursion.

  > Retry : Boolean := True;
  > I     : ...     := ...;
  > ...
  > while Retry loop
  >    Retry := False;
  >    while I < ... and not Retry loop
  >	 ...
  >	 if entry_type = continue then
  >	    ...
  >	    Retry := True;
  >	 end if;
  >	 I := ...; -- e.g., I + 1 or ...'Succ(I)
  >    end loop;
  > end loop;
  >	Again, I'm not saying this is better, but my point is that you could
  > "fix" the goto without recursion.

   Your implication is correct, this is a lot worse. ;-) "Fixing" the
flow with state variables either requires at least second loop, two
state variables, multiple settings of the state variable or
duplication of the code for reading the table header.  (In this two
loop variation, you can go back to a for loop for the inner loop since
the continue entry occurs last--if you use are willing to use a loop
exit or return statement to get out in the "normal" case. Otherwise
you need a second state variable.) All of these are abortions that I
wouldn't put in any code I wrote in preference to a single goto and
label.  Not only do the alternatives obfuscate the actual logic, but
some create unexecutable paths through the code that require a lot of
reasoning to verify.  The recursive solution is slightly messy because
you often need four or five parameters in a real parser, but at least
the logic is clean.

--

					Robert I. Eachus

with Standard_Disclaimer;
use  Standard_Disclaimer;
function Message (Text: in Clever_Ideas) return Better_Ideas is...

Re: Help with Exceptions!

[Michel Gauthier]

In article <DrEB77.Kwu@world.std.com>, bobduff@world.std.com (Robert A
Duff) wrote:

>>  In article <gauthier-1405960958270001@164.81.60.62>,
>>  Michel Gauthier <gauthier@unilim.fr> wrote:
>>  >...So, I teach the 
>>  >rule : for a label, a program end or an exception handler, always
establish a 
>>  >complete list of all gotos or raises and attach the corresponding
assertion.
>>  
>>  This makes good sense for labels/goto's, but I don't think it is
>>  reasonable for exception handlers.  The whole point of exception
>>  handling is that the code detecting the error, and the code handling the
>>  error are separated from each other, and need not know about each other.

May I insist ?

From an assertion/proof point of view, sequential flow is really straightforward
(although in reverse direction...), conditional statements are simple (wichever
the number of branches), and "while" or "for" loops are manageable via the
preliminary design of invariants. This relates to the old "structured"
programming, which was assessed to be correct but insufficient.

For languages younger than Pascal, for "modular" or "object" programming,
hence for Ada (both -83 and -95), other features require understanding their
actual status according to assertions and proofs. The concern is for
program returns, loop exits, exception raises (widely used features) and
gotos, if any. 

Until now, I guess we can agree.

What I add is that there is nothing difficult in returning, exiting, raising or
going to. The programmer knows the assertion at the place of this
statement. Moreover, the statement is likely to be inside a conditional,
and there is a rich information, obtained as a logical conjunct, attached 
to this location of the program.
     What is difficult is bringing program flows together. This is always a 
disjunct, and the information is weakened, except for only one flow
(example : GETting and handling Data_Error). It is therefore really difficult
to manage multiple arrivals, and the point to be considereed with great
attention is the convergence point : the end of the subprogram, the
statement following the loop, the exception handler, the label.
    In many cases, there is only one arrival, and mastering the case is simple.
The maximum price to be paid is adding an assertion.
    When there are many arrivals on to the location, you CANNOT decide
what to do if you do not know the state of the program. How can you
build this knowledge if you have not establish the complete list of all 
arrivals prior to any other task ?

If you wish more detailed complements about these (heretic ?) ideas,
they have already been discussed in my book "Ada, a professional course"
(Macmillan, 1993) and in a dissertation (unfortunately in French) that
you can anonymously ftp from "ftp.unilim.fr" in the directory
/pub/labo_informatique/genie_logiciel/  (files hab_mg_*, essentially
part 2). These files are zipped postscript documents.

Obviously, you may also consider the assertion/proof point of view to be
a useless academic fashion. In this case, the above comments are of strictly
no interest for you. IMHO, it is a valid professional tool.

----------          ----------          ----------          ---------- 
Michel Gauthier / Laboratoire d'informatique
123 avenue Albert Thomas / F-87060 Limoges
telephone +33 () 55457335 [or ~ 7232]
fax +33 ()  55457315  [or ~7201]
----------          ----------          ----------          ----------
La grande equation de la fin du siecle : windows-X = Mac-Y
The main end-of-century equation : windows-X = Mac-Y
----------          ----------          ----------          ----------
Si l'an 2000 est pour vous un mysticisme stupide, utilisez la base 9
If you feel year 2000 a stupid mystic craze, use numeration base 9
----------          ----------          ----------          ----------

Re: Help with Exceptions!

[Norman H. Cohen]

In article <DrEB77.Kwu@world.std.com>, bobduff@world.std.com
(Robert A Duff) writes: 

|> In article <gauthier-1405960958270001@164.81.60.62>,
|> Michel Gauthier <gauthier@unilim.fr> wrote: 
|> >...So, I
|> >teach the
|> >rule : for a label, a program end or an exception handler, always establish a
|> >complete list of all gotos or raises and attach the corresponding assertion.
|>
|> This makes good sense for labels/goto's, but I don't think it is
|> reasonable for exception handlers.  The whole point of exception
|> handling is that the code detecting the error, and the code handling the
|> error are separated from each other, and need not know about each other.

A formal approach to a program with exception handlers is to establish a
postcondition for the block statement (or other frame) containing the
handlers.  One then proves that

(1) the postcondition is satisfied if the handled sequence of statements
    completes normally; and

(2) the postcondition is satisfied if the frame completes by invoking one
    of the handlers.

A naive view is that proving (2) entails proving, for each statement in
the handled sequence of statements, that if that statement raises some
exception handled in the frame, then the execution of the handled
sequence of statements up to that point, followed by execution of the
handler for that exception, establishes the precondition.  In fact,
because of RM 11.6, such an intricate approach is futile:  Just because
some subexpression within a statement can raise an exception does not
mean that all the preceding statements have been executed when it does
so!  One can prove very little about the state of the computation at the
moment an exception arises.

Because of RM 11.6, one should not write handlers that depend too heavily
on the state of the computation when the handler is entered.  Taken to
its extreme, this principle means that a handler should be written so
that it is possible to prove that it establishes the required
postcondition >>>regardless of the state of the computation upon entry to
the handler<<<.

In fact, one need not be so extreme:  One can rely on the values of
variables upon entry to the handled sequence of statements if those
variables are never altered within the handled sequence.

--
Norman H. Cohen    ncohen@watson.ibm.com

Re: Help with Exceptions!

[Robert A Duff]

In article <4nd7cm$fnp@watnews1.watson.ibm.com>,
Norman H. Cohen <ncohen@watson.ibm.com> wrote:
>A formal approach to a program with exception handlers is to establish a
>postcondition for the block statement (or other frame) containing the
>handlers.  One then proves that
>
>(1) the postcondition is satisfied if the handled sequence of statements
>    completes normally; and
>
>(2) the postcondition is satisfied if the frame completes by invoking one
>    of the handlers.

Quite reasonable.  But Ada doesn't have any way to declare which
exceptions are raised by which subprograms.  I thought the earlier
poster was saying that one should "know about" all the raise statements,
which is what I was objecting to.  Viewing the exceptions potentially
raised by a subprogram as part of that subprogram's interface, would be
much more reasonable, IMHO.  But that's not simple -- consider a
subprogram that takes an access-to-subprogram as a parameter.  To reason
precisely, you would sometimes like to say that the first subprogram
raises whatever exceptions can be raised by its parameter (which is not
known until run time).  In any case, Ada doesn't have any way of saying
these things, other than with comments.

>A naive view is that proving (2) entails proving, for each statement in
>the handled sequence of statements, that if that statement raises some
>exception handled in the frame, then the execution of the handled
>sequence of statements up to that point, followed by execution of the
>handler for that exception, establishes the precondition.  In fact,
>because of RM 11.6, such an intricate approach is futile:  ...

In the case of predefined exceptions, this is quite true.  But 11.6 does
not apply to user-defined exceptions, so you can reason about them much
more precisely.

>...Just because
>some subexpression within a statement can raise an exception does not
>mean that all the preceding statements have been executed when it does
>so!  One can prove very little about the state of the computation at the
>moment an exception arises.
>
>Because of RM 11.6, one should not write handlers that depend too heavily
>on the state of the computation when the handler is entered.  Taken to
>its extreme, this principle means that a handler should be written so
>that it is possible to prove that it establishes the required
>postcondition >>>regardless of the state of the computation upon entry to
>the handler<<<.

Well, this makes exception handlers pretty useless, since you can't do
much of anything in a handler, that depends on much of anything.  That
is, if you have to prove that "True" implies the post-condition, then
the post-condition will necessarily be pretty weak.  And, in fact,
exception handlers for the predefined exceptions *are* pretty much
useless, given 11.6.  There are *some* things you can safely do, but
it's not easy to tell what.  (How many programmers even understand
11.6?!  Even language lawyers are confused by it.  I know *I* am.)
A simple rule of thumb is, "don't handle predefined exceptions".

User-defined exceptions are easier to deal with, but you need some way
of telling which exceptions can be raised by any subprogram.

A "clean-up" exception handler is also easier to deal with ("when others
=> Clean_Up; raise;").  Here's a case where you very well might be able
to prove that Clean_Up works, despite the fact that it's precondition is
"True".  And in this case, you don't need to prove anything about the
post-condition of the containing block.

>In fact, one need not be so extreme:  One can rely on the values of
>variables upon entry to the handled sequence of statements if those
>variables are never altered within the handled sequence.

Right.

- Bob

Re: Help with Exceptions!

[Jon S Anthony]

In article <DrGz6L.7LA@world.std.com> bobduff@world.std.com (Robert A Duff) writes:

> User-defined exceptions are easier to deal with, but you need some way
> of telling which exceptions can be raised by any subprogram.

One possible trick here would be to use Ada.Exceptions capabilities
and attach information about the raising subprogram and such so that
handlers could determine who,what,when,where,why sorts of things.
Or do you have something more stringent in mind?

/Jon
-- 
Jon Anthony
Organon Motives, Inc.
1 Williston Road, Suite 4
Belmont, MA 02178

617.484.3383
jsa@organon.com

Re: Help with Exceptions!

[Robert A Duff]

In article <JSA.96May16141119@organon.com>,
Jon S Anthony <jsa@organon.com> wrote:
>One possible trick here would be to use Ada.Exceptions capabilities
>and attach information about the raising subprogram and such so that
>handlers could determine who,what,when,where,why sorts of things.
>Or do you have something more stringent in mind?

I had compile-time knowledge in mind.  Knowledge that could be used to
prove useful things about the program without running it, rather than
useful stuff that the handler can do at run time.

- Bob

Re: Help with Exceptions!

[Jon S Anthony]

In article <Dr7J1p.18G@world.std.com> bobduff@world.std.com (Robert A Duff) writes:

> In article <JSA.96May10151348@organon.com>,
> Jon S Anthony <jsa@organon.com> wrote:
> >This is a nice trick which allows you to approximate Eiffel style
> >exception capabilities.
> 
> I don't like Eiffel's exception capabilities.  The "retry" feature is
> just a loop implemented with a goto (i.e. "retry" is really a backward
> goto).  I much prefer the Ada style, where you explicitly code a loop
> statement, and put a block-statement-with-exception-handler inside that.

Hmmm, just goes to show how people can differ.  I don't think that
Eiffel exception capabilities are as flexible as Ada's, but you can
make a reasonable argument that that is a "good thing".


> Eiffel has some nice features for asserting things about loops (loop
> invariants, and loop variants -- the latter helps prove that the loop
> terminates in a finite number of steps).  But the retry construct seems
> to by-pass all that -- how does one prove that a retry will ever
> terminate?

In general?  You can't.  It's not magic.

/Jon
-- 
Jon Anthony
Organon Motives, Inc.
1 Williston Road, Suite 4
Belmont, MA 02178

617.484.3383
jsa@organon.com