Version 1.7 of ai05s/ai05-0269-1.txt

• if the tested type is an access type and the named subtype excludes null, the value of the simple_expression is not null.

• if the tested type is an access type and the named subtype excludes null, the value of the simple_expression is not null;

• if the tested type is a general access-to-object type, the type of the simple_expression is convertible to the tested type and its accessibility level is no deeper than that of the tested type; further, if the designated type of the tested type is tagged and the simple_expression is non-null, the tag of the object designated by the value of the simple_expression is covered by the designated type of the tested type.

• a dependent_expression of a case_expression whose selecting_expression is static and whose value is not covered by the corresponding discrete_choice_list; or

No_Implementation_Attributes

There are no implementation-defined attributes. This restriction applies only to the current compilation or environment, not the entire partition.

No_Implementation_Identifiers

There are no usage names that denote declarations with implementation-defined identifiers that occur within language-defined packages or instances of language-defined generic packages. Such identifiers can arise as follows:

• If T is an array type, S'Output first writes the bounds, and S'Input first reads the bounds. If T has discriminants without defaults, S'Output first writes the discriminants (using S'Write for each), and S'Input first reads the discriminants (using S'Read for each).

• If T is an array type, S'Output first writes the bounds, and S'Input first reads the bounds. If T has discriminants without defaults, S'Output first writes the discriminants (using the Write attribute of the discriminant type for each), and S'Input first reads the discriminants (using the Read attribute of the discriminant type for each).

From: Steve Baird
Sent: Friday, March 11, 2011  7:06 PM

[This message was misplaced which is why it is getting handled in this AI; only the
relevant part is included here.]

While looking at this, I did notice a minor wording issue.

