comp.lang.ada
 help / color / mirror / Atom feed
* Exceptions and out procedure arguments (using GNAT GPL)
@ 2007-06-16  1:05 Fionn Mac Cumhaill
  2007-06-16  1:53 ` Anh Vo
                   ` (4 more replies)
  0 siblings, 5 replies; 31+ messages in thread
From: Fionn Mac Cumhaill @ 2007-06-16  1:05 UTC (permalink / raw)


Consider a procedure that starts like this:

procedure My_Procedure (
  O: out integer
)
is
begin

  -- various statements follow

  O := 999;

  -- more statements follow

  raise My_Exception;

I'm using GNAT GPL.

My question is:

Is the routine which calls My_Procedure guaranteed to get a value if
it does something like this?

X := 0;
My_Procedure(X);

and has an exception handler

exception
  when My_Exception =>
    null;

Will X get a value of 999? I.e., is an Ada compiler free to optimize
the code such that the assignment to the out variable O is moved to
some place after the point where the exception is raised?





^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-16  1:05 Exceptions and out procedure arguments (using GNAT GPL) Fionn Mac Cumhaill
@ 2007-06-16  1:53 ` Anh Vo
  2007-06-16  2:50 ` Brian May
                   ` (3 subsequent siblings)
  4 siblings, 0 replies; 31+ messages in thread
From: Anh Vo @ 2007-06-16  1:53 UTC (permalink / raw)


On Jun 15, 6:05 pm, Fionn Mac Cumhaill <invisi...@hiding.from.spam>
wrote:
> Consider a procedure that starts like this:
[...]
> Will X get a value of 999? I.e., is an Ada compiler free to optimize
> the code such that the assignment to the out variable O is moved to
> some place after the point where the exception is raised?

When an exception is raised, all bets are off. It is not guaranteed X
has a value of 999. However, the exception handler is allowed you to
do just that by setting X equal to 999 as shown below
...
exception
    when others =>
        X := 999;
...

AV




^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-16  1:05 Exceptions and out procedure arguments (using GNAT GPL) Fionn Mac Cumhaill
  2007-06-16  1:53 ` Anh Vo
@ 2007-06-16  2:50 ` Brian May
  2007-06-16  3:08 ` Randy Brukardt
                   ` (2 subsequent siblings)
  4 siblings, 0 replies; 31+ messages in thread
From: Brian May @ 2007-06-16  2:50 UTC (permalink / raw)


>>>>> "Fionn" == Fionn Mac Cumhaill <invisible@hiding.from.spam> writes:

    Fionn> Is the routine which calls My_Procedure guaranteed to get a
    Fionn> value if it does something like this?

I seem to remember the answer is no - when an exception occurs you
can't rely on anything returned via out or in out parameters.
-- 
Brian May <bam@snoopy.apana.org.au>



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-16  1:05 Exceptions and out procedure arguments (using GNAT GPL) Fionn Mac Cumhaill
  2007-06-16  1:53 ` Anh Vo
  2007-06-16  2:50 ` Brian May
@ 2007-06-16  3:08 ` Randy Brukardt
  2007-06-16  6:55 ` Dmitry A. Kazakov
  2007-06-18 15:44 ` Adam Beneschan
  4 siblings, 0 replies; 31+ messages in thread
From: Randy Brukardt @ 2007-06-16  3:08 UTC (permalink / raw)


"Fionn Mac Cumhaill" <invisible@hiding.from.spam> wrote in message
news:79c673pq5htg508nkoi935n3udqg5ps7r8@4ax.com...
...
> Will X get a value of 999? I.e., is an Ada compiler free to optimize
> the code such that the assignment to the out variable O is moved to
> some place after the point where the exception is raised?

My gut feeling (not one backed up by checking the rules in detail) is that
it depends on how the parameters are passed. Integers are a by-copy type, so
a compiler that modified X would be wrong: the copy back into X occurs on
the return from the call, and when the exception is raised that copy back
will not be executed.

Conversely, if the parameter is a by-reference type, then the assignment
should be reflected. (But I'd have to read the 11.6 rules ten times to be
sure, and it probably would depend on the actual code in the subprogram.)
Surely, Janus/Ada would make the assignment in that case.

If the language does not specify the parameter passing mechanism (as for
untagged records and arrays), then either thing could happen and you should
depend on nothing.

Surely the safest rule is to never depend on the parameter being changed,
but either thing can happen.

                           Randy.





^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-16  1:05 Exceptions and out procedure arguments (using GNAT GPL) Fionn Mac Cumhaill
                   ` (2 preceding siblings ...)
  2007-06-16  3:08 ` Randy Brukardt
@ 2007-06-16  6:55 ` Dmitry A. Kazakov
  2007-06-18 15:44 ` Adam Beneschan
  4 siblings, 0 replies; 31+ messages in thread
From: Dmitry A. Kazakov @ 2007-06-16  6:55 UTC (permalink / raw)


On Sat, 16 Jun 2007 01:05:10 GMT, Fionn Mac Cumhaill wrote:

> Consider a procedure that starts like this:
> 
> procedure My_Procedure (
>   O: out integer
> )
> is
> begin
> 
>   -- various statements follow
> 
>   O := 999;
> 
>   -- more statements follow
> 
>   raise My_Exception;

If you want to keep side effects on a parameter upon raising an exception,
then you should use access to Integer, because Integer is not a
by-reference type:

procedure My_Procedure (O: access integer) is
begin
   ...
   O.all := 999;
   ...
   raise My_Exception;

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-16  1:05 Exceptions and out procedure arguments (using GNAT GPL) Fionn Mac Cumhaill
                   ` (3 preceding siblings ...)
  2007-06-16  6:55 ` Dmitry A. Kazakov
@ 2007-06-18 15:44 ` Adam Beneschan
  2007-06-19  5:23   ` Fionn Mac Cumhaill
  4 siblings, 1 reply; 31+ messages in thread
From: Adam Beneschan @ 2007-06-18 15:44 UTC (permalink / raw)


On Jun 15, 6:05 pm, Fionn Mac Cumhaill <invisi...@hiding.from.spam>
wrote:
> Consider a procedure that starts like this:
>
> procedure My_Procedure (
>   O: out integer
> )
> is
> begin
>
>   -- various statements follow
>
>   O := 999;
>
>   -- more statements follow
>
>   raise My_Exception;
>
> I'm using GNAT GPL.
>
> My question is:
>
> Is the routine which calls My_Procedure guaranteed to get a value if
> it does something like this?
>
> X := 0;
> My_Procedure(X);
>
> and has an exception handler
>
> exception
>   when My_Exception =>
>     null;
>
> Will X get a value of 999?

