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

[Georg Bauhaus <bauhaus.rm.tsoh@maps.futureapps.de>]

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?