Version 1.5 of ai12s/ai12-0068-1.txt

Unformatted version of ai12s/ai12-0068-1.txt version 1.5
Other versions for file ai12s/ai12-0068-1.txt

!standard 3.10.2(7/3)          14-07-22 AI12-0068-1/02
!class binding interpretation 13-05-30
!status Corrigendum 2015 14-07-22
!status ARG Approved 2-0-6 14-06-28
!status work item 13-05-30
!status received 13-04-20
!priority Medium
!difficulty Medium
!qualifier Omission
!subject Predicates and the current instance of a subtype
!summary
The current instance of a subtype acts like a value of the type, not as an object.
!question
For a predicate, is the current instance of the subtype an object or a value? This matters in unusual cases. Consider:
type T (Kind : T_Kind := Zoofle) is ... ;
-- A variable is in this subtype if and only if it -- is ok to assign it a value whose Kind is Zoofle subtype Zoofleable is T with Dynamic_Predicate => Zoofleable.Kind = Zoofle or else not Zoofleable'Constrained;
procedure Zoofalize (X : out Zoofleable) is begin X := (Kind => Zoofle, ...); -- Assignment's discriminant check guaranteed to pass end;
Y : T := (Foozle, ...); -- unconstrained, Kind /= Zoofle Z : T (Foozle) := Y; -- constrained, Kind /= Zoofle
begin Zoofalize (Y); -- Works Zoofalize (Z); -- Fails predicate check (??)
Is it expected that the value of 'Constrained reflects that of the actual object, or is this check on a value and the properties of the object aren't querable? (Something. :-)
In a related question, is the nominal subtype of the current instance of a type or subtype defined? This matters in case expressions. Given this example,
subtype S is Natural with Dynamic_Predicate => (case S is ...
is coverage of the negative values required or forbidden? (Forbidden.)
!recommendation
(See !summary.)
!wording
Add after RM 8.6(17/3):
Within an aspect_specification for a type or subtype, the current instance represents a value of the type; it is not an object. The nominal subtype of this value is given by the subtype itself (the first subtype in the case of a type_declaration), prior to applying any predicate specified directly on the type or subtype. If the type or subtype is by-reference, the associated object with the value is the object associated (see 6.2) with the execution of the usage name.
AARM Ramification: For the purposes of Legality Rules, the current instance acts as a value within an aspect_specification. It might really be an object (and has to be for a by-reference type), but that isn't discoverable by direct use of the name of the current instance.
!discussion
Note that at the moment, a current instance of a type and a subtype is a variable, since it is not in the list of things that denote constant views in 3.3. That list is supposed to be exhaustive (and we keep adding to it as things are missed). Moreover, it is clear that it is a variable by practice, as the Rosen trick depends on that fact:
type Outer; type Inner (Ref : access Outer) is limited null record;
-- discriminant's type is access-to-variable
type Outer is limited record Self : Inner (Outer'access); end record;
This would not be legal if Outer was a constant view (as converting an access-to-constant value to an access-to-variable value is illegal).
---
We considered the model that the current instance of a subtype acts like an in-mode parameter for the purposes of use in a predicate definition. This is the most information that a predicate should be allowed to use, as we want to allow compilers to implement a predicate as a Boolean function with a parameter of the base type of the subtype.
But we chose to treat it as a constant value. By choosing this model, even using object attributes within a predicate are illegal. For instance, 'Size, 'Alignment, 'Access, and 'Address are all illegal as their prefix does not denote an object.
!corrigendum 8.6(17/3)
Insert after the paragraph:
the new paragraph:
Within an aspect_specification for a type or subtype, the current instance represents a value of the type; it is not an object. The nominal subtype of this value is given by the subtype itself (the first subtype in the case of a type_declaration), prior to applying any predicate specified directly on the type or subtype. If the type or subtype is by-reference, the associated object with the value is the object associated (see 6.2) with the execution of the usage name.
!ACATS Test
The examples discussed in the mail (see !appendix) should be made into ACATS tests (some will be legality rules and some will be determinable at runtime).
!ASIS
No ASIS effect.
!appendix

From: Steve Baird
Sent: Saturday, April 20, 2013  4:54 PM

Randy and I were discussing whether predicates really work on values or on
objects.

The manual is not clear on this point:
   the current instance of a type is the object or value of
   the type that is associated with the execution that
   evaluates the usage name.

The following example illustrates the difference:

     type T (Kind : T_Kind := Zoofle) is ... ;

     -- A variable is in this subtype if and only if it
     -- is ok to assign it a value whose Kind is Zoofle
     --
     subtype Zoofleable is T with
       Dynamic_Predicate =>
         Zoofleable.Kind = Zoofle
         or else not Zoofleable'Constrained;

     procedure Zoofalize (X : out Zoofleable) is
     begin
         X := (Kind => Zoofle, ...);
         -- assignment's discrim check guaranteed to pass
     end;

     Y : T := (Foozle, ...); -- unconstrained, Kind /= Zoofle
     Z : T (Foozle) := Y; -- constrained, Kind /= Zoofle
   begin
     Zoofalize (Y); -- works
     Zoofalize (Z); -- fails predicate check

Is this supposed to work as the comments suggest (because the current instance
is the object), or should the use of Zoofleable'Constrained always return False
(because the current instance is a value)?

Randy suggests a more nuanced approach: a name denoting the current instance in
a predicate should behave as though it denotes an in-mode parameter where the
corresponding actual parameter is the current instance of the type.

This means that attributes such as Size, Address, and Alignment can be queried,
but they might not yield useful results in some cases.
Current_Instance'Constrained would then always yield True. This model also works
well with by-reference types. And like any equivalence rule, it has the
advantage of providing a clear implementation model.

Sounds right to me; this is probably how a predicate would be implemented anyway
so this model is probably consistent with existing practice.

However, note the use of "in-mode" above.

The current instance of a type is variable, not constant.

This is at the heart of the well established "Rosen trick", which allows
modification of a limited constant via a self-referential access-to-variable
discriminant.

A strict reading of the current wording
would allow the following (absurd) example:

      X : constant Integer := 123;

      function Is_456 (Y : out Integer) return Boolean is
      begin
         Y := 456; -- even if it wasn't 456 before, it is now
         return True;
      end;

      subtype S is Integer with Dynamic_Predicate =>
        Is_456 (S); -- should be illegal, but is legal because
                    -- name "S" denotes a variable

      pragma Assert (X = 123 and then (X in S) and then X = 456);

Do not waste your time trying to figure out what this ought to do at runtime; it
should be rejected at compile time. This is just a minor language hole that
needs to be plugged.

I think we need wording something like

    In an aspect specification for a type or subtype, a name
    denoting the current instance of the type or subtype denotes
    a constant view.

It seems to me that
    1) Randy's "treat the current instance like a parameter"
       model is right.
    2) The mode of that parameter needs to be In in the case of
       an aspect specification.