No.  When My_Procedure completes abnormally, due to an exception
raise, X should have the value that it had before My_Procedure was
called.  An Ada compiler that causes X to be 999 here (if it wasn't
999 before) is incorrect.  This isn't a matter of "is the compiler
allowed to optimize" or "all bets are off" or "you can't rely on the
value"; rather, the semantics *require* that X be unchanged.  This is
because O is a by-copy parameter (6.2(3)), which means that inside the
subprogram, O denotes a *separate* object from X (6.2(2)), and O is
copied back to X only on *normal* completion of the subprogram
(6.4.1(17)), but an exception raise causes My_Procedure to be
completed abnormally (7.6.1(2)).

By-reference parameters work differently.  If, for example, your OUT
parameter were a tagged record, and you had assigned a component of it
to 999, it should still be 999 even after the exception in
My_Procedure is raised.  As I interpret the rules in 11.6, this might
not be the case if the exception raise is due to a language-defined
check; if, after you assign the component to 999, you do an array
access on a nonexistent element, so that Constraint_Error is raised,
this is a language-defined check, and now I think the compiler may be
allowed to optimize in a way so that the assignment of the component
to 999 might not take place.  But in your example, you have an
explicit raise of a user-defined exception, and 11.6 doesn't apply to
those, as I read it.  The same would apply in an access parameter
case; if My_Procedure is abandoned due to a raise of a user-defined
exception, you can count on any assignments that you've already done
through the access value, but you can't count on assignments done
before My_Procedure is abandoned due to a language-defined check.

Hope this helps,
                           -- Adam





^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-18 15:44 ` Adam Beneschan
@ 2007-06-19  5:23   ` Fionn Mac Cumhaill
  2007-06-19  7:34     ` Maciej Sobczak
  2007-06-19 21:40     ` Randy Brukardt
  0 siblings, 2 replies; 31+ messages in thread
From: Fionn Mac Cumhaill @ 2007-06-19  5:23 UTC (permalink / raw)


On Mon, 18 Jun 2007 08:44:57 -0700, Adam Beneschan <adam@irvine.com>
wrote:

>On Jun 15, 6:05 pm, Fionn Mac Cumhaill <invisi...@hiding.from.spam>
>wrote:
>> Consider a procedure that starts like this:
>>
>> procedure My_Procedure (
>>   O: out integer
>> )
>> is
>> begin
>>
>>   -- various statements follow
>>
>>   O := 999;
>>
>>   -- more statements follow
>>
>>   raise My_Exception;
>>
>> I'm using GNAT GPL.
>>
>> My question is:
>>
>> Is the routine which calls My_Procedure guaranteed to get a value if
>> it does something like this?
>>
>> X := 0;
>> My_Procedure(X);
>>
>> and has an exception handler
>>
>> exception
>>   when My_Exception =>
>>     null;
>>
>> Will X get a value of 999?
>
>No.  When My_Procedure completes abnormally, due to an exception
>raise, X should have the value that it had before My_Procedure was
>called.  An Ada compiler that causes X to be 999 here (if it wasn't
>999 before) is incorrect.  This isn't a matter of "is the compiler
>allowed to optimize" or "all bets are off" or "you can't rely on the
>value"; rather, the semantics *require* that X be unchanged.  This is
>because O is a by-copy parameter (6.2(3)), which means that inside the
>subprogram, O denotes a *separate* object from X (6.2(2)), and O is
>copied back to X only on *normal* completion of the subprogram
>(6.4.1(17)), but an exception raise causes My_Procedure to be
>completed abnormally (7.6.1(2)).
>
>By-reference parameters work differently.  If, for example, your OUT
>parameter were a tagged record, and you had assigned a component of it
>to 999, it should still be 999 even after the exception in
>My_Procedure is raised.  As I interpret the rules in 11.6, this might
>not be the case if the exception raise is due to a language-defined
>check; if, after you assign the component to 999, you do an array
>access on a nonexistent element, so that Constraint_Error is raised,
>this is a language-defined check, and now I think the compiler may be
>allowed to optimize in a way so that the assignment of the component
>to 999 might not take place.  But in your example, you have an
>explicit raise of a user-defined exception, and 11.6 doesn't apply to
>those, as I read it.  The same would apply in an access parameter
>case; if My_Procedure is abandoned due to a raise of a user-defined
>exception, you can count on any assignments that you've already done
>through the access value, but you can't count on assignments done
>before My_Procedure is abandoned due to a language-defined check.
>
>Hope this helps,
>                           -- Adam
>

It does indeed help, and convinces me that GNAT GPL 2007 has a bug.
The example I gave is a highly condensed version of a problem I had
while working on upgrading the MySQL binding in GNADE to work with
MySQL 5. I found after posting my first message that the situation is
even more confusing than I thought it was.
                            
Having (more or less) completed the work on the binding, I proceeded
to lay another package on top of it so that I could have something
that closely resembled the database package in GWindows. This would
greatly simplify the task of moving a lot of Windows software to
Linux.  The sample is a highly condensed version of my Query procedure
which raises an exception when a query sent to the MySQL database
server returns no rows. The O argument in my sample is actually a
handle whisch is used by other routines which extract data from the
columns in the returned row set.The routine that uses My_Procedure to
set the value of X is a procedure in the additional package. Let's
call it My_Outer_Procedure. I have two test programs that use a query
which returns no rows.

What I have found is, in effect, that whether X is 0 or 999 depends on
something in the routine that calls My_Outer_Procedure. I have two
test programs which use a query which  produces no rows, which means
that My_Procedure always raises an exception. In one of the test
programs, X is 0, and in the other it is 999, which makes no sense to
me.

I eliminated the problem by modifying the offending procedure to not
raise exceptions. It now returns a status code in an additional out
argument.






^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-19  5:23   ` Fionn Mac Cumhaill
@ 2007-06-19  7:34     ` Maciej Sobczak
  2007-06-19 15:21       ` Adam Beneschan
  2007-06-19 21:40     ` Randy Brukardt
  1 sibling, 1 reply; 31+ messages in thread
From: Maciej Sobczak @ 2007-06-19  7:34 UTC (permalink / raw)


On 19 Cze, 07:23, Fionn Mac Cumhaill <invisi...@hiding.from.spam>
wrote:

> I eliminated the problem by modifying the offending procedure to not
> raise exceptions. It now returns a status code in an additional out
> argument.

You might also introduce a temporary variable in the procedure to keep
the "candidate" result and copy it into the relevant out parameter
just before leaving the procedure (on the successful path).
This would be better than changing the interface and error handling
policy, which is very intrusive.

--
Maciej Sobczak
http://www.msobczak.com/




^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-19  7:34     ` Maciej Sobczak
@ 2007-06-19 15:21       ` Adam Beneschan
  2007-06-19 20:07         ` Dmitry A. Kazakov
  2007-06-20 15:15         ` Fionn Mac Cumhaill
  0 siblings, 2 replies; 31+ messages in thread
From: Adam Beneschan @ 2007-06-19 15:21 UTC (permalink / raw)


