!standard 6.1.1(7/4)                                    16-07-21  AI12-0185-1/02
!standard 6.1.1(8/3)
!standard 6.1.1(26.10/4)
!standard 6.1.1(29/3)
!class binding interpretation 16-04-20
!status Amendment 1-2012 16-07-21
!status WG9 Approved 16-10-08
!status ARG Approved 11-0-0  16-06-11
!status work item 16-04-20
!status received 16-01-28
!priority Low
!difficulty Easy
!qualifier Error
!subject Resolution of postcondition-specific attributes 
!summary

We confirm that the type of S'Result was changed in some cases by
the Corrigendum (via AI12-0113-1); wording that says it wasn't is wrong.

We also remove excess wording defining the resolution of the Old attribute.

!question

(1) 6.1.1(7/4) says that the type of S'Result in a Post'Class expression
when S has a controlling result is the nominal subtype NT. 6.1.1(29/3) 
says that the type of S'Result in a Post'Class expression
when S has a controlling result is the T'Class. It is unlikely that any
entity in Ada can have two different types at the same time, so which
rule is correct? (6.1.1(7/4)).

(2) 6.1.1(8/3) (a Name Resolution Rule) says:

For an attribute_reference with attribute_designator Old, if the attribute
reference has an expected type or shall resolve to a given type, the same
applies to the prefix; otherwise, the prefix shall be resolved independently
of context.

6.1.1(26.10/4) (a Static Semantics rule, part of the definition of the Old
attribute) says:

The nominal subtype of X'Old is as implied by the above definitions. The
expected type of the prefix of an Old attribute is that of the attribute.
Similarly, if an Old attribute shall resolve to be of some type, then the
prefix of the attribute shall resolve to be of that type.

We've essentially the same rule in two places; in addition, neither rule is
quite complete. The first rule doesn't define the type of the attribute;
the second rule doesn't define the resolution in the case where the context
allows any type (as in a type conversion).

Should these rules be reconciled? (Yes.)

!recommendation

(See Summary.)

!wording

Modify 6.1.1(26.10/4):

The {type and }nominal subtype of X'Old is as implied by the above
definitions.[ The expected type of the prefix of an Old attribute is that
of the attribute. Similarly, if an Old attribute shall resolve to be of some
type, then the prefix of the attribute shall resolve to be of that type.]

Modify 6.1.1(29/3):

Within a postcondition expression for function F, denotes the result object
of the function. The type of this attribute is that of the function result
except within a Post'Class postcondition expression for a function with a
controlling result or with a controlling access result{; in those cases the
type of the attribute was described previously}.[ For a controlling result,
the type of the attribute is T'Class, where T is the function result type. For
a controlling access result, the type of the attribute is an anonymous
access type whose designated type is T'Class, where T is the designated
type of the function result type.]

!discussion

For (1), since the rules in 6.1.1(7/4) were revised more recently than those
in 6.1.1(29/3), it seems that the revision failed to update 6.1.1(29/3).

For this problem, we just redo the wording to refer to the previous rules.
Given the complexity of 6.1.1(7/4), it would be madness to repeat the rule
in 6.1.1(29/3) -- it inevitably would end up subtly different.

An alternative we considered would be to put the entire definition of the
type of attribute into the Name Resolution part of this text. To do that,
we'd add a new paragraph after 6.1.1(7/4):

Unless the attribute Result occurs within a Post'Class postcondition
expression for a function with a controlling result or with a controlling
access result, the type of the attribute Result is that of the function
result.

AARM Note: The "unless" cases are defined by the paragraph preceding this
one.

This would be more consistent with 'Old; but we'd then have the odd effect
of not defining the type of the attribute within the attribute definition
itself. Since it is not clearly better, we just make the minimum change.


For (2), we just delete the (newer) redundant text. We considered moving
the type of the attribute to the 6.1.1(8/3), but just saying that the
type of the attribute is that of the prefix is not accurate for an anonymous
access object (the attribute has a different, structurally equivalent type).

