Re: Exceptions and out procedure arguments (using GNAT GPL)

["Dmitry A. Kazakov" <mailbox@dmitry-kazakov.de>]

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