On Jun 19, 12:34 am, Maciej Sobczak <see.my.homep...@gmail.com> wrote:
> On 19 Cze, 07:23, Fionn Mac Cumhaill <invisi...@hiding.from.spam>
> wrote:
>
> > I eliminated the problem by modifying the offending procedure to not
> > raise exceptions. It now returns a status code in an additional out
> > argument.
>
> You might also introduce a temporary variable in the procedure to keep
> the "candidate" result and copy it into the relevant out parameter
> just before leaving the procedure (on the successful path).
> This would be better than changing the interface and error handling
> policy, which is very intrusive.

But it might be the correct design anyway.  My gut feeling is that, in
the abstract, a subprogram should either produce a result *or*
(perhaps) raise an exception, but not both; in general, if your
definition of a subprogram is that, under certain conditions, the
subprogram will raise an exception AND the caller can expect a certain
value to be returned (whether in an OUT parameter or an IN OUT or a
global or in something pointed to by an access parameter or whatever)
even though an exception is raised, the design is wrong.  It's better
to use an OUT status code of some sort in that case.  Sorry if I'm not
explaining this well---I don't always know what the common terminology
is for the things I'm thinking.  Also, I'm not saying that this
necessarily applies to Fionn's program.

                     -- Adam





^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-19 15:21       ` Adam Beneschan
@ 2007-06-19 20:07         ` Dmitry A. Kazakov
  2007-06-19 21:20           ` Adam Beneschan
  2007-06-20  6:21           ` Georg Bauhaus
  2007-06-20 15:15         ` Fionn Mac Cumhaill
  1 sibling, 2 replies; 31+ messages in thread
From: Dmitry A. Kazakov @ 2007-06-19 20:07 UTC (permalink / raw)


On Tue, 19 Jun 2007 08:21:26 -0700, Adam Beneschan wrote:

> My gut feeling is that, in
> the abstract, a subprogram should either produce a result *or*
> (perhaps) raise an exception, but not both; in general, if your
> definition of a subprogram is that, under certain conditions, the
> subprogram will raise an exception AND the caller can expect a certain
> value to be returned (whether in an OUT parameter or an IN OUT or a
> global or in something pointed to by an access parameter or whatever)
> even though an exception is raised, the design is wrong.  It's better
> to use an OUT status code of some sort in that case.

I don't think this is a good advice. In my view a right design assumes that
whether an exception is propagated or not, the subprogram should not leave
anything in an undefined state.

That is independent on the way an in-out parameter is passed. If the
parameter is by-reference, then the subprogram shall document all side
effects on it, which cannot be rolled back.

(Thee is a quite specific case of non-initialized out parameters, but I
don't like the idea of using that pattern rather than result anyway.)

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-19 20:07         ` Dmitry A. Kazakov
@ 2007-06-19 21:20           ` Adam Beneschan
  2007-06-20  6:16             ` Georg Bauhaus
  2007-06-20  8:01             ` Dmitry A. Kazakov
  2007-06-20  6:21           ` Georg Bauhaus
  1 sibling, 2 replies; 31+ messages in thread
From: Adam Beneschan @ 2007-06-19 21:20 UTC (permalink / raw)


On Jun 19, 1:07 pm, "Dmitry A. Kazakov" <mail...@dmitry-kazakov.de>
wrote:
> On Tue, 19 Jun 2007 08:21:26 -0700, Adam Beneschan wrote:
> > My gut feeling is that, in
> > the abstract, a subprogram should either produce a result *or*
> > (perhaps) raise an exception, but not both; in general, if your
> > definition of a subprogram is that, under certain conditions, the
> > subprogram will raise an exception AND the caller can expect a certain
> > value to be returned (whether in an OUT parameter or an IN OUT or a
> > global or in something pointed to by an access parameter or whatever)
> > even though an exception is raised, the design is wrong.  It's better
> > to use an OUT status code of some sort in that case.
>
> I don't think this is a good advice. In my view a right design assumes that
> whether an exception is propagated or not, the subprogram should not leave
> anything in an undefined state.

I think I agree with what you're saying, sort of.  Leaving things in
an undefined state (or worse, in an unusable state with dangling
pointer references or something like that) is bad.  The kind of thing
I'd object to is, say, a procedure that reads a string from a file
into an OUT parameter, and then raises an exception if the string
doesn't conform to some syntax.  Then, from the caller's point of
view, the procedure can *both* return valid (although inferior) output
*and* raise an exception, which I think would make things difficult to
understand for someone trying to read the code that calls the
procedure---I'd be scratching my head trying to figure out why, after
the caller has caught an exception in the procedure, is it still using
the value returned by the procedure?  That's a case where an
additional OUT parameter to say "this data is malformed" would be
better.  There's a subtle difference between saying "a procedure that
raises an exception shouldn't be counted on to produce valid output"
and "a procedure that raises an exception shouldn't leave undefined
random garbage lying around", but I realize that this is rather
difficult for me to express precisely.

                        -- Adam





^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-19  5:23   ` Fionn Mac Cumhaill
  2007-06-19  7:34     ` Maciej Sobczak
@ 2007-06-19 21:40     ` Randy Brukardt
  1 sibling, 0 replies; 31+ messages in thread
From: Randy Brukardt @ 2007-06-19 21:40 UTC (permalink / raw)


"Fionn Mac Cumhaill" <invisible@hiding.from.spam> wrote in message
news:drle731ukcmhlt5km966imoudr5s92napd@4ax.com...
...
> I eliminated the problem by modifying the offending procedure to not
> raise exceptions. It now returns a status code in an additional out
> argument.

My initial reaction to this was that it is like cutting off your foot
because your toe itches. ;-)

But I do have to agree with Adam that there is something wrong with the
design if you are expecting to get results back even if an exception is
raised. That does seem to be inappropriate use of an exception; it's not an
error at all if you expect results (it's just another normal case).

Still, in general result codes make me ill, so I would be at least as
concerned about a design that seems to be combining two operations (one to
return the initial results, and one to make the checks that lead to errors).

                         Randy.





^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-19 21:20           ` Adam Beneschan
@ 2007-06-20  6:16             ` Georg Bauhaus
  2007-06-20  8:01             ` Dmitry A. Kazakov
  1 sibling, 0 replies; 31+ messages in thread
From: Georg Bauhaus @ 2007-06-20  6:16 UTC (permalink / raw)


Adam Beneschan wrote:
>
> I'd object to is, say, a procedure that reads a string from a file
> into an OUT parameter, and then raises an exception if the string
> doesn't conform to some syntax.  Then, from the caller's point of
> view, the procedure can *both* return valid (although inferior) output
> *and* raise an exception, which I think would make things difficult to
> understand for someone trying to read the code that calls the
> procedure

The Design by Contract point of view :-)  I.e., you do not use assertions
(and hence exceptions) for handling invalid input; instead, you
use an if statement, or whatever seems equivalent.




-- Georg 



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-19 20:07         ` Dmitry A. Kazakov
  2007-06-19 21:20           ` Adam Beneschan
@ 2007-06-20  6:21           ` Georg Bauhaus
  2007-06-20  8:02             ` Dmitry A. Kazakov
  1 sibling, 1 reply; 31+ messages in thread