Do folks agree with these general ideas?

Wording, of course, is a separate question.

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

From: Tucker Taft
Sent: Saturday, April 20, 2013  8:50 PM

> ... It seems to me that
>     1) Randy's "treat the current instance like a parameter"
>        model is right.
>     2) The mode of that parameter needs to be In in the case of
>        an aspect specification.
>
> Do folks agree with these general ideas?

Yes.

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

From: Jean-Pierre Rosen
Sent: Sunday, April 21, 2013  4:26 AM

>     Zoofalize (Y); -- works
>     Zoofalize (Z); -- fails predicate check

At first, I had some sympathy with this. However, I think a precondition is more
appropriate for someone who wants to express that. And we don't have the same
problem in preconditions, have we?

[...]
> Randy suggests a more nuanced approach: a name denoting the current
> instance in a predicate should behave as though it denotes an in-mode
> parameter where the corresponding actual parameter is the current
> instance of the type.
>
> This means that attributes such as Size, Address, and Alignment can be
> queried, but they might not yield useful results in some cases.
> Current_Instance'Constrained would then always yield True. This model
> also works well with by-reference types. And like any equivalence
> rule, it has the advantage of providing a clear implementation model.
>
> Sounds right to me; this is probably how a predicate would be
> implemented anyway so this model is probably consistent with existing
> practice.
>
> However, note the use of "in-mode" above.
>
> The current instance of a type is variable, not constant.

You lost me here. Is the sentence above about the current wording, or the new
one? AFAIK, an in-parameter is a constant view.

> This is at the heart of the well established "Rosen trick", which
> allows modification of a limited constant via a self-referential
> access-to-variable discriminant.

I'd rather say that it is a constant view that carries an access to a variable
view of the same object.

> I think we need wording something like
>
>    In an aspect specification for a type or subtype, a name
>    denoting the current instance of the type or subtype denotes
>    a constant view.
>
> It seems to me that
>    1) Randy's "treat the current instance like a parameter"
>       model is right.
>    2) The mode of that parameter needs to be In in the case of
>       an aspect specification.

Are you proposing to say that it "denotes a constant view", or "it is an
in-parameter", or is it really equivalent?

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

From: Steve Baird
Sent: Monday, April 22, 2013  1:29 PM