We could have deleted 6.1.1(8/3) and moved the rest of its text into
6.1.1(26.10/4), but that larger change doesn't improve the wording, and in
any case, some part of the resolution will always be in 6.1.1(7/4).

!corrigendum 6.1.1(26.10/4)

@drepl
@xindent<The nominal subtype of X'Old is as implied by the above definitions. The
expected type of the prefix of an Old attribute is that of the attribute.
Similarly, if an Old attribute shall resolve to be of some type, then
the prefix of the attribute shall resolve to be of that type.>
@dby
@xindent<The type and nominal subtype of X'Old is as implied by the above
definitions.>

!corrigendum 6.1.1(29/4)

@drepl
@xhang<@xterm<F'Result>Within
   a postcondition expression for function F, denotes
   the result object of the function. The type of this attribute is that
   of the function result except within a Post'Class postcondition
   expression for a function with a controlling result or with a
   controlling access result. For a controlling result, the type of the
   attribute is @i<T>'Class, where @i<T> is the function result type. For a
   controlling access result, the type of the attribute is an anonymous
   access type whose designated type is @i<T>'Class, where @i<T> is the
   designated type of the function result type.>
@dby
@xhang<@xterm<F'Result>Within
   a postcondition expression for function F, denotes
   the result object of the function. The type of this attribute is that
   of the function result except within a Post'Class postcondition
   expression for a function with a controlling result or with a
   controlling access result; in those cases the type of the attribute was
   described previously.>

!ASIS

No ASIS effect.

!ACATS test


!appendix

From: Randy Brukardt
Sent: Thursday, January 28, 2016  7:28 PM

6.1.1(8/3) (a Name Resolution Rule) says:

For an attribute_reference with attribute_designator Old, if the attribute
reference has an expected type or shall resolve to a given type, the same
applies to the prefix; otherwise, the prefix shall be resolved independently
of context.

6.1.1(26.10/4) (a Static Semantics rule, part of the definition of the Old
attribute) says:

The nominal subtype of X'Old is as implied by the above definitions. The
expected type of the prefix of an Old attribute is that of the attribute.
Similarly, if an Old attribute shall resolve to be of some type, then the
prefix of the attribute shall resolve to be of that type.

What is this, the Department of Redundancy Department?? What the heck
possessed us to add the last two sentences of paragraph 26.10 in AI12-0032-1??

Normally, attribute definitions are self-contained, so in some ways, the 26.10
definition makes more sense. But looking at these side-by-side, it's clear
that neither is complete by itself. Paragraph 8 doesn't ever give the type of
the attribute. Paragraph 26.10 doesn't define the resolution if the attribute
is in a context where any type is allowed (as the operand of a type
conversion, for instance).

If we had wanted to move the resolution stuff to the attribute definition
(definitely a defensible idea), we ought to have done that! Not just add 60%
of it and then leave the original behind.

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

From: Randy Brukardt
Sent: Friday, January 29, 2016  5:45 PM

The second through fourth sentences of 6.1.1(29/3) say:

The type of this attribute is that of the function result except within a
Post'Class postcondition expression for a function with a controlling result
or with a controlling access result. For a controlling result, the type of
the attribute is T'Class, where T is the function result type. For a
controlling access result, the type of the attribute is an anonymous access
type whose designated type is T'Class, where T is the designated type of the
function result type.

I wonder if this is right. We've changed the definition of the types within
a class-wide postcondition to be a notional generic formal NT (6.1.1(7/4),
AI12-0113-1), from T'Class. Shouldn't F'Result have this notional type NT?
We don't want F'Result to force dynamic binding in an expression that
otherwise would be statically bound:

    function F (Obj : T) return T 
        with Post'Class => Is_Foo(F'Result) and -- Always dynamically bound
                           Is_Foo(Obj)          -- Might be statically or