From: Georg Bauhaus @ 2007-06-20  6:21 UTC (permalink / raw)


Dmitry A. Kazakov wrote:
> On Tue, 19 Jun 2007 08:21:26 -0700, Adam Beneschan wrote:
> 
>> My gut feeling is that, in
>> the abstract, a subprogram should either produce a result *or*
>> (perhaps) raise an exception, but not both; in general, if your
>> definition of a subprogram is that, under certain conditions, the
>> subprogram will raise an exception AND the caller can expect a certain
>> value to be returned (whether in an OUT parameter or an IN OUT or a
>> global or in something pointed to by an access parameter or whatever)
>> even though an exception is raised, the design is wrong.  It's better
>> to use an OUT status code of some sort in that case.
> 
> I don't think this is a good advice. In my view a right design assumes that
> whether an exception is propagated or not, the subprogram should not leave
> anything in an undefined state.

Including unititialised in-variables? Partially initialised records?

And can you document all side effects on by reference (or global)
variables at all, in the presence of exceptions? In the general case?
(Considering this is Ada, which has exceptions, not SPARK, which is
about exceptional things not happening :-)




^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-19 21:20           ` Adam Beneschan
  2007-06-20  6:16             ` Georg Bauhaus
@ 2007-06-20  8:01             ` Dmitry A. Kazakov
  2007-06-20  8:45               ` Georg Bauhaus
  1 sibling, 1 reply; 31+ messages in thread
From: Dmitry A. Kazakov @ 2007-06-20  8:01 UTC (permalink / raw)


On Tue, 19 Jun 2007 14:20:56 -0700, Adam Beneschan wrote:

> The kind of thing
> I'd object to is, say, a procedure that reads a string from a file
> into an OUT parameter, and then raises an exception if the string
> doesn't conform to some syntax.  Then, from the caller's point of
> view, the procedure can *both* return valid (although inferior) output
> *and* raise an exception, which I think would make things difficult to
> understand for someone trying to read the code that calls the
> procedure---I'd be scratching my head trying to figure out why, after
> the caller has caught an exception in the procedure, is it still using
> the value returned by the procedure?  That's a case where an
> additional OUT parameter to say "this data is malformed" would be
> better.

Oh yes, this is a great example. No, I am using exceptions here. When
designing something like a recursive descent parser, I'm always use this
pattern:

   function Get (Source : Source_Type) return Thing;

when Get parses Thing (which can be as big as "package declarative region"
or "subprogram body" etc) it advances Source to the position following the
thing. When it fails, it propagates an exception and leaves Source in some
definite state, because the exception can potentially be handled to allow
compilation to continue and you cannot reasonably continue if you don't
know where you are. To use return codes for hundreds of Get's would be
extremely tedious and close to unreadable.

> There's a subtle difference between saying "a procedure that
> raises an exception shouldn't be counted on to produce valid output"
> and "a procedure that raises an exception shouldn't leave undefined
> random garbage lying around",

Yes

> but I realize that this is rather
> difficult for me to express precisely.

Actually I think that boils down to your stand point on exceptions vs.
program correctness. Mine is that any exception shall be a valid (correct)
outcome.

In other words, exceptions are a subject of DbC, they aren't a vehicle of.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-20  6:21           ` Georg Bauhaus
@ 2007-06-20  8:02             ` Dmitry A. Kazakov
  2007-06-20  8:46               ` Georg Bauhaus
  0 siblings, 1 reply; 31+ messages in thread
From: Dmitry A. Kazakov @ 2007-06-20  8:02 UTC (permalink / raw)


On Wed, 20 Jun 2007 08:21:16 +0200, Georg Bauhaus wrote:

> Dmitry A. Kazakov wrote:
>> On Tue, 19 Jun 2007 08:21:26 -0700, Adam Beneschan wrote:
>> 
>>> My gut feeling is that, in
>>> the abstract, a subprogram should either produce a result *or*
>>> (perhaps) raise an exception, but not both; in general, if your
>>> definition of a subprogram is that, under certain conditions, the
>>> subprogram will raise an exception AND the caller can expect a certain
>>> value to be returned (whether in an OUT parameter or an IN OUT or a
>>> global or in something pointed to by an access parameter or whatever)
>>> even though an exception is raised, the design is wrong.  It's better
>>> to use an OUT status code of some sort in that case.
>> 
>> I don't think this is a good advice. In my view a right design assumes that
>> whether an exception is propagated or not, the subprogram should not leave
>> anything in an undefined state.
> 
> Including unititialised in-variables? Partially initialised records?

OK, clearly this applies only to the things the subprogram is responsible
for.

> And can you document all side effects on by reference (or global)
> variables at all, in the presence of exceptions?

That depends on the meaning of "all." Certainly, we cannot control
side-effects on the CPU's cache or on the green gas emission caused by
consuming electricity during subprogram execution...

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-20  8:01             ` Dmitry A. Kazakov
@ 2007-06-20  8:45               ` Georg Bauhaus
  2007-06-20  9:29                 ` Dmitry A. Kazakov
  0 siblings, 1 reply; 31+ messages in thread
From: Georg Bauhaus @ 2007-06-20  8:45 UTC (permalink / raw)


On Wed, 2007-06-20 at 10:01 +0200, Dmitry A. Kazakov wrote:
> any exception shall be a valid (correct) outcome.

What will be the criteria for an outcome via exception
to be invalid (incorrect)? (Other than a trivial "not"?)





^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-20  8:02             ` Dmitry A. Kazakov
@ 2007-06-20  8:46               ` Georg Bauhaus
  2007-06-20  9:29                 ` Dmitry A. Kazakov
  0 siblings, 1 reply; 31+ messages in thread
From: Georg Bauhaus @ 2007-06-20  8:46 UTC (permalink / raw)


On Wed, 2007-06-20 at 10:02 +0200, Dmitry A. Kazakov wrote:
> On Wed, 20 Jun 2007 08:21:16 +0200, Georg Bauhaus wrote:

> > Including unititialised in-variables? Partially initialised records?
> 
> OK, clearly this applies only to the things the subprogram is responsible
> for.
> 
> > And can you document all side effects on by reference (or global)
> > variables at all, in the presence of exceptions?
> 
> That depends on the meaning of "all." Certainly, we cannot control
> side-effects on the CPU's cache or on the green gas emission caused by
> consuming electricity during subprogram execution...

Yes, no need repeating the absurd. So what is the meaning of "all
side effects"?