...
>>      Zoofalize (Y); -- works
>>      Zoofalize (Z); -- fails predicate check
> At first, I had some sympathy with this. However, I think a
> precondition is more appropriate for someone who wants to express
> that. And we don't have the same problem in preconditions, have we?

Right, because preconditions don't use the "current instance"
mechanism.

>> The current instance of a type is variable, not constant.
>
> You lost me here. Is the sentence above about the current wording, or
> the new one? AFAIK, an in-parameter is a constant view.

The above sentence is about the current wording (or really about the
well-established interpretation of the RM's lack of explicit wording about the
constancy of the current instance of a type).

If this were not the case, then this example would be illegal:

     type Outer;
     type Inner (Ref : access Outer) is limited null record;
       -- discriminant's type is access-to-variable

     type Outer is limited record
       Self : Inner (Outer'Access);
     end record;

> I'd rather say that it is a constant view that carries an access to a
> variable view of the same object.

Maybe it should work that way and that is a good way to think about it.
Strictly speaking, however, I think you are mistaken.

I think the current language definition allows, for example, passing the current
instance of a type as an out-mode actual parameter in default initialization
expression for a component (not something that I would recommend. although I
don't see that this introduces any definitional problems). One could argue that
the language should be changed to prevent this. Alternatively, one could argue
that disallowing something which is useless but well defined and unlikely to
occur accidentally is not worth the bother.

Note that we still have problems in this area even if the current instance
denotes a constant view. Given

     type T is
        record
           F, G : Component_Type := Some_Func (T);
        end record;

one of those two calls (whichever is evaluated first) is going to be passed a
value with an uninitialized component. Note that Component_Type could be an
access type, a task type, or anything.

>> I think we need wording something like
>>
>>     In an aspect specification for a type or subtype, a name
>>     denoting the current instance of the type or subtype denotes
>>     a constant view.
>>
>> It seems to me that
>>     1) Randy's "treat the current instance like a parameter"
>>        model is right.
>>     2) The mode of that parameter needs to be In in the case of
>>        an aspect specification.
>
> Are you proposing to say that it "denotes a constant view", or "it is
> an in-parameter", or is it really equivalent?

Constant view and in-parameter are not equivalent because of things like 'Size
and 'Alignment. Consider the current instance of a type T when declaring X of
type T where X'Alignment /= T'Alignment. What is Current_Instance'Allignment? If
we require it to be X'Alignment, then we are imposing distributed overhead on
any implementation which wants to use the reasonable implementation strategy of
implementing predicates via a compiler-generated boolean-valued function. Let's
not do that.

I didn't propose wording for the "it behaves like a parameter" approach.
The wording we end up with to get constancy right might depend on how that goes.

One possibility is that we define the "it behaves like a parameter" rule without
reference to the mode of the parameter; in that case we might need something
like the wording I proposed.

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

From: Steve Baird
Sent: Friday, November 22, 2013  5:08 PM

Is the nominal subtype of the current instance of a type or subtype defined
anywhere? It certainly is not defined in 8.6(17/3).

See AI05-0006 for an explanation of why anyone would care.

I noticed this in the context of ignored subtype predicates.

Randy - do I get Brownie points for sending this as
  a separate message?

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

From: Randy Brukardt
Sent: Friday, November 22, 2013  6:54 PM

...
> Randy - do I get Brownie points for sending this as
>   a separate message?

Yes, you get 2 Brownie points for this. Of course, you need 1000 Brownie points
in order to be able to redeem them for an official ARG keychain. ;-)

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

From: Steve Baird
Sent: Friday, November 22, 2013  6:11 PM

> See AI05-0006 for an explanation of why anyone would care.
The short explanation is "case expressions".