In 13.13.2(26), the parenthesized wording eems wrong:

    If T has discriminants without defaults, S'Output first writes the
    discriminants (using S'Write for each), and S'Input first reads the
    discriminants (using S'Read for each).

S is a discriminated subtype. We are using S'Write and S'Read to write/read single
discriminant values? Probably "using S'Write" should be replaced with something like "using
the Write attribute of each dicriminant type", and similarly for Read.

****************************************************************

From: Bob Duff
Sent: Wednesday, September 15, 2010  4:39 PM

[This thread was unintentionally ignored and just now has been rediscovered,
which is why it is getting handled in this AI - Editor.]

AI05-0193-1: Alignment of allocators says:

    The Alignment parameter is at least D'Alignment if D is a specific type,
    and otherwise is at least the alignment of the specific type identified by
    the tag of the object being created. The Alignment parameter is no more
    than D'Max_Alignment_For_Allocation.

Shouldn't it say it's "equal to or stricter than D'Alignment"?
That is, equal to D'Alignment, or some positive integer multiple thereof.

Because if D'Alignment is 4, you don't want to pass Alignment => 5 to Allocate.
4, 8, or 16 should be OK. 12 is weird, but still OK, I guess.

****************************************************************

From: Robert Dewar
Sent: Wednesday, September 15, 2010  4:41 PM

Only powers of 2 make sense for alignments anyway, so in practice greater/less
than mean the same as multiple/factor

****************************************************************

From: Tucker Taft
Sent: Wednesday, September 15, 2010  5:05 PM

I agree "stricter" is more correct.
Do we use that term elsewhere?

****************************************************************

From: Bob Duff
Sent: Wednesday, September 15, 2010  5:39 PM

> I agree "stricter" is more correct.
> Do we use that term elsewhere?

Only in the AARM, as far as I know.

I don't think we need to have a formal definition of "stricter" in order to use
it in the RM. It's clear what it means.

Or we can just leave it alone, and trust implementers to never pass Alignment=>5
or the like.

Re: Robert's comment: I would have been happy with a rule saying Alignment must
be a power of 2. I can't imagine any hardware (past, present, or future) where
anything else would make sense. I'd be interested in hearing of
counter-examples, if such exist[ed]!

****************************************************************

From: Robert Dewar
Sent: Wednesday, September 15, 2010  6:11 PM

Certainly GNAT requires alignments to be a power of 2

****************************************************************

From: Tucker Taft
Sent: Wednesday, September 15, 2010  6:09 PM

> I don't think we need to have a formal definition of "stricter" in
> order to use it in the RM.
> It's clear what it means. ...

What I was really asking was how do we require that one alignment be stricter
than another alignment in other places in the manual.  I just looked in the
section on the 'Alignment attribute, and we always talk in terms of one
alignment being a multiple of another alignment.  So I think we should use that
terminology here, rather than "greater" or "stricter".

****************************************************************

From: Bob Duff
Sent: Wednesday, September 15, 2010  6:31 PM

OK, that makes sense.

[Randy will no doubt include this in the appendix of the AI in a way that makes
the referent of "that" in "that makes sense" unclear.  Sigh.]

[Editor's note: I did my best to follow his instructions. :-) If you the reader
are really confused, the preceeding message is the referent.]

****************************************************************

From: Randy Brukardt
Sent: Monday, September 27, 2010  5:59 PM

Forget my filing system: my new phone just showed "OK, that makes sense"
with all of the quoted stuff eliminated. So I didn't find out what you meant
until I looked at it here in the office. Probably best to write a few more words
(but that's not fun when answering from a phone).

****************************************************************

From: Bob Duff
Sent: Monday, September 27, 2010  6:19 PM

Reading e-mail on a phone is something I would never consider doing.
I realize that makes me a luddite.  ;-)

But seriously, I don't think you should be vigorously trying to keep the
!appendix sections small.  Over-quoting is a sin, but underquoting is a worse
sin.  I really find it hard to follow the conversation when I can't tell what
someone is replying to.

And I was deliberately yanking your chain when I wrote just "OK, that makes
sense.", which is incomprehensible without context.  ;-)

****************************************************************

From: Randy Brukardt
Sent: Friday, January 27, 2012  1:53 AM

A couple of weeks ago, I responded to one of Steve's comments thusly:

> > 13.11(21.5/3) says
> >    The Alignment parameter is at least D'Alignment if D is a
> > specific type, ...
> >
> > It does seem odd that if D'Alignment is 4, then this would allow
> > passing in a value of 5.
> >
> > We may have already talked about this one and decided to ignore it.
>
> I vaguely remember such a discussion, but it doesn't seem to appear in
> the filed e-mail (or we decided to ignore it).
>
> It doesn't seem too critical; it sounds hard to nail this down
> perfectly. (I can't think of a reason to support an alignment of, say
> 6, but I wouldn't be surprised of someone had a reason on some unusual
> machine. So requiring only powers-of-two along wouldn't seem
> appropriate to me.)

I just ran across the old e-mail discussion (from September 2010!). Tucker
suggested using "multiple" as that is what 13.3 uses when comparing to
alignments. (Actually, the wording is "nonzero integral multiple".) It seems
that your editor was supposed to make this change, but it got lost in a blizzard
of mail on other topics.

So the wording should be:

The Alignment parameter is a nonzero integral multiple of D'Alignment if D is a
specific type, and otherwise is a nonzero integral multiple the alignment of the
specific type identified by the tag of the object being created.

Please speak up if you (or anyone) disagrees for some reason. (It's been a year
and a half; everyone should have changed their minds by now... :-)

****************************************************************

From: Alan Burns
Sent: Monday, September 19, 2011  4:51 AM

We have just held IRTAW - lots of interesting stuff for post Ada2012!

But a couple of 'editorial' issues were noted with regard to D.16.1

package System.Multiprocessors.Dispatching_Domain has pragma Preelaborate. But it also
withs Ada.Real-Time that does not have this pragma. This seems to be wrong.

... [Rest omitted here, in AI05-0278-1.]

****************************************************************

From: Brad Moore
Sent: Wednesday, December 28, 2011  10:29 AM

[Part of a larger review... - Editor]

A.18.18 (73.a.1/3) Delete this paragraph, it is almost identical to the preceding
paragraph, and the 'Implementation Advice' tag is also redundant, since it falls
under the 'Implementation Advice' section.

...

If the preceding paragraphs are necessary, then there is a consistency problem, because
some of the containers do not have these redundant paragraphs.

****************************************************************

From: Randy Brukardt
Sent: Friday, December 30, 2011  11:38 PM

> A.18.18 (73.a.1/3) Delete this paragraph, it is almost identical to
> the preceding paragraph, and the 'Implementation Advice' tag is also
> redundant, since it falls under the 'Implementation Advice' section.

This is the "marker" note for the what becomes the contents of the Implementation
Advice annex (which is automatically generated from these notes). We could consider
suppressing these globally (so they aren't shown at all), but doing so would change
the paragraph numbers of some AARM notes silently, so that would not be a great idea.

...
> If the preceding paragraphs are necessary, then there is a consistency
> problem, because some of the containers do not have these redundant
> paragraphs.

Anything that doesn't have these paragraphs won't show up in the Annex (M.3), which would
be a fairly serious bug. There should be one after every implementation advice (or some
other note stating that we don't want an annex entry, there is a couple of cases of that).

I can't find any missing ones on a quicky random check. If you can, please tell me so
that I can fix them somehow.

****************************************************************

From: Brad Moore
Sent: Saturday, December 31, 2011  10:22 AM

The inconsistent containers are ;

A.18.22 The Generic Package Containers.Bounded_Ordered_Maps
        <cid:part1.08030602.04050506@shaw.ca>
A.18.24 The Generic Package Containers.Bounded_Ordered_Sets
        <cid:part2.01030905.05000005@shaw.ca>

****************************************************************

From: Randy Brukardt
Sent: Saturday, December 31, 2011  5:25 PM

Ah, I see that's intentional, because the wording of the Implementation Advice is
identical to the hashed versions. It would look insane to repeat that wording twice
in a row in the annex.

There should have been a comment in the code (rather than just in the source, where
there is one), so you could see why it is omitted.

Arguably, omitting these is a bad idea because the section reference is missed in the
annex. In that case, we need to change the (normative) wording of all four sets of this
advice to add "ordered" and "hashed" appropriately. Should we do that? What do you think?

****************************************************************

From: Brad Moore
Sent: Tuesday, January  3, 2012  12:22 PM

Definitely not a high priority issue, but if it's not too much trouble, I think it
would be good to make the changes in the name of consistency, otherwise it looks like
an omission.

****************************************************************

From: Steve Baird
Sent: Monday, January 9, 2012  3:43 PM

[Part of a larger review... - Editor]

Oh dear. I read 13.11.3 and became very confused. It isn't at all clear for which
entities the Default_Storage_Pool aspect may be specified.
5/3 says
   The language-defined aspect Default_Storage_Pool may be used to define
   the default pool for access types within an instance.

Is this a roundabout way of saying that this aspect may be specified for an instance?
It reads like non-normative introductory text. More precise wording is definitely needed,
especially when we are doing non-intuitive things like allowing it to be specified via
an aspect definition clause for an instance, but only via a pragma for a generic.
Or something like that. I can't tell.

Did we lose a paragraph or something?

****************************************************************

From: Randy Brukardt
Sent: Friday, January 13, 2012  1:22 AM

...
> Is this a roundabout way of saying that this aspect may be
> specified for an instance?

Yes (I think). The AARM notes explain the intended model, but I agree that the
normative wording ought to match.

> It reads like non-normative introductory text.
> More precise wording is definitely needed, especially when we
> are doing non-intuitive things like allowing it to be
> specified via an aspect definition clause for an instance,
> but only via a pragma for a generic. Or something like that.
> I can't tell.
>
> Did we lose a paragraph or something?

No, that's the wording in the original AI. So it is more that the text was
never there.

I don't think much additional is actually needed, add a second sentence:

"The aspect can be specified for a generic instance".

Or maybe it is better to just change the first sentence:

The language-defined aspect Default_Storage_Pool may be {specified for a generic
instance; it defines} [used to define] the default pool for access types within
an instance.

****************************************************************

From: Randy Brukardt
Sent: Saturday, February  4, 2012 12:35 AM

7.3.2(14-15/3) says:

Upon successful return from a call on any subprogram or entry that:
*is explicitly declared within the immediate scope of type T (or by an instance of a
generic unit, and the generic is declared within the immediate scope of type T), and

Erhard points out (in a very convoluted way, unfortunately, I wasted 20 minutes
writing an explanation before stumbling onto his point), that this means that
implicitly declared subprograms, like inherited primitives, aren't covered by invariant
checks "on the way back". And this means that 7.3.2(22/3) is a lie, which is surely
not our intent.

I can't find any reason for the "explicitly" in this bullet, so I've just deleted it,
in which case the rules work and the note is true. But I worry that it was there for
some good reason. If the reason was to avoid wrappers, well, we decided that we didn't
want to do that (as evidenced by the 7.3.2(22/3) note), so then the word is just wrong.

If there was any other reason, I can't figure it out, and I didn't find anything in the
AIs to help. Anyone else remember? (Tucker in particular.) More generally, anyone know
of a reason not to delete this stray "explicitly"?

****************************************************************

From: Tucker Taft
Sent: Saturday, February  4, 2012 11:10 AM

> I can't find any reason for the "explicitly" in this bullet, so I've
> just deleted it, in which case the rules work and the note is true.
> But I worry that it was there for some good reason. If the reason was
> to avoid wrappers, well, we decided that we didn't want to do that (as
> evidenced by the
> 7.3.2(22/3) note), so then the word is just wrong.

I have some trouble parsing your last sentence.  Could you clarify?
"We didn't want to do that" -- what is "that"?  And "the word is just wrong" --
what word?

In any case, we spent a lot of time on wording this, and we covered the case of
inherited primitives in paragraph 12, because when calling an inherited
primitive, there are view conversions applied, and those view conversions do the
check (per paragraph 12). Of course some kind of AARM note, or perhaps even a
user NOTE, might help clarify this case.

> If there was any other reason, I can't figure it out, and I didn't
> find anything in the AIs to help. Anyone else remember? (Tucker in
> particular.) More generally, anyone know of a reason not to delete
> this stray "explicitly"?

See above.  I believe it is correct as written, given paragraph 12.

****************************************************************

From: Randy Brukardt
Sent: Saturday, February  4, 2012  4:17 PM

> I have some trouble parsing your last sentence.  Could you clarify?
> "We didn't want to do that" -- what is "that"?  And "the word is just
> wrong" -- what word?

"the word" is "explicitly" in 7.3.2(15/3). "that" is "avoid wrappers". I realize
there is a double negative here, but my point is that 7.3.2(22/3) says that we
expect to need wrappers for inherited subprograms, so any wording that is
intended to avoid such a need is unnecessary.

> In any case, we spent a lot of time on wording this, and we covered
> the case of inherited primitives in paragraph 12, because when calling
> an inherited primitive, there are view conversions applied, and those
> view conversions do the check (per paragraph 12).
> Of course some kind of AARM note, or perhaps even a user NOTE, might
> help clarify this case.

There are view conversions to T. What covers the checks on NT on the way out?
And if you say the view conversions, then what rule causes the checks on T (in
the inherited subprogram) on the way out (because we're not (formally) calling
the T routine, so we don't get to apply the rules associated with T).

> > If there was any other reason, I can't figure it out, and I didn't
> > find anything in the AIs to help. Anyone else remember? (Tucker in
> > particular.) More generally, anyone know of a reason not to delete
> > this stray "explicitly"?
>
> See above.  I believe it is correct as written, given paragraph 12.

Neither Erhard nor I see how paragraph 12 applies. Please explain how this
actually works (I realize this has been done before, but please try again).

Specifically, in the note 7.3.2(22/3), what rule triggers the check of the
invariant of NT for an out parameter (on return from the call))? And why?
Similarly for the check of the invariant of T (again on return from the call)?

When I read 7.3.2(12/3), it says that a check is made on a view conversion from
T to an ancestor of T. It then says something about the same check being made on
in out parameters. But that doesn't happen for an "in out" parameter, because
the conversion goes from T to NT, and NT is not an ancestor of T. So there is no
check to be made in that case.

I can easily believe Erhard is wrong, and he got me so confused that I can no
longer see what the intent is much less whether the rules cover that intent.
(That's why I didn't quote his original message, I didn't want that effect to
happen to anyone else.)

But it seems to me that something is missing here. I had thought that it just
was applying the explicit check to inherited subprograms (that seems to be the
easiest way to deal with this), but perhaps 12/3 was supposed to do it (but
doesn't). Or maybe 12/3 has mixed up static and dynamic semantics to the point
it is incomprehensible...

Anyway, thanks in advance for the clear explanation I'm sure to receive.

****************************************************************

From: Tucker Taft
Sent: Saturday, February  4, 2012  5:00 PM

> There are view conversions to T. What covers the checks on NT on the
> way out? And if you say the view conversions, then what rule causes
> the checks on T (in the inherited subprogram) on the way out (because
> we're not
> (formally) calling the T routine, so we don't get to apply the rules
> associated with T).

Here is paragraph 12:

     After assigning to a view conversion, outside the immediate scope
     of T, that converts from T or one or more record extensions (and
     no private extensions) of T to an ancestor of type T, a check is
     performed on the part of the object that is of type T; similarly,
     for passing a view conversion as an out or in out parameter
     outside the immediate scope of T, this check is performed upon
     successful return;

I'm not sure what you meant by "NT" above.  Is that the ancestor of T from which
it is inheriting the subprogram?  I will assume that, even though usually "NT"
is meant to signify a *descendant* of T.

Anyway, when calling a subprogram inherited by T from its ancestor T0, if there
is an invariant that applies to T, then at the point of calling the inherited
subprogram, what happens is that the primitive of T0 is called, with all
parameters of type T0 in that primitive of T0 being passed view conversions from
T to T0. If any of them are OUT or IN OUT parameters, then based on para. 12
above, on the way back, a check is performed on the T part of the object that is
identified in the view conversion, which in this case is the whole thing.  For
example:

    type T0 is ...
    procedure Update(X : out T0);

...

    type T is new T0 with ...
      with Type_Invariant => Is_Valid(T) = True;

    -- Update inherited

...

     Y : T;

     Update(Y);
       --> this becomes a call on T0's Update:

        Update(T0(Y))

       --> That "T0(Y)" is a view conversion being
       --> passed as an OUT parameter, so per para. 12, a
       --> check on T's invariant is performed
       --> on Y if the call completes successfully.
       --> If T0 also has an invariant, then it is checked on T0(Y)
       --> upon return from the call on T0's Update, and
       --> if that succeeds, then we would perform T's invariant
       --> check on Y as a whole.

>>> If there was any other reason, I can't figure it out, and I didn't
>>> find anything in the AIs to help. Anyone else remember? (Tucker in
>>> particular.) More generally, anyone know of a reason not to delete
>>> this stray "explicitly"?
>>
>> See above.  I believe it is correct as written, given paragraph 12.
>
> Neither Erhard nor I see how paragraph 12 applies. Please explain how
> this actually works (I realize this has been done before, but please try again).

See example above.  Let me know if this is not clear.

> Specifically, in the note 7.3.2(22/3), what rule triggers the check of
> the invariant of NT for an out parameter (on return from the call))? And why?
> Similarly for the check of the invariant of T (again on return from
> the call)?

I don't know how NT relates to T.  Hopefully you can make appropriate
substitutions into my example above using T and T0.

> When I read 7.3.2(12/3), it says that a check is made on a view
> conversion from T to an ancestor of T. It then says something about
> the same check being made on in out parameters. But that doesn't happen for an "in out"
> parameter, because the conversion goes from T to NT, and NT is not an
> ancestor of T. So there is no check to be made in that case.

I believe you are slightly misreading it.  The actual parameter is a "view
conversion" from the descendant type to the ancestor type, (from T to T0 in my
example) even though upon return, the (conceptual) value conversion actually
goes the opposite way, namely from T0 back to T.  But of course you can't really
do the reverse as a "value conversion" for a tagged type, since you wouldn't
know where to come up with the values for the additional components.  So there
is really no conversion going the other way, it is logically more like an
assignment to the T0 part of the actual parameter, so it is more like:

    T0(Y) := Final_Value_Of_Formal_Param;

So again, the view conversion involved is from T to T0.
even though the logical flow of data is from an object of type T0 to (the T0
part) of an object of type T.

View conversions are confusing.  I would recommend rereading 4.6(52-56).  For a
tagged type, since they are passed by reference, there is no conversion "back"
after a call for an OUT parameter.  And even if there were, it would have the
semantics of the assignment I showed above.

> I can easily believe Erhard is wrong, and he got me so confused that I
> can no longer see what the intent is much less whether the rules cover
> that intent. (That's why I didn't quote his original message, I didn't
> want that effect to happen to anyone else.)
>
> But it seems to me that something is missing here. I had thought that
> it just was applying the explicit check to inherited subprograms (that
> seems to be the easiest way to deal with this), but perhaps 12/3 was
> supposed to do it (but doesn't). Or maybe 12/3 has mixed up static and
> dynamic semantics to the point it is incomprehensible...
>
> Anyway, thanks in advance for the clear explanation I'm sure to receive.

I hope I have clarified things, but probably not...

****************************************************************

From: Randy Brukardt
Sent: Saturday, February  4, 2012  5:54 PM

> I hope I have clarified things, but probably not...

Doesn't look like it. :-(

> I'm not sure what you meant by "NT" above.  Is that the ancestor of T
> from which it is inheriting the subprogram?  I will assume that, even
> though usually "NT" is meant to signify a *descendant* of T.

Erhard was asking about the "note" 7.3.2(22/3) which talks about types NT and T.
I've mentioned that several times, in parts of my messages that you haven't
quoted, so I'm not surprised that you missed that.

But I think we need to stick to the T and NT types, so we can understand this in
terms of the wording that's actually in the RM.

> > Specifically, in the note 7.3.2(22/3), what rule triggers the check
> > of the invariant of NT for an out parameter (on return from the
> > call))? And
why?
> > Similarly for the check of the invariant of T (again on return from
> > the call)?
>
> I don't know how NT relates to T.  Hopefully you can make appropriate
> substitutions into my example above using T and T0.

That's explained in the note! There's a reason that I specifically mentioned the
note above!! Erhard (and by corollary, me) wanted to relate the note to the
rules, and neither of us have been able to do it.

So now we have three people not paying much attention to each other...
(grumble).

I would have thought that I didn't have to copy large blocks of text out of the
RM because we can read each other...

"A call of a primitive subprogram of type NT that is inherited from type T needs
to satisfy the specific invariants of both the types NT and T. A call of a
primitive subprogram of type NT that is overridden for type NT needs to satisfy
only the specific invariants of type NT."

Sigh. So I'll try to manually substitute the names of the types in your
following text and see if it makes any sense.

...
> Anyway, when calling a subprogram inherited by NT from its ancestor T,
> if there is an invariant that applies to NT, then at the point of
> calling the inherited subprogram, what happens is that the primitive
> of T is called, with all parameters of type T in that primitive of T
> being passed view conversions from NT to T.

Yup, knew that.

> If any of them are OUT or IN OUT parameters, then based on para. 12
> above, on the way back, a check is performed on the NT part of the
> object that is identified in the view conversion, which in this case
> is the whole thing.

Maybe that's what's supposed to happen, but I can't see that in 7.3.2(12/3).
Maybe the problem is that it talks about "this check" for in out parameters, but
the previously described check as nothing to do with this case. The described
check goes in the other direction to to the one we need here (because we're
going from T to NT here).

>  For example:
>
>     type T is ...
>     procedure Update(X : out T);
>
> ...
>
>     type NT is new T with ...
>       with Type_Invariant => Is_Valid(NT) = True;
>
>     -- Update inherited
>
> ...
>
>      Y : NT;
>
>      Update(Y);
>        --> this becomes a call on T's Update:

No, it doesn't. It's a call on NT's update, that executes the body of T with
view conversions of the parameters.

Ohhh, having looked this up, I see the 3.4(27/2) actually says this. No wonder
we have such trouble with overriding, because a model based on real calls has no
hope of working in face of multiple inheritance and/or null/abstract subprograms
with no implementation. Never mind that though.

We have AARM notes in 7.3.2 (22.a/3) that try to explain this, but they way miss
the mark because I don't understand the model either. Perhaps you could try
clarifying the AARM note to repeat the entire model (it's obvious that hardly
anyone, even inside the ARG, understands it, so writing notes that assume that
they do isn't helping much).

The AARM note at least has to mention the call model and have a cross-reference
to 3.4.

Here's an attempt:

Proof: This follows from the definition of inheritance as view conversions of
the parameters of the type {and a call to the original routine (see 3.4)}, along
with {the normal invariant checking rules}[ the rules require checks on such
view conversions]. {In particular, the call to the original routine takes care
of any checks needed on type T, and the checks required on view conversions take
care of any checks needed on type NT, specifically on in out and out
parameters.} We require this in order that the semantics of an explicitly
defined wrapper that does nothing but call the original routine is the same as
that of an inherited routine.

Can this be clearer still??

>         Update(T(Y))
>
>        --> That "T(Y)" is a view conversion being
>        --> passed as an OUT parameter, so per para. 12, a
>        --> check on NT's invariant is performed
>        --> on Y if the call completes successfully.
>        --> If T also has an invariant, then it is checked on T(Y)
>        --> upon return from the call on T's Update, and
>        --> if that succeeds, then we would perform NT's invariant
>        --> check on Y as a whole.

Back to paragraph 12/3 and the note 22/3. The note says that the above is what
happens, so it's pretty obvious that this is the intent. But I can't see how to
get this out of paragraph 12/3, beyond your say-so.

...
> > When I read 7.3.2(12/3), it says that a check is made on a view
> > conversion from T to an ancestor of T. It then says something about
> > the same check being made on in out parameters. But that doesn't
> > happen for an "in out"
> > parameter, because the conversion goes from T to NT, and NT is not
> > an ancestor of T. So there is no check to be made in that case.
>
> I believe you are slightly misreading it.  The actual parameter is a
> "view conversion" from the descendant type to the ancestor type, (from
> NT to T in my example) even though upon return, the (conceptual) value
> conversion actually goes the opposite way, namely from T back to NT.
> But of course you can't really do the reverse as a "value conversion"
> for a tagged type, since you wouldn't know where to come up with the
> values for the additional components.  So there is really no
> conversion going the other way, it is logically more like an
> assignment to the T part of the actual parameter, so it is more like:
>
>     T(Y) := Final_Value_Of_Formal_Param;
>
> So again, the view conversion involved is from NT to T.
> even though the logical flow of data is from an object of type T to
> (the NT part) of an object of type NT.
>
> View conversions are confusing.  I would recommend rereading
> 4.6(52-56).  For a tagged type, since they are passed by reference,
> there is no conversion "back" after a call for an OUT parameter.  And
> even if there were, it would have the semantics of the assignment I
> showed above.

Well, duh, it's obvious that they're confusing.

Even with your roadmap here I'm skeptical. I can't imagine how an ordinary user
would ever be able to figure out when this would happen (and that's necessary
for understanding the cause of failures).

At least part of the problem here is all of the emphasis on what the view
conversion goes to (which is backwards from anything that we care about). I have
to wonder if we care about any of that in the first place. Are there any view
conversions from a *private* type (and outside the package) that we would *not*
care about? I mean, don't we need to do this even for derived scalar types? (If
T and NT are ultimately scalar types or access types, don't we still want the
same checks of their invariants?) And you can't convert to a more derived type
(that would require adding components, which isn't possible). So what am I
missing

So, I guess what I'm saying, is what is wrong with something like:

After assigning to a view conversion, outside the immediate scope of T, that
converts an object of type T to some other type, a check is performed on the
part of the object that is of type T; similarly, for passing a view conversion
as an out or in out parameter outside the immediate scope of T, this check is
performed upon successful return;

And even here I'd prefer to get rid of the "from" and "to" (since they're
confusing beyond belief), unfortunately, I wasn't able to do it. Perhaps we
could just drop the "to some other type" (irrelevant as previously noted), but
that seems a bit vague:

After assigning to a view conversion, outside the immediate scope of T, that
converts an object of type T, a check is performed on the object; similarly, for
passing a view conversion as an out or in out parameter outside the immediate
scope of T, this check is performed upon successful return;

(I dropped the whole "the part of the object" here, because it is irrelevant for
the reverse type conversion -- the check is on the  result of that reverse type
conversion, which is the entire object. You'd need to check only a part if you
were making the forward check to the ancestor, but if I understand you
correctly, that is not the part that this rule is covering. To wit: an
assignment to a view conversion of NT to T assigns just the T part, but the
check is on the entire NT object.)

By now, I have this completely wrong. Enjoy straightening me out... :-)

****************************************************************

From: Erhard Ploedereder
Sent: Saturday, February  4, 2012  7:08 PM

Tuck, my original (convoluted?) comment was:

>> ================
>>> 7.3.2 22/3 I cannot identify the rule that requires the check of the
>>> specific invariant of type NT for the return from an inherited
>>> subprogram of T. (It's neither 12/3 nor 14-18/3.
>>> So, where is the rule?
>>> Alternatively, this part of the note would need to become a rule.)

I did not think that 12/3 covered the case. The first sentence talks exclusively
about upcasts. The second says "similarly", so upcasts only.

The note says:
13 A call of a primitive subprogram of type NT that is inherited from type T
needs to satisfy the specific invariants of both the types NT and T. A call of a
primitive subprogram of type NT that is overridden for type NT needs to satisfy
only the specific invariants of type NT.

(Come to think of it, now the second sentence of the Note becomes very
mysterious, too, since for a redefinition dispatchingly called via the parent
method such an upcast would happen on the way out and hence invariants of T
would be checked.)

****************************************************************

From: Tucker Taft
Sent: Sunday, February  5, 2012 12:03 PM

> I did not think that 12/3 covered the case. The first sentence talks
> exclusively about upcasts. The second says "similarly", so upcasts
> only.

Oh boy, now we are changing the vocabulary again!
By "upcast" I presume you mean a view conversion from a descendant to an
ancestor.  The important thing to realize is that a view conversion is
*writable*. It doesn't really convert the data, it just provides a narrowed view
of it, so you only see the ancestor part of some descendant.  Through a view
conversion you can willy-nilly change the ancestor part of the descendant
object, using assignments, passing as OUT parameters, etc.

The challenge is that the type-invariant on a descendant might depend on the
consistency between data residing in the ancestor part with data in the
extension part(s) after that.  So if someone changes the ancestor part, then we
need to recheck the various invariants of any descendants.

> The note says:
> 13 A call of a primitive subprogram of type NT that is inherited from
> type T needs to satisfy the specific invariants of both the types NT
> and T. A call of a primitive subprogram of type NT that is overridden
> for type NT needs to satisfy only the specific invariants of type NT.

OK, sorry I missed the reference to the Note.  Thanks for copying it here.  So
what this is saying is that if NT inherits an operation from T rather than
overriding it, both the T invariant is checked, and then the NT invariant.
Paragraph 12 ensures that the NT invariant is checked, because a call on an
inherited subprogram turns into a call on the ancestor's subprogram with
controlling parameters being view conversions, so [IN] OUT controlling
parameters which are view conversions will trigger para 12. The normal semantics
of the subprogram call on the original T subprogram takes care of the check on
the T invariant.

If you override with a new NT subprogram, then T's invariant isn't checked as
part of the call on this new subprogram. On the other hand, if inside this
subprogram there is a call on a primitive of T to update the T "part" of the
object, then there will be a check on T's invariant at that point. But that is
buried inside the NT primitive, and we aren't worried about that in this note.

> (Come to think of it, now the second sentence of the Note becomes very
> mysterious, too, since for a redefinition dispatchingly called via the
> parent method such an upcast would happen on the way out and hence
> invariants of T would be checked.)

You are using "upcast" in a way that is totally non-Ada-like here.
There is *no* separate T-to-NT view conversion "on the way out,"
on any sort of call.  In fact, normally there is absolutely nothing that happens
"on the way out."  All the "damage" has already been done, since tagged types,
including view conversions thereof, are passed by *reference.*  But with
Type_Invariants we now *do* have something done "on the way out."  But the view
conversion is still syntactically and semantically going from NT to T, even
though you might logically think of this as some kind of "upcast" back to NT.
*Don't think about it that way!* You will get yourself totally confused (and
take Randy along with you ;-).