^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-20  8:46               ` Georg Bauhaus
@ 2007-06-20  9:29                 ` Dmitry A. Kazakov
  2007-06-20 10:13                   ` Georg Bauhaus
  0 siblings, 1 reply; 31+ messages in thread
From: Dmitry A. Kazakov @ 2007-06-20  9:29 UTC (permalink / raw)


On Wed, 20 Jun 2007 10:46:33 +0200, Georg Bauhaus wrote:

>>> And can you document all side effects on by reference (or global)
>>> variables at all, in the presence of exceptions?
>> 
>> That depends on the meaning of "all." Certainly, we cannot control
>> side-effects on the CPU's cache or on the green gas emission caused by
>> consuming electricity during subprogram execution...
> 
> Yes, no need repeating the absurd. So what is the meaning of "all
> side effects"?

Language-distinguishable sets of program states corresponding the
identified elements of the problem space.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-20  8:45               ` Georg Bauhaus
@ 2007-06-20  9:29                 ` Dmitry A. Kazakov
  0 siblings, 0 replies; 31+ messages in thread
From: Dmitry A. Kazakov @ 2007-06-20  9:29 UTC (permalink / raw)


On Wed, 20 Jun 2007 10:45:20 +0200, Georg Bauhaus wrote:

> On Wed, 2007-06-20 at 10:01 +0200, Dmitry A. Kazakov wrote:
>> any exception shall be a valid (correct) outcome.
> 
> What will be the criteria for an outcome via exception
> to be invalid (incorrect)? (Other than a trivial "not"?)

The criteria of correctness are same as for any flow control statement of
Ada.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-20  9:29                 ` Dmitry A. Kazakov
@ 2007-06-20 10:13                   ` Georg Bauhaus
  2007-06-20 12:58                     ` Dmitry A. Kazakov
  0 siblings, 1 reply; 31+ messages in thread
From: Georg Bauhaus @ 2007-06-20 10:13 UTC (permalink / raw)


On Wed, 2007-06-20 at 11:29 +0200, Dmitry A. Kazakov wrote:
> On Wed, 20 Jun 2007 10:46:33 +0200, Georg Bauhaus wrote:
> 
> >>> And can you document all side effects on by reference (or global)
> >>> variables at all, in the presence of exceptions?
> >> 
> >> That depends on the meaning of "all." Certainly, we cannot control
> >> side-effects on the CPU's cache or on the green gas emission caused by
> >> consuming electricity during subprogram execution...
> > 
> > Yes, no need repeating the absurd. So what is the meaning of "all
> > side effects"?
> 
> Language-distinguishable sets of program states corresponding the
> identified elements of the problem space.

Rephrasing the notion won't help defining it. :-) IIUC, your
(ambitious) goal is to write a correct program including
non-local goto. Whew, in which O(<?>) will this be?





^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-20 10:13                   ` Georg Bauhaus
@ 2007-06-20 12:58                     ` Dmitry A. Kazakov
  2007-06-20 14:16                       ` Georg Bauhaus
  0 siblings, 1 reply; 31+ messages in thread
From: Dmitry A. Kazakov @ 2007-06-20 12:58 UTC (permalink / raw)


On Wed, 20 Jun 2007 12:13:29 +0200, Georg Bauhaus wrote:

> On Wed, 2007-06-20 at 11:29 +0200, Dmitry A. Kazakov wrote:
>> On Wed, 20 Jun 2007 10:46:33 +0200, Georg Bauhaus wrote:
>> 
>>>>> And can you document all side effects on by reference (or global)
>>>>> variables at all, in the presence of exceptions?
>>>> 
>>>> That depends on the meaning of "all." Certainly, we cannot control
>>>> side-effects on the CPU's cache or on the green gas emission caused by
>>>> consuming electricity during subprogram execution...
>>> 
>>> Yes, no need repeating the absurd. So what is the meaning of "all
>>> side effects"?
>> 
>> Language-distinguishable sets of program states corresponding the
>> identified elements of the problem space.
> 
> Rephrasing the notion won't help defining it.

OK, give your definition of [side] effect of program execution so that we
could discuss your point.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-20 12:58                     ` Dmitry A. Kazakov
@ 2007-06-20 14:16                       ` Georg Bauhaus
  2007-06-20 18:22                         ` Dmitry A. Kazakov
  0 siblings, 1 reply; 31+ messages in thread
From: Georg Bauhaus @ 2007-06-20 14:16 UTC (permalink / raw)


On Wed, 2007-06-20 at 14:58 +0200, Dmitry A. Kazakov wrote:
> On Wed, 20 Jun 2007 12:13:29 +0200, Georg Bauhaus wrote:
> 
> > On Wed, 2007-06-20 at 11:29 +0200, Dmitry A. Kazakov wrote:
> >> On Wed, 20 Jun 2007 10:46:33 +0200, Georg Bauhaus wrote:
> >> 
> >>>>> And can you document all side effects on by reference (or global)
> >>>>> variables at all, in the presence of exceptions?
> >>>> 
> >>>> That depends on the meaning of "all." Certainly, we cannot control
> >>>> side-effects on the CPU's cache or on the green gas emission caused by
> >>>> consuming electricity during subprogram execution...
> >>> 
> >>> Yes, no need repeating the absurd. So what is the meaning of "all
> >>> side effects"?
> >> 
> >> Language-distinguishable sets of program states corresponding the
> >> identified elements of the problem space.
> > 
> > Rephrasing the notion won't help defining it.
> 
> OK, give your definition of [side] effect of program execution so that we
> could discuss your point.

A side effect of a subprogram P is a possible update of an object
(in some partition) that is not mentioned in P's parameter profile.





^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-19 15:21       ` Adam Beneschan
  2007-06-19 20:07         ` Dmitry A. Kazakov
@ 2007-06-20 15:15         ` Fionn Mac Cumhaill
  1 sibling, 0 replies; 31+ messages in thread
From: Fionn Mac Cumhaill @ 2007-06-20 15:15 UTC (permalink / raw)


On Tue, 19 Jun 2007 08:21:26 -0700, Adam Beneschan <adam@irvine.com>
wrote:

>On Jun 19, 12:34 am, Maciej Sobczak <see.my.homep...@gmail.com> wrote:
>> On 19 Cze, 07:23, Fionn Mac Cumhaill <invisi...@hiding.from.spam>
>> wrote:
>>
>> > I eliminated the problem by modifying the offending procedure to not
>> > raise exceptions. It now returns a status code in an additional out
>> > argument.
>>
>> You might also introduce a temporary variable in the procedure to keep
>> the "candidate" result and copy it into the relevant out parameter
>> just before leaving the procedure (on the successful path).
>> This would be better than changing the interface and error handling
>> policy, which is very intrusive.
>
>But it might be the correct design anyway.  My gut feeling is that, in
>the abstract, a subprogram should either produce a result *or*
>(perhaps) raise an exception, but not both; in general, if your
>definition of a subprogram is that, under certain conditions, the
>subprogram will raise an exception AND the caller can expect a certain
>value to be returned (whether in an OUT parameter or an IN OUT or a
>global or in something pointed to by an access parameter or whatever)
>even though an exception is raised, the design is wrong.  It's better
>to use an OUT status code of some sort in that case.  Sorry if I'm not
>explaining this well---I don't always know what the common terminology
>is for the things I'm thinking.  Also, I'm not saying that this
>necessarily applies to Fionn's program.
>
>                     -- Adam
>

The design needed to change in any case. The original Query was a
function, not a procedure. It returned a handle to storage allocated
to hold information about the result set returned by the query. That
storage was allocated before the query was made. If no rows were
returned, the exception was raised and the handle was lost. Given the
design of the package, it might well have been possible to retrieve
the handle, but that would have required producing a new function or
procedure to find it. It is best not to lose it.

With the design as I now have it, a loop to process looks like this
pseudocode:

Open a Query, return handle to result set

while rows remain, process rows

Close the query and deallocate storage designated by the handle.

This is the simple and obvious way to do it, and works as expected
even when the number of rows returned by the query is 0. It requires
minimal revision to the original code to achieve this goal.




^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-20 14:16                       ` Georg Bauhaus
@ 2007-06-20 18:22                         ` Dmitry A. Kazakov
  2007-06-20 19:16                           ` Georg Bauhaus
  0 siblings, 1 reply; 31+ messages in thread