Given this example,

    subtype S is Natural with Dynamic_Predicate => (case S is ...

is coverage of the negative values required or forbidden?

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

From: Robert Dewar
Sent: Friday, November 22, 2013  6:22 PM

> Given this example,
>
>      subtype S is Natural with Dynamic_Predicate => (case S is ...
>
> is coverage of the negative values required or forbidden?

I would say required ... you certainly can't have the case statement assuming
that S is in Natural range, that would be non-conforming (erreoneousness arising
from bounded error)

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

From: Tucker Taft
Sent: Friday, November 22, 2013  6:43 PM

I'm not sure I agree.  The subtype constraints are evaluated *before* the
dynamic predicate (according to the new AI), so by the time you get to the case
expression, it would be annoying to have to worry about values that didn't
satisfy the constraints (presuming they are static).

I guess to me the "obvious" ;-) answer is that the nominal subtype is the
subtype before applying the predicate.

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

From: Steve Baird
Sent: Friday, November 22, 2013  6:52 PM

That was my thinking too.

Is there agreement that the current RM wording doesn't provide an answer for
this question (because the nominal subtype of the current instance of a subtype
is never defined)?

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

From: Randy Brukardt
Sent: Friday, November 22, 2013  6:53 PM

> > Given this example,
> >
> >      subtype S is Natural with Dynamic_Predicate => (case S is ...
> >
> > is coverage of the negative values required or forbidden?
>
> I would say required ... you certainly can't have the case statement
> assuming that S is in Natural range, that would be non-conforming
> (erreoneousness arising from bounded error)

Not sure why you would say that. AI12-0071-1 requires that the constraint check
be made first before evaluating the predicate, so no value out of the range of
Natural should ever be presented to the predicate. Moreover, if the check is
suppressed, then the code is erroneous for failing a suppressed check, so we
don't need to protect against that, either. Finally, case statements and
expressions require a test that the value is in the base type (this is not a
check, it can't be suppressed). So I don't think there is any semantic need for
the base range be covered.

Having said that, we might still prefer such a model as it is simpler than
basing it on the subtype_mark given in the subtype_declaration (this thing
unfortunately does not have an official name and it is always awkward to refer
to it in formal wording).

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

From: Randy Brukardt
Sent: Friday, November 22, 2013  6:58 PM

> Is the nominal subtype of the current instance of a type or subtype
> defined anywhere? It certainly is not defined in 8.6(17/3).

BTW, I'd recommend that this get added to AI12-0068-1, which is supposed to
define the meaning of the current instance of a subtype. We might as well get
the nominal subtype defined at the same time (given that the entire concept
isn't defined in the currrent RM, the subtype is just a tiny corner).

Mr. Taft has that AI assigned to him and he didn't get to it for the recent
meeting. So he should add this topic to his homework.

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

From: Randy Brukardt
Sent: Friday, November 22, 2013  7:00 PM

...
> Is there agreement that the current RM wording doesn't provide an
> answer for this question (because the nominal subtype of the current
> instance of a subtype is never defined)?

Since the current instance of a subtype is not defined by the current RM wording
(remember AI12-0068-1?), I think it is pretty likely that the nominal subtype of
it isn't defined, either. :-)

The nominal subtype of a current instance of a type probably isn't defined,
either; that probably ought to be the base type of the type. (Although I don't
think that one can use that current instance in a way where it would matter.)

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

From: Robert Dewar
Sent: Friday, November 22, 2013  7:19 PM

> Is there agreement that the current RM wording doesn't provide an
> answer for this question (because the nominal subtype of the current
> instance of a subtype is never defined)?

Well it's sort of obvious what the nominal subtype is, even if not formally
defined, any other choice would be absurd, and we are not allowed absurd
conclusions, so by the Sherlock Holmes rule the NS *is* defined, and indeed I
agree, negative values need not be covered (but must in the general case be
checked for!)

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

From: Steve Baird
Sent: Friday, November 22, 2013  7:47 PM

> The nominal subtype of a current instance of a type probably isn't
> defined, either; that probably ought to be the base type of the type.

Even that isn't obvious in the case of a derived type.

Or a type like
    type T is range 1 .. 10 with Dynamic_Predicate => (case T ...

(although there is a derived type hiding in there somewhere, so perhaps this
isn't really a different case).

> BTW, I'd recommend that this get added to AI12-0068-1

Good point. I had forgotten about this AI and I agree that this issue should be
addressed there.

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

From: Geert Bosch
Sent: Friday, November 22, 2013  10:36 PM

> I'm not sure I agree.  The subtype constraints are evaluated *before* the
> dynamic predicate (according to the new AI), so by the time you get to the case
> expression, it would be annoying to have to worry about values that didn't
> satisfy the constraints (presuming they are static).
>
> I guess to me the "obvious" ;-) answer is that the nominal subtype is the
> subtype before applying the predicate.

Right. We'd always be free to check the subtype first.

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

From: Steve Baird
Sent: Monday, November 25, 2013  1:20 PM

I think it is important that AI12-0071 (which, to be sure, hasn't been approved
yet) says that checking the other stuff before evaluating the  predicate is
required, not just allowed.

Without AI12-0071 (i.e., if this order was allowed but not
required) my opinion on this nominal subtype question would be different.

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

From: Tucker Taft
Sent: Monday, November 25, 2013  8:36 PM

> I think it is important that AI12-0071 (which, to be sure, hasn't been
> approved yet) says that checking the other stuff before evaluating the
> predicate is required, not just allowed.

That is what it says now (or at least that was my intent).

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

Questions? Ask the ACAA Technical Agent