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

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

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?