From: Dmitry A. Kazakov @ 2007-06-20 18:22 UTC (permalink / raw)


On Wed, 20 Jun 2007 16:16:58 +0200, Georg Bauhaus wrote:

> On Wed, 2007-06-20 at 14:58 +0200, Dmitry A. Kazakov wrote:
>> On Wed, 20 Jun 2007 12:13:29 +0200, Georg Bauhaus wrote:
>> 
>>> On Wed, 2007-06-20 at 11:29 +0200, Dmitry A. Kazakov wrote:
>>>> On Wed, 20 Jun 2007 10:46:33 +0200, Georg Bauhaus wrote:
>>>> 
>>>>>>> And can you document all side effects on by reference (or global)
>>>>>>> variables at all, in the presence of exceptions?
>>>>>> 
>>>>>> That depends on the meaning of "all." Certainly, we cannot control
>>>>>> side-effects on the CPU's cache or on the green gas emission caused by
>>>>>> consuming electricity during subprogram execution...
>>>>> 
>>>>> Yes, no need repeating the absurd. So what is the meaning of "all
>>>>> side effects"?
>>>> 
>>>> Language-distinguishable sets of program states corresponding the
>>>> identified elements of the problem space.
>>> 
>>> Rephrasing the notion won't help defining it.
>> 
>> OK, give your definition of [side] effect of program execution so that we
>> could discuss your point.
> 
> A side effect of a subprogram P is a possible update of an object
> (in some partition) that is not mentioned in P's parameter profile.

1. What is "object"?
2. What is "update"?
3. Why this does not include "objects" mentioned in the parameter profile?
4. Which "updates" are you suggesting not to document?
6. When?
7. Why?

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-20 18:22                         ` Dmitry A. Kazakov
@ 2007-06-20 19:16                           ` Georg Bauhaus
  2007-06-20 20:40                             ` Dmitry A. Kazakov
  0 siblings, 1 reply; 31+ messages in thread
From: Georg Bauhaus @ 2007-06-20 19:16 UTC (permalink / raw)


Dmitry A. Kazakov wrote:
> On Wed, 20 Jun 2007 16:16:58 +0200, Georg Bauhaus wrote:
> 
>> On Wed, 2007-06-20 at 14:58 +0200, Dmitry A. Kazakov wrote:
>>> On Wed, 20 Jun 2007 12:13:29 +0200, Georg Bauhaus wrote:
>>>
>>>> On Wed, 2007-06-20 at 11:29 +0200, Dmitry A. Kazakov wrote:
>>>>> On Wed, 20 Jun 2007 10:46:33 +0200, Georg Bauhaus wrote:
>>>>>
>>>>>>>> And can you document all side effects on by reference (or global)
>>>>>>>> variables at all, in the presence of exceptions?
>>>>>>> That depends on the meaning of "all." Certainly, we cannot control
>>>>>>> side-effects on the CPU's cache or on the green gas emission caused by
>>>>>>> consuming electricity during subprogram execution...
>>>>>> Yes, no need repeating the absurd. So what is the meaning of "all
>>>>>> side effects"?
>>>>> Language-distinguishable sets of program states corresponding the
>>>>> identified elements of the problem space.
>>>> Rephrasing the notion won't help defining it.
>>> OK, give your definition of [side] effect of program execution so that we
>>> could discuss your point.
>> A side effect of a subprogram P is a possible update of an object
>> (in some partition) that is not mentioned in P's parameter profile.
> 
> 1. What is "object"?

Defined for Ada.

> 2. What is "update"?

Assignment.

> 3. Why this does not include "objects" mentioned in the parameter profile?

Because parameters and returns are better described by "effect of P",
not side effect of P. Reasoning/annotations/... will include them,
for sure. (cf. # global in SPARK.)

> 4. Which "updates" are you suggesting not to document?

I'm not suggesting to document or not to document.  I'm suggesting
that documenting all effects (wrt program state) of a subprogram,
including non-local goto is quite ambitious. Can the idea be made
more than a vague hint.


> 6. When?

In principle. Can we have a definition of a correct outcome of P
that includes exceptions raised by P, not handled by P, within the
Ada language framework?
If not, can you describe the extensions needed?


> 7. Why?

Because you said it would be possible, or at least that is what I had
understood. Is it possible, and if you say yes, then how would we
do this in Ada?



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-20 19:16                           ` Georg Bauhaus
@ 2007-06-20 20:40                             ` Dmitry A. Kazakov
  2007-06-21  9:52                               ` Georg Bauhaus
  0 siblings, 1 reply; 31+ messages in thread
From: Dmitry A. Kazakov @ 2007-06-20 20:40 UTC (permalink / raw)


On Wed, 20 Jun 2007 21:16:11 +0200, Georg Bauhaus wrote:

> Dmitry A. Kazakov wrote:
>> On Wed, 20 Jun 2007 16:16:58 +0200, Georg Bauhaus wrote:
>> 
>>> On Wed, 2007-06-20 at 14:58 +0200, Dmitry A. Kazakov wrote:
>>>> On Wed, 20 Jun 2007 12:13:29 +0200, Georg Bauhaus wrote:
>>>>
>>>>> On Wed, 2007-06-20 at 11:29 +0200, Dmitry A. Kazakov wrote:
>>>>>> On Wed, 20 Jun 2007 10:46:33 +0200, Georg Bauhaus wrote:
>>>>>>
>>>>>>>>> And can you document all side effects on by reference (or global)
>>>>>>>>> variables at all, in the presence of exceptions?
>>>>>>>> That depends on the meaning of "all." Certainly, we cannot control
>>>>>>>> side-effects on the CPU's cache or on the green gas emission caused by
>>>>>>>> consuming electricity during subprogram execution...
>>>>>>> Yes, no need repeating the absurd. So what is the meaning of "all
>>>>>>> side effects"?
>>>>>> Language-distinguishable sets of program states corresponding the
>>>>>> identified elements of the problem space.
>>>>> Rephrasing the notion won't help defining it.
>>>> OK, give your definition of [side] effect of program execution so that we
>>>> could discuss your point.
>>> A side effect of a subprogram P is a possible update of an object
>>> (in some partition) that is not mentioned in P's parameter profile.
>> 
>> 1. What is "object"?
> 
> Defined for Ada.