dynamically bound

Indeed, 6.1.1(7/4) includes a mention of S'Result:

Within the expression for a Pre'Class or Post'Class aspect for a primitive
subprogram S of a tagged type T, a name that denotes a formal parameter (or
S'Result) of type T is interpreted as though it had a (notional) type NT
that is a formal derived type whose ancestor type is T, with directly
visible primitive operations.

So 6.1.1(7/4) and 6.1.1(29/3) give different types for S'Result in this
case!!

Probably we ought to replace 6.1.1(29/3) with something like: (probably
combine this with the fix for the duplicated resolution wording)

The type of this attribute is that of the function result except within a
Post'Class postcondition expression for a function with a controlling result
or with a controlling access result; in those cases the type of the
attribute is described above.

[We can't use paragraph numbers in normative wording, else we could be more
specific.]

Or may "...was described previously"??

I don't want to duplicate the wording that's in 6.1.1(7/4); undoubtedly it
would end up subtly different.

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

From: Steve Baird
Sent: Friday, January 29, 2016  8:11 PM

If the result type of a function is a specific tagged type, the tag of 
the return object is that of the result type (this is different
than the situation with parameters).

So it seems like dynamic or static binding take you to the same place
if F'Result is the controlling operand and so dispatching to the wrong
body is not a problem.

There may be a different problem with something like
     Is_Salubrious (F'Result, Obj)
where we have a requirement that the two controlling operands have to
agree about whether they are statically or dynamically tagged.

In particular, suppose we use "=" as our two-controlling-operands
function.

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

From: Randy Brukardt
Sent: Friday, January 29, 2016  8:35 PM

...
> So it seems like dynamic or static binding take you to the same place 
> if F'Result is the controlling operand and so dispatching to the wrong 
> body is not a problem.

I suppose...

> There may be a different problem with something like
>      Is_Salubrious (F'Result, Obj)
> where we have a requirement that the two controlling operands have to 
> agree about whether they are statically or dynamically tagged.
> 
> In particular, suppose we use "=" as our two-controlling-operands 
> function.

Right,
     F'Result = Obj
would be illegal if F'Result has T'Class and Obj has NT, because of mixed
dynamic and static tags.

But I think it is more important that 6.1.1(7/4) says explicitly that the
type of S'Result with a controlling result has type NT in a class-wide
precondition, and 6.1.1(29/3) says it has T'Class. "Two men say they're
Jesus, one of them must be wrong." - Industrial Disease, Dire Straits

I would have concentrated on that had I seen it when I wrote the first 2/3rds
of that message.

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

From: Randy Brukardt
Sent: Thursday, January 28, 2016  7:28 PM

6.1.1(8/3) (a Name Resolution Rule) says:

For an attribute_reference with attribute_designator Old, if the attribute
reference has an expected type or shall resolve to a given type, the same
applies to the prefix; otherwise, the prefix shall be resolved independently
of context.

6.1.1(26.10/4) (a Static Semantics rule, part of the definition of the Old
attribute) says:

The nominal subtype of X'Old is as implied by the above definitions. The
expected type of the prefix of an Old attribute is that of the attribute.
Similarly, if an Old attribute shall resolve to be of some type, then the
prefix of the attribute shall resolve to be of that type.

What is this, the Department of Redundancy Department?? What the heck
possessed us to add the last two sentences of paragraph 26.10 in AI12-0032-1??

Normally, attribute definitions are self-contained, so in some ways, the 26.10
definition makes more sense. But looking at these side-by-side, it's clear
that neither is complete by itself. Paragraph 8 doesn't ever give the type of
the attribute. Paragraph 26.10 doesn't define the resolution if the attribute
is in a context where any type is allowed (as the operand of a type
conversion, for instance).

If we had wanted to move the resolution stuff to the attribute definition
(definitely a defensible idea), we ought to have done that! Not just add 60%
of it and then leave the original behind.

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