****************************************************************

From: Erhard Ploedereder
Sent: Sunday, February  5, 2012  3:32 PM

> Oh boy, now we are changing the vocabulary again!
> By "upcast" I presume you mean a view conversion from a descendant to
> an ancestor.

Merely too lazy to spell out "a view conversion, outside the immediate scope of
T, that converts from T or one or more record extensions (and no private
extensions) of T to an ancestor of type T". I'll stay lazy and call this
mouthful an "upcast" in this msg.

> You are using "upcast" in a way that is totally non-Ada-like here.
> There is *no* separate T-to-NT view conversion "on the way out,"
> on any sort of call.

My 2 a.m. mistake. I remembered the rule 6.4.1 (17):
"After normal completion and leaving of a subprogram, for each in out or out
parameter that is passed by copy, the value of the formal parameter is converted
to the subtype of the variable given as the actual parameter and assigned to
it." which for inherited ops is an "upcast" NT->T, but I forgot that
by-reference types are excepted from being safe at this point and do not require
"upcast" semantics.

> But the view conversion is still syntactically and semantically going
> from NT to T, even though you might logically think of this as some
> kind of "upcast" back to NT.  *Don't think about it that way!* You
> will get yourself totally confused (and take Randy along with you .

O.k., I'll try not to. But I am still trying to understand the model and find
the rules for it. Here is my example and exegesis....

Type T is tagged private;
procedure P(X:T);

Type NT is new T;
 ...

O: T'Class := new NT;
P(O);

(1) I get different semantics wrt the specific type invariants, depending on
    whether NT redefines P. This is a bit unusual, but o.k., since these are
    specific invariants. The semantics are....

(2) When NT redefines P, then I get the specific type invariant checks for NT
    from the implicit view conversion T->NT on the way in (11/3), and then again
    from the return of the call (15/3-17/3 all apply), unless it is an "in"
    parameter (which happens to be the case here). For "in" and "in out"
    parameters, (12/3) would require the very same check again for a
    redefinition.

(3) When NT inherits P, then I get the specific type invariant checks for NT
    from the implicit view conversion T->NT on the way in (11/3), and then the
    check for T because ...... that is the rule that I had problems finding,
    since 17/3 and hence all of 14/3-18/3 does not apply -- my O is an "in"
    parameter.

So where is the rule that makes the check for T in my example?
(Don't I wish there were! But that is the "other discussion".)

If there isn't one, the note is incorrect (unless, and this is a momentary
afterthought, "needs to satisfy the invariant" is not equivalent to saying
"needs to pass the invariant check", but the "other discussion" appears to go
that way.).

About:
> The normal semantics of the subprogram call on the original T
> subprogram takes care of the check on the T invariant.
which in their entirety are spelled out by 14/3-18/3, right?
So, no help there.

****************************************************************

From: Tucker Taft
Sent: Sunday, February  5, 2012  3:59 PM

> (2) When NT redefines P, then I get the specific type invariant checks
> for NT from the implicit view conversion T->NT on the way in (11/3),
> and then again from the return of the call (15/3-17/3 all apply),
> unless it is an "in" parameter (which happens to be the case here).
> For "in" and "in out" parameters, (12/3) would require the very same
> check again for a redefinition.

Now you have confused me.  If NT redefines P, then there are no view conversions
involved.  So the only check that is relevant is any invariant on NT itself.  T
is irrelevant at this point. And as you point out below, P has no outputs, so no
invariant checks.

> (3) When NT inherits P, then I get the specific type invariant checks
> for NT from the implicit view conversion T->NT on the way in (11/3),
> and then the check for T because ...... that is the rule that I had
> problems finding, since 17/3 and hence all of 14/3-18/3 does not apply
> -- my O is an "in" parameter.

No invariant checks at all on an IN parameter (unless you get us to change
that).  Make the mode "OUT" and then we have something to discuss.

> So where is the rule that makes the check for T in my example?
> (Don't I wish there were! But that is the "other discussion".)

There are no checks on IN parameters, and the note in 22 certainly should be
interpreted as implying there are.

> If there isn't one, the note is incorrect (unless, and this is a
> momentary afterthought, "needs to satisfy the invariant" is not
> equivalent to saying "needs to pass the invariant check", but the
> "other discussion" appears to go that way.)

So you are complaining it doesn't repeat all of the earlier discussion?  It is
simply warning the user that above (in 12-21) we talk about the checks
associated with a call, and the NOTE is saying that if the operation is
inherited, then you need to worry about both the ancestor and the descendant
type.

****************************************************************

From: Randy Brukardt
Sent: Sunday, February  5, 2012  4:09 PM

...
> O.k., I'll try not to. But I am still trying to understand the model
> and find the rules for it. Here is my example and exegesis....
>
> Type T is tagged private;
> procedure P(X:T);
>
> Type NT is new T;
>  ...
>
> O: T'Class := new NT;
> P(O);
>
> (1) I get different semantics wrt the specific type invariants,
> depending on whether NT redefines P. This is a bit unusual, but o.k.,
> since these are specific invariants.
> The semantics are....
>
> (2) When NT redefines P, then I get the specific type invariant checks
> for NT from the implicit view conversion
> T->NT on the way in (11/3), and then again from the return of
> the call (15/3-17/3 all apply), unless it is an "in"
> parameter (which happens to be the case here).
> For "in" and "in out" parameters, (12/3) would require the very same
> check again for a redefinition.

When NT redefines P, there are no view conversions anywhere in the calls to the
redefined P, and thus no checks. Unless you are talking about those occurring in
an explicit body, and then the checks are on conversions to type T, not NT.

That is, the redefinition of P is:

     procedure P (X : NT) is
     begin
         P (T (X));
     end P;

There are no checks on NT anywhere here.

If X is an in out parameter, there is a check on T on the way in, and checks on
both T and NT on the way out. The check on T on the way in seems to be a mistake
(I don't think there should be any checks on the way in), but doesn't seem
possible to eliminate it.

> (3) When NT inherits P, then I get the specific type invariant checks
> for NT from the implicit view conversion
> T->NT on the way in (11/3), and then the check for T because
> ...... that is the rule that I had problems finding, since
> 17/3 and hence all of 14/3-18/3 does not apply -- my O is an "in"
> parameter.

This is an in parameter, so there should be no checks at all. The check from an
explicit conversion is unnecessary in this case, but as I said, that seems like
a bug.

Invariant checks are only on the way out of subprograms. There are never any on
the way in. The only way to get checks on the way in is to explicit write
something that forces a check (like an explicit conversion).

> So where is the rule that makes the check for T in my example?
> (Don't I wish there were! But that is the "other discussion".)

There is no check intended, so there is no rule!

> If there isn't one, the note is incorrect (unless, and this is a
> momentary afterthought, "needs to satisfy the invariant"
> is not equivalent to saying "needs to pass the invariant check", but
> the "other discussion" appears to go that way.).

The note is fine, it is only talking about in out and out parameters (there
being no checks of any kind on in parameters).

****************************************************************

From: Erhard Ploederder
Sent: Sunday, February  5, 2012  4:35 PM

> Conversions that "cross" T are also checked.
> That is perhaps what makes para 12 confusing, but it is there for a
> reason.

right. I worked it through and, apart from the "in" issue, the whole thing
works. In fact, I had played through the following example, and then deleted it
from the mail, since it did not add to my case...


Type PT is tagged private;
procedure P(X: in out PT);

type T is new PT;
   -- inherits P(X: in out T);

Type NT is new T;
 ...

O: T'Class := new NT;
P(O);

Now, if NT inherits P, you get checks for PT and NT. If it redefines, checks are
for NT only.

****************************************************************

From: Erhard Ploederder
Sent: Sunday, February  5, 2012  4:38 PM

> For "in" and "in out" parameters, (12/3) would require the very same
> check again for a redefinition.
Of course, I meant
> For "out" and "in out" parameters, (12/3) would require the very same
> check again for a redefinition.

****************************************************************

From: Erhard Ploederder
Sent: Sunday, February  5, 2012  5:01 PM

> When NT redefines P, there are no view conversions anywhere in the
> calls to the redefined P

Live and learn. I had it in my mind that a dispatching call achieved the
"change" from T'Class via T (the spec to which the name binds) to NT (the impl
dispatched to) by means of a trivially successful view conversion (as it would
have to, if one mapped the dispatching scheme to an underlying monomorphic type
system). I was wrong.

****************************************************************

From: Erhard Ploederder
Sent: Sunday, February  5, 2012  5:09 PM

A version of the note that I would have no problems with would be

13 For a call of a primitive subprogram of type NT that is inherited from type
T, the specified checks of the specific invariants of both the types NT and T
are performed. For a call of a primitive subprogram of type NT that is
overridden for type NT, the specified checks of the specific invariants of only
type NT are performed.

------ the present version for comparison:
> 13 A call of a primitive subprogram of type NT that is inherited from
> type T needs to satisfy the specific invariants of both the types NT
> and T. A call of a primitive subprogram of type NT that is overridden
> for type NT needs to satisfy only the specific invariants of type NT.

****************************************************************

From: Tucker Taft
Sent: Sunday, February  5, 2012  6:56 PM

Works for me.

****************************************************************

From: Randy Brukardt
Sent: Sunday, February  5, 2012  3:14 PM

...
> OK, sorry I missed the reference to the Note.

Yes, I know that. Despite the fact that I mentioned it three times. Grrrr.

...
> Paragraph 12 ensures that the NT invariant is checked, because a call
> on an inherited subprogram turns into a call on the ancestor's
> subprogram with controlling parameters being view conversions, so [IN]
> OUT controlling parameters which are view conversions will trigger
> para 12.
> The normal semantics of the subprogram call on the original T
> subprogram takes care of the check on the T invariant.

That's what paragraph 12 should say, but it is bogged down in verbal diarrhea;
it babbles on about things that are irrelevant and thus confuses the issue to
the point where I'm not even convinced it's right.

So I want to start over with that text. I proposed a rewording in a previous
message that you didn't read, and since I figure you won't read this one either
(at least not in detail), I'll explain that in a separate message.

****************************************************************

From: Tucker Taft
Sent: Sunday, February  5, 2012  3:28 PM

> ... So, I guess what I'm saying, is what is wrong with something like:
>
> After assigning to a view conversion, outside the immediate scope of
> T, that converts an object of type T to some other type, a check is
> performed on the part of the object that is of type T; similarly, for
> passing a view conversion as an out or in out parameter outside the
> immediate scope of T, this check is performed upon successful return;

The problem is that if a view conversion goes from a (proper) descendant of T to
a (proper) ancestor of T, then there are checks as well.  So it is not just when
you convert from T itself.  Conversions that "cross" T are also checked. That is
perhaps what makes para 12 confusing, but it is there for a reason.

>
> And even here I'd prefer to get rid of the "from" and "to" (since
> they're confusing beyond belief), unfortunately, I wasn't able to do
> it. Perhaps we could just drop the "to some other type" (irrelevant as
> previously noted), but that seems a bit vague:
>
> After assigning to a view conversion, outside the immediate scope of
> T, that converts an object of type T, a check is performed on the
> object; similarly, for passing a view conversion as an out or in out
> parameter outside the immediate scope of T, this check is performed
> upon successful return;

Again, I believe you are losing the checks that arise in view conversions that
"cross" T, but don't start at T.

> (I dropped the whole "the part of the object" here, because it is
> irrelevant for the reverse type conversion -- the check is on the
> result of that reverse type conversion, which is the entire object.
> You'd need to check only a part if you were making the forward check
> to the ancestor, but if I understand you correctly, that is not the part that this rule is covering.
> To wit: an assignment to a view conversion of NT to T assigns just the
> T part, but the check is on the entire NT object.)
>
> By now, I have this completely wrong. Enjoy straightening me out...
> :-)

See above.  I do remember struggling with this wording in Edinburgh, and almost
every word in para. 12 was debated.  So fixing it won't be easy without losing
something.

****************************************************************

From: Randy Brukardt
Sent: Sunday, February  5, 2012  3:55 PM

[Editor's note: This message crossed in the mail with Tucker's previous
message.]

As noted in my last message, now that I understand (again) the intent, it's
clear to me that 7.3.2(12/3) is far more complex a rule than needed. It should
be simplified.

[For those of you with limited time, feel free to skip to the end of this
message to see the payoff. But if you have questions, *read* my message, don't
ask questions that I've already answered!]


Starting from principles. What we're trying to accomplish with these checks is
essentially:

Outside of the package of type T, any modification of an object of type T should
be checked that the invariant of T holds after the modification.

OK, let's get more specific about the case of interest:

Outside of the package of type T, any object of type T where all or some part of
the object is replaced by an object of some other type should be checked that
the invariant of T holds after the replacement.

Since T has to be a private type, there aren't many cases of this. The case of
interest involves view conversions.

Still speaking informally, that means we're interested in the following
case:

Outside of the package of type T, any assignment (implicit or explicit) to a
view conversion with a source of type T should be checked that the invariant of
T holds after the assignment.

It's important to note here that the target type of the conversion is completely
irrelevant. It does not matter what type the replaced part of the object is,
because we need to check the whole object afterwards. We also don't need to talk
about "parts", because a view conversion can only change the type of the object
itself, not that of any components. (There is no view conversion of an array of
NT becoming an array of T, for instance.)

Even if the only kind of view conversion (I'm not certain) that is relevant is a
tagged extension conversion, that's irrelevant to both the reason for the check
and the details of the check. So leave it out!

Similarly, since this check can never have anything to do with parts, leave that
out too. All of that extra wording just confuses the important issues.

I think we also want to be a bit more explicit about what is being checked (also
to avoid confusion).

Now, I realize the wording I have above is too informal; the "in out"
parameter case is not really an assignment at all. So we have to have a separate
sentence to cover that.

And we need something to handle the visible extension case (but again, this
should apply to any derived type, not just extensions). The key is to
think only of conversions between directly related types.

So here's my attempt:

Outside the immediate scope of T:
   * after assigning to a view conversion that converts an object of T, a check
     is performed on the object;
   * after a call that passes a view conversion of an object of T as an out or
     in out parameter, a check is performed on the actual object.
For the purposes of determining the need for these checks, each view conversion
is considered a set of nested view conversions including each visible ancestor
between the source and target types.

Discussion: The last rule means that if we have:
     type T is ...
     type NT is new T ...
     type NNT is new NT ...
     Obj : NNT;
     P (... T(Obj) ...);
then the checks are applied as if the view conversion was NT(T(Obj)).

I'm sure this can be improved.

The other thing that needs to be improved is the AARM note that tries to explain
22/3, perhaps if it had been more explicit we would have headed off Erhard's
original complaint. I put a suggestion into a previous message, and I'm not
going to confuse the issue including it here.

****************************************************************

From: Randy Brukardt
Sent: Monday, February  6, 2012 10:04 PM

> > ... So, I guess what I'm saying, is what is wrong with something like:
> >
> > After assigning to a view conversion, outside the immediate scope of
> > T, that converts an object of type T to some other type, a check is
> > performed on the part of the object that is of type T; similarly,
> > for passing a view conversion as an out or in out parameter outside
> > the immediate scope of T, this check is performed upon successful
> > return;
>
> The problem is that if a view conversion goes from a (proper)
> descendant of T to a (proper) ancestor of T, then there are checks as
> well.  So it is not just when you convert from T itself.  Conversions
> that "cross" T are also checked.
> That is perhaps what makes para 12 confusing, but it is there for a
> reason.

See the message that I was writing at the same time as this one. I covered that
case.

Note that an important part of the confusion is mentioning the type that we're
converting to: the wording says that it is an "ancestor", and that seems to
combine with the other parts of the wording. But it's definitely the case that
the type we convert to is irrelevant, and shouldn't be mentioned at all, or at
least should simply say "some other type". Part of the problem with the "from"
wording is that it seems to imply a need for "to", which we don't care about
here.

Beyond that, I still stick to my contention that "extensions" are irrelevant for
the reasons for the rule, and we ought to try to mention them as little as
possible. Indeed, I much prefer mentioning them at the end in a "similarly"
clause, rather than confusing everything by sticking them into the main text.

---------

Now for the important part: I think that the semantics described in the existing
rule is wrong, or (more accurately) different for the inherited and explicitly
written routines. It's not crystal clear that this should be fixed (all of these
cases are corner cases to start with), but I wanted to raise the issue.

If we are inheriting a routine from a grandparent, as in:

          type T is tagged private
              with Invariant => InvT;
          procedure P (A : in out T);
          Obj_T : T;

          ...

          type NT is new T ...
             with Invariant => InvNT;
          -- Inherits procedure P (A : in out NT); from T
          Obj_NT : NT;
          ...

          type NNT is new NT ...
             with Invariant => InvNNT;
          -- Inherits procedure P (A : in out NNT); from NT
          Pbj_NNT : NNT;

We agree that a call P(Obj_NT) is translated to P(T(Obj_NT)), and this evaluates
both InvT and InvNT when the routine returns (InvT from the normal rules for the
body, InvNT from the view conversion rule).

I believe that a call P(Obj_NNT) is translated to P(NT(Obj_NNT), which then
(after applying the previous rule) becomes P(T(NT(Obj_NNT))). That means that
such a "doubly inherited call" this evaluates all of InvT, InvNT, InvNNT when
the routine returns (because we have two view conversions here).

This is good because this is the natural implementation; the wrapper for NT's P
would become the called body for the inherited P for NNT.

OTOH, it's likely that if someone wrote this explicitly, they'd write:
P(T(Obj_NNT)).

Given the way 7.3.2(12/3) is written, this is *not* the same thing; only InvT
and InvNNT would be evaluated for this call.

I think it would be better if the semantics included any intervening invariant
(that is, effectively you would make the checks for each intervening derived
types). Then T(Obj_NNT) would be exactly equivalent to T(NT(Obj_NNT)). And as I
noted in my message yesterday, if this is the case, then there is no need to
special case any extensions (you'll pick up any invariants in the walk from the
target type to the source type).

What I don't know is what the intended semantics of a "doubly inherited call"
is. I can't find a compelling reason to insist on evaluating InvNT (in the
example above), so perhaps the intent was that the "middle" invariant not be
evaluated. If so, the semantics are wrong for that case, and we need to revisit
the wording for that reason. (I'd prefer to require it be evaluated, all other
things being equal, but of course they're rarely equal.)

I'll take another crack at improving this wording, but I'd like to know what the
intended semantics are.

> See above.  I do remember struggling with this wording in Edinburgh,
> and almost every word in para. 12 was debated.  So fixing it won't be
> easy without
> losing something.

I think that we lost sight of the big picture in favor of patching up the
bug-de-jour. The general principle is very simple (outside of the package
defining T, check anything that might modify an object of type T), and the case
in question is pretty simple (after changing the result of a view conversion
with source T, make a check of the invariant of T). The only question is whether
intervening types need to be checked, or whether talking about types related to
T is enough.

****************************************************************

From: Jean-Pierre Rosen
Sent: Tuesday, February  7, 2012  7:01 AM

> I think it would be better if the semantics included any intervening
> invariant (that is, effectively you would make the checks for each
> intervening derived types). Then T(Obj_NNT) would be exactly
> equivalent to T(NT(Obj_NNT)). And as I noted in my message yesterday,
> if this is the case, then there is no need to special case any
> extensions (you'll pick up any invariants in the walk from the target type to the source type).
>
> What I don't know is what the intended semantics of a "doubly
> inherited call" is. I can't find a compelling reason to insist on
> evaluating InvNT (in the example above), so perhaps the intent was
> that the "middle" invariant not be evaluated.

I fully agree with you (that InvNT should be evaluated). Remember that in OO
reasoning, an NNT "is a" NT (which "is a" T). Therefore, any invariant for NT
should hold for NNT.

Imagine that the additional components added by NT depend on the components of
T. If the invariants for NT are not evaluated, you could create an object whose
NT part does not obey its invariant.

****************************************************************

From: Tucker Taft
Sent: Tuesday, February  7, 2012  8:46 AM

One issue that I just thought of has to do with view conversions from a
class-wide type to an ancestor's specific type.  If you assign to such a view
conversion, it is not clear at compile-time how many type invariants you will
need to check.  I fear this means creating a type-invariant-checking implicit
dispatching operation.  Yuck.  For example:

   type T is ... private ...
      with Type_Invariant => Valid(T);

   type NT is new T with private
      with Type_Invariant => NT_Valid(NT);

   type NNT is new NT with private
      with Type_Invariant => NNT_Valid(NNT);


   X : T'Class := ...

   T(X) := ...
     -- How many type-invariant checks need to be performed?

Nasty...

****************************************************************

From: Bob Duff
Sent: Tuesday, February  7, 2012  9:24 AM

> ...I fear this
> means creating a type-invariant-checking implicit dispatching
> operation.  Yuck.

Doesn't seem SO horrible.  I mean, relative to some other implemetation horrors
I can think of.

****************************************************************

From: Tucker Taft
Sent: Tuesday, February  7, 2012  9:57 AM

True, but it was totally unexpected as far as I was concerned.

I guess what the compiler will need to do is create an implicit dispatching
operation which will take two parameters, an object and a level, and check the
type invariant on the object, and if the level implies it, call the
corresponding type-invariant-checking routine of its parent type.  The level
would indicate the "extension level" of the target type of the view conversion.

Or I suppose it might want to call its parent type's type-invariant checker
first if the level number indicates it is appropriate, and then if that passed
(or was bypassed), check its own.

Not that hard to do but annoying to have to create yet another implicit
dispatching operation for the oddball case involving class-wide objects.

****************************************************************

From: Randy Brukardt
Sent: Friday, February 10, 2012  2:07 AM

> I guess what the compiler will need to do is create an implicit
> dispatching operation which will take two parameters, an object and a
> level, and check the type invariant on the object, and if the level
> implies it, call the corresponding type-invariant-checking routine of
> its parent type.  The level would indicate the "extension level"
> of the target type of the view conversion.

This seems more complicated than necessary. Here's how I described this for the
AARM:

  For view conversions involving class-wide types, the exact checks needed may
  not be known at compile-time. One way to deal with this is to have an implicit
  dispatching operation that is given the object to check and the tag of the
  target of the conversion, and which first checks if the passed tag is not for
  itself, and if not, checks the its invariant on the object and then calls
  the operation of its parent type. If the tag is for itself, the operation is complete.

This tag comparison is the same as (the much more common) one needed for
checking type conversions to descendant class-wide types for inclusion. And each
such routine only makes a single check for each type, it doesn't try to pile all
of them up, or invent a "extension level". If we have to have a dispatching
routine, we might as well leverage that.

(BTW, I don't find this that unusual. I think we have more than 10 such routines
already, what's one more??)

****************************************************************

From: Tucker Taft
Sent: Tuesday, February  7, 2012  1:09 PM

...
> I think it would be better if the semantics included any intervening
> invariant (that is, effectively you would make the checks for each
> intervening derived types). Then T(Obj_NNT) would be exactly
> equivalent to T(NT(Obj_NNT)). And as I noted in my message yesterday,
> if this is the case, then there is no need to special case any
> extensions (you'll pick up any invariants in the walk from the target type to the source type).

This could also be fixed by eliminating the mention of record extensions vs.
private extensions in para 12 (which you have been recommending), and require
the invariant checks on all types that are "crossed" by a view conversion be
checked:

    After assigning to a view conversion, outside the immediate scope of
    T, that converts from [T or one or more record extensions (and no
    private extensions) of T] {a descendant of T (including T itself)} to
    an ancestor of type T {(other than T itself)}, a check is performed
    on the part of the object that is of type T; similarly, for passing a
    view conversion as an out or in out parameter outside the immediate
    scope of T, this check is performed upon successful return;

> What I don't know is what the intended semantics of a "doubly
> inherited call" is. I can't find a compelling reason to insist on
> evaluating InvNT (in the example above), so perhaps the intent was
> that the "middle" invariant not be evaluated. If so, the semantics are
> wrong for that case, and we need to revisit the wording for that
> reason. (I'd prefer to require it be evaluated, all other things being
> equal, but of course they're rarely equal.)...

It seems that the intermediate invariant should be re-checked, since if you
change the ancestor part, then you could easily invalidate invariants of every
descendant.

****************************************************************

From: Randy Brukardt
Sent: Wednesday, February  8, 2012 10:25 PM

> This could also be fixed by eliminating the mention of record
> extensions vs. private extensions in para 12 (which you have been
> recommending), and require the invariant checks on all types that are
> "crossed" by a view conversion be checked:
>
>     After assigning to a view conversion, outside the immediate scope of
>     T, that converts from [T or one or more record extensions (and no
>     private extensions) of T] {a descendant of T (including T itself)} to
>     an ancestor of type T {(other than T itself)}, a check is performed
>     on the part of the object that is of type T; similarly, for passing a
>     view conversion as an out or in out parameter outside the immediate
>     scope of T, this check is performed upon successful return;

Ah, this is what I trying to get to on Sunday. As usual, your wording is better
than mine. I'll write up the change this way (replacing last week's work).

I still wonder if the second branch (the in out case) is a bit too vague; it
never says that it is only talking about view conversions that meet the
conversion rules of the previous branch. That's kind of important, and it's easy
to read it that way because the part about being outside of the scope is
repeated, but not the type part.

Perhaps it would be better to repeat the entire thing and use bullets for the
non-repeated part:

For a view conversion, outside the immediate scope of T, that converts from a descendant of T
(including T itself) to an ancestor of type T {(other than T itself), a check is performed on the
part of the object that is of type T:
   * after assigning to the view conversion; and
   * after successful return from a call that passes the view conversion as out or in out parameter.

Now there is no confusion about which cases are included (no vague similarly),
and there's almost no duplication of wording.

I think this is a big improvement, and is great. :-) What about the rest of
you??

P.S. I think either of these wordings would benefit from an AARM note that
explains that a single view conversion could trigger this rule for multiple
types and thus cause multiple invariant checks.


****************************************************************

From: Tullio Vardanega
Sent: Thursday, February  9, 2012  2:24 AM

The latest formulation is becoming digestible even to the likes of me.
Perhaps this counts as an indication of convergence ;-)

****************************************************************