Aha, referencing to ARM is allowed! Then please take my definition back.
Observe, that ARM uses the word "effect" on many occasions, see ARM 1.1.5.
It does not limit it to either assignment or parameters. The documentation
of the effects titled in ARM as "dynamic semantics."

Is ARM nonsensical?

>> 2. What is "update"?
> 
> Assignment.

Of limited objects?

Is aborting a task an "update"? May integer overflow in Standard."+" abort
any tasks before leaving the current scope?

>> 3. Why this does not include "objects" mentioned in the parameter profile?
> 
> Because parameters and returns are better described by "effect of P",
> not side effect of P. Reasoning/annotations/... will include them,
> for sure. (cf. # global in SPARK.)

When an exception is propagated out of P, is "update" on an out parameter
of P an "effect"?

>> 4. Which "updates" are you suggesting not to document?
> 
> I'm not suggesting to document or not to document.  I'm suggesting
> that documenting all effects (wrt program state) of a subprogram,
> including non-local goto is quite ambitious.

I don't know how often you are using global variables, but if documenting
side effects looks ambitious, then you should probably review your
programming guidelines.

>> 6. When?
> 
> In principle. Can we have a definition of a correct outcome of P
> that includes exceptions raised by P, not handled by P, within the
> Ada language framework?

Yes. See any part of ARM which defines "dynamic semantics" of an operation.
For the operation ".all" the *only* correct outcome with the parameter null
is propagation Constraint_Error. Note that this also presumes no side
effects like:

   X := 4;
   Ptr := null;
   .. Ptr.all ...;  -- Surprise, this shall not change X!

Is it ambitious to require?

(Note also that "propagation" as used in ARM does not mean the "ultimate
effect of propagation.")

>> 7. Why?
> 
> Because you said it would be possible, or at least that is what I had
> understood. Is it possible, and if you say yes, then how would we
> do this in Ada?

In the same way ARM does it for operations on predefined types. For the
things which may have unpredictable side effects ARM uses the notion of
erroneous execution.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-20 20:40                             ` Dmitry A. Kazakov
@ 2007-06-21  9:52                               ` Georg Bauhaus
  2007-06-21 13:48                                 ` Dmitry A. Kazakov
  0 siblings, 1 reply; 31+ messages in thread
From: Georg Bauhaus @ 2007-06-21  9:52 UTC (permalink / raw)


On Wed, 2007-06-20 at 22:40 +0200, Dmitry A. Kazakov wrote:
> On Wed, 20 Jun 2007 21:16:11 +0200, Georg Bauhaus wrote:
> 
> > Dmitry A. Kazakov wrote:
> >> On Wed, 20 Jun 2007 16:16:58 +0200, Georg Bauhaus wrote:
> >> 
> >>> On Wed, 2007-06-20 at 14:58 +0200, Dmitry A. Kazakov wrote:
> >>>> On Wed, 20 Jun 2007 12:13:29 +0200, Georg Bauhaus wrote:
> >>>>
> >>>>> On Wed, 2007-06-20 at 11:29 +0200, Dmitry A. Kazakov wrote:
> >>>>>> On Wed, 20 Jun 2007 10:46:33 +0200, Georg Bauhaus wrote:
> >>>>>>
> >>>>>>>>> And can you document all side effects on by reference (or global)
> >>>>>>>>> variables at all, in the presence of exceptions?
> >>>>>>>> That depends on the meaning of "all." Certainly, we cannot control
> >>>>>>>> side-effects on the CPU's cache or on the green gas emission caused by
> >>>>>>>> consuming electricity during subprogram execution...
> >>>>>>> Yes, no need repeating the absurd. So what is the meaning of "all
> >>>>>>> side effects"?
> >>>>>> Language-distinguishable sets of program states corresponding the
> >>>>>> identified elements of the problem space.
> >>>>> Rephrasing the notion won't help defining it.
> >>>> OK, give your definition of [side] effect of program execution so that we
> >>>> could discuss your point.
> >>> A side effect of a subprogram P is a possible update of an object
> >>> (in some partition) that is not mentioned in P's parameter profile.

[I'm cutting out your questions because they give details
about the very things I'm kindly asking you to provide.
I'm curious about your exact formal, writable, specifications
so that programmers can write expressions detailed at a level
that is on a par with, say, parameter profiles, or assertions.]


> >> 4. Which "updates" are you suggesting not to document?
> > 
> > I'm not suggesting to document or not to document.  I'm suggesting
> > that documenting all effects (wrt program state) of a subprogram,
> > including non-local goto is quite ambitious.
> 
> I don't know how often you are using global variables, but if documenting
> side effects looks ambitious, then you should probably review your
> programming guidelines.

I'm not taking this as an argument when your offer is that
there exists a LRM that says "dynamic semantics". We cannot just
squeeze a copy of the LRM a bit and expect to have a formal apparatus
for expressing formal expectations in your *Different-from-DbC*
*states-plus-exceptions* approach (IIUC), together with a way to
mechanically checking our assumptions (which is part of why we
have high level programming languages, and compilers.)

>  See any part of ARM which defines "dynamic semantics" of an operation.

I think I fail to express myself clearly, as IMHO you talk evasively
around the real question: What is your formal documentation language,
with set-of-words = {program variables, pre/post/inv, ...} such that
a compiler/translator/analysis program can be used as a programmer's
aid in demonstrating correctness of a program.


> For the operation ".all" the *only* correct outcome with the parameter null
> is propagation Constraint_Error. Note that this also presumes no side
> effects like:
> 
>    X := 4;
>    Ptr := null;
>    .. Ptr.all ...;  -- Surprise, this shall not change X!
> 
> Is it ambitious to require?

Will it change Ptr.all?


>  For the
> things which may have unpredictable side effects ARM uses the notion of
> erroneous execution.

Is erroneous execution correct or incorrect, valid or invalid, and how
does this affect having exceptions a possible values of any type?





^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-21  9:52                               ` Georg Bauhaus
@ 2007-06-21 13:48                                 ` Dmitry A. Kazakov
  2007-06-22 18:15                                   ` Georg Bauhaus
  0 siblings, 1 reply; 31+ messages in thread
From: Dmitry A. Kazakov @ 2007-06-21 13:48 UTC (permalink / raw)


On Thu, 21 Jun 2007 11:52:09 +0200, Georg Bauhaus wrote:

> On Wed, 2007-06-20 at 22:40 +0200, Dmitry A. Kazakov wrote:

>> I don't know how often you are using global variables, but if documenting
>> side effects looks ambitious, then you should probably review your
>> programming guidelines.
> 
> I'm not taking this as an argument when your offer is that
> there exists a LRM that says "dynamic semantics". We cannot just
> squeeze a copy of the LRM a bit and expect to have a formal apparatus
> for expressing formal expectations in your *Different-from-DbC*
> *states-plus-exceptions* approach (IIUC),

In which way is it different?

I didn't talk about formal correctness or pre-/postconditions, but if you
bring this topic in. What is so difficult in:

require: ...
   ... Ptr.all ...
ensure: (Ptr=null and Propagated(Constraint_Error)) or ...

>>  See any part of ARM which defines "dynamic semantics" of an operation.
> 
> I think I fail to express myself clearly, as IMHO you talk evasively
> around the real question: What is your formal documentation language,
> with set-of-words = {program variables, pre/post/inv, ...} such that
> a compiler/translator/analysis program can be used as a programmer's
> aid in demonstrating correctness of a program.

Then I probably understood you wrong. What was your objection? A) to
documenting side effects in case of exception propagation, B) to proving
formal correctness of a program in the same case, C) to both?

A or B or C imply a total ban on any exceptions. Clearly, you need not
document anything that cannot happen...

>> For the operation ".all" the *only* correct outcome with the parameter null
>> is propagation Constraint_Error. Note that this also presumes no side
>> effects like:
>> 
>>    X := 4;
>>    Ptr := null;
>>    .. Ptr.all ...;  -- Surprise, this shall not change X!
>> 
>> Is it ambitious to require?
> 
> Will it change Ptr.all?

Yes, if the compiler is broken or else some erroneous execution is
underway.

> Is erroneous execution correct or incorrect, valid or invalid, and how
> does this affect having exceptions a possible values of any type?

This question is meaningless. Erroneous execution does not have this
property. You should specify a program, be it an application program or
then compiler. When the application program enters erroneous execution
where ARM allows this, then the compiler used to compile that program is
correct. When the specification of the application program allows erroneous
execution in the corresponding problem space states, then the program is
correct as well.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-21 13:48                                 ` Dmitry A. Kazakov
@ 2007-06-22 18:15                                   ` Georg Bauhaus
  2007-06-22 19:45                                     ` Dmitry A. Kazakov
  0 siblings, 1 reply; 31+ messages in thread
From: Georg Bauhaus @ 2007-06-22 18:15 UTC (permalink / raw)


Dmitry A. Kazakov wrote:
> 
> I didn't talk about formal correctness or pre-/postconditions, but if you
> bring this topic in. What is so difficult in:

I had this in mind:
"Actually I think that boils down to your [Adam Beneschan's] stand point
on exceptions vs. program correctness. Mine is that any exception shall
be a valid (correct) outcome.

"In other words, exceptions are a subject of DbC, they aren't a vehicle of. "

How, exactly, can exception be made a subject of DbC (other than
banning them)?



^ permalink raw reply	[flat|nested] 31+ messages in thread

* Re: Exceptions and out procedure arguments (using GNAT GPL)
  2007-06-22 18:15                                   ` Georg Bauhaus
@ 2007-06-22 19:45                                     ` Dmitry A. Kazakov
  0 siblings, 0 replies; 31+ messages in thread
From: Dmitry A. Kazakov @ 2007-06-22 19:45 UTC (permalink / raw)


On Fri, 22 Jun 2007 20:15:02 +0200, Georg Bauhaus wrote:

> Dmitry A. Kazakov wrote:
>> 
>> I didn't talk about formal correctness or pre-/postconditions, but if you
>> bring this topic in. What is so difficult in:
> 
> I had this in mind:
> "Actually I think that boils down to your [Adam Beneschan's] stand point
> on exceptions vs. program correctness. Mine is that any exception shall
> be a valid (correct) outcome.
> 
> "In other words, exceptions are a subject of DbC, they aren't a vehicle of. "
> 
> How, exactly, can exception be made a subject of DbC (other than
> banning them)?

By having contracted exceptions, obviously.

Heck, I am not an employee of Praxis, you know, so you'd better ask them. 
But if I were at their place, I would introduce the predicate 
propagated(e). For each e, exception, propagated(e) is true when e is being 
propagated. Trivially, each Ada statement has in its precondition

   forall e not propagated (e)

except for the first statement of an exception handler:

exception
   when Constraint_Error =>
       require propagated(Constraint_Error) and
            not (...other exceptions...);

For built-in operations like "+" we could have:

   function "+" (Left, Right : Integer) return Integer;
   ensure
      (Left + Right not in Integer'Range and propagated(Constraint_Error))
   or
      (Left + Right in Integer'Range and Result = Left + Right)

[and not propagated (Program_Error) and not propagated (Data_Error) ...)]

For raise:

   raise e;
   ensure propagated(e) [and not ...]

P.S. Robert Duff said on many occasions that Storage_Error could be 
propagated almost anywhere. That's better to change and he mentioned some 
ideas of how to do this. But Storage_Error is not a catastrophe for 
provability. Just don't mention it in the contracts, and *consequently* 
don't handle it because you could not.

-- 
Regards,
Dmitry A. Kazakov
http://www.dmitry-kazakov.de



^ permalink raw reply	[flat|nested] 31+ messages in thread

end of thread, other threads:[~2007-06-22 19:45 UTC | newest]

Thread overview: 31+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2007-06-16  1:05 Exceptions and out procedure arguments (using GNAT GPL) Fionn Mac Cumhaill
2007-06-16  1:53 ` Anh Vo
2007-06-16  2:50 ` Brian May
2007-06-16  3:08 ` Randy Brukardt
2007-06-16  6:55 ` Dmitry A. Kazakov
2007-06-18 15:44 ` Adam Beneschan
2007-06-19  5:23   ` Fionn Mac Cumhaill
2007-06-19  7:34     ` Maciej Sobczak
2007-06-19 15:21       ` Adam Beneschan
2007-06-19 20:07         ` Dmitry A. Kazakov
2007-06-19 21:20           ` Adam Beneschan
2007-06-20  6:16             ` Georg Bauhaus
2007-06-20  8:01             ` Dmitry A. Kazakov
2007-06-20  8:45               ` Georg Bauhaus
2007-06-20  9:29                 ` Dmitry A. Kazakov
2007-06-20  6:21           ` Georg Bauhaus
2007-06-20  8:02             ` Dmitry A. Kazakov
2007-06-20  8:46               ` Georg Bauhaus
2007-06-20  9:29                 ` Dmitry A. Kazakov
2007-06-20 10:13                   ` Georg Bauhaus
2007-06-20 12:58                     ` Dmitry A. Kazakov
2007-06-20 14:16                       ` Georg Bauhaus
2007-06-20 18:22                         ` Dmitry A. Kazakov
2007-06-20 19:16                           ` Georg Bauhaus
2007-06-20 20:40                             ` Dmitry A. Kazakov
2007-06-21  9:52                               ` Georg Bauhaus
2007-06-21 13:48                                 ` Dmitry A. Kazakov
2007-06-22 18:15                                   ` Georg Bauhaus
2007-06-22 19:45                                     ` Dmitry A. Kazakov
2007-06-20 15:15         ` Fionn Mac Cumhaill
2007-06-19 21:40     ` Randy Brukardt

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox