Version 1.5 of ai05s/ai05-0183-1.txt

Unformatted version of ai05s/ai05-0183-1.txt version 1.5
Other versions for file ai05s/ai05-0183-1.txt

!standard 3.2.1(2) 10-04-27 AI05-0183-1/03
!standard 3.2.2(2)
!standard 3.3.1(2/2)
!standard 3.8(6)
!standard 3.9.3(1.1/2)
!standard 6.1(2/2)
!standard 6.7(2/2)
!standard 9.5.2(2/2)
!standard 7.1(3)
!standard 7.3(2)
!standard 7.3(3)
!standard 9.1(2/2)
!standard 9.1(3/2)
!standard 9.4(2/2)
!standard 9.4(3/2)
!standard 9.5.2(2/2)
!standard 12.1(3)
!standard 12.4(2/3)
!standard 12.5(2)
!standard 12.6(2.1-2.2/2)
!standard 12.7(2)
!standard 13.1(0.1/2)
!standard 13.3.1(0)
!class amendment 09-11-01
!status work item 09-11-01
!status received 09-11-01
!priority Medium
!difficulty Medium
!subject Aspect Specifications

!summary

To support the specification of pre- and postconditions, as well as invariants on types and object, we propose a general notation for specifying "aspects" of an entity as part of its declaration, rather than with a separate aspect clause.

!problem

There is a desire to be able to specify "aspects" of subprograms such as pre- and postconditions. Unfortunately, specifying aspects for subprograms using a pragma or an attribute_definition_clause is generally awkward in Ada, because subprograms can be overloaded. Having to insert a local renaming simply to provide a unique name is verbose, and at least in some cases, the aspect to be specified belongs in close proximity with the declaration. More generally, specifying attributes or other aspects of an entity with a separate clause or pragma is not always desirable, as the aspect may be integral to the appropriate use of the entity.

!proposal

We propose to allow certain aspects of an entity to be specified as part of the declaration of the entity, using an aspect_specification that is placed immediately in front of the semicolon ending the declaration:

aspect_specification ::= with aspect_mark [=> expression] {, aspect_mark [=> expression] }

The aspect_specification is an optional element in the following kinds of declarations:

* object_declaration;

* full_type_declaration;

* subtype_declaration;

* component_declaration;

* subprogram_declaration;

* abstract_subprogram_declaration;

* null_procedure_declaration;

* package_declaration;

* private_type_declaration;

* private_extension_declaration;

* task_type_declaration;

* single_task_declaration;

* protected_type_declaration;

* single_protected_declaration;

* entry_declaration;

* generic_declaration;

* generic_formal_parameter_declaration.

[What about renaming declarations?]

At most one occurrence of each aspect is allowed within a single aspect_specification. The named aspect must be an aspect that can be specified for the given kind of entity.

The names in the expressions of an aspect_specification are resolved not at the point of the associated declaration, but rather at the freezing point of the associated entity. If the aspect_specification occurs within a visible part, declarations occuring after the freezing point or within the corresponding private part are not considered.

The expression may be omitted only when the aspect is of a boolean type, in which case it is equivalent to being specified as True.

!wording

Replace 3.2.1(2) by:

full_type_declaration ::= type defining_identifier [known_discriminant_part] is type_definition [aspect_specification];

| task_type_declaration | protected_type_declaration

Replace 3.2.2(2) by:

subtype_declaration ::= subtype defining_identifier is subtype_indication [aspect_specification];

Replace 3.3.1(2/2) by:

object_declaration ::= defining_identifier_list : [aliased] [constant] subtype_indication [:= expression] [aspect_specification]; | defining_identifier_list : [aliased] [constant] access_definition [:= expression] [aspect_specification]; | defining_identifier_list : [aliased] [constant] array_type_definition [:= expression] [aspect_specification]; | single_task_declaration | single_protected_declaration

Replace 3.8(6) by:

component_declaration ::= defining_identifier_list : component_definition [:= default_expression] [aspect_specification];

Replace 3.9.3(1.1/2) by:

abstract_subprogram_declaration ::= [overriding_indicator] subprogram_specification is abstract [aspect_specification];

Replace 6.1(2/2) by:

subprogram_declaration ::= [overriding_indicator] subprogram_specification [aspect_specification]

Replace 6.7(2/2) by:

null_procedure_declaration ::= [overriding_indicator] procedure_specification is null [aspect_specification];

Replace 7.1(3) by:

package_specification ::= package defining_program_unit_name [aspect_specification] is {basic_declarative_item} [private {basic_declarative_item}] end [[parent_unit_name.]identifier]

Replace 7.3(2) by:

private_type_declaration ::= type defining_identifier [discriminant_part] is [[abstract] tagged] [limited] private [aspect_specification];

Replace 7.3(3/2) by:

private_extension_declaration ::= type defining_identifier [discriminant_part] is [abstract] [limited | synchronized] new ancestor_subtype_indication [and interface_list] with private [aspect_specification];

Replace 9.1(2/2) by:

task_type_declaration ::= task type defining_identifier [known_discriminant_part] [aspect_specification] [is [new interface_list with] task_definition];

Replace 9.1(3/2) by:

single_task_declaration ::= task defining_identifier [aspect_specification] [is [new interface_list with] task_definition];

Replace 9.4(2/2) by:

protected_type_declaration ::= protected type defining_identifier [known_discriminant_part] [aspect_specification] is [new interface_list with] protected_definition;

Replace 9.4(3/2) by:

single_protected_declaration ::= protected defining_identifier [aspect_specification] is [new interface_list with] protected_definition;

Replace 9.5.2(2/2) by:

entry_declaration ::= [overriding_indicator] entry defining_identifier [(discrete_subtype_definition)] parameter_profile [aspect_specification];

Replace 12.1(3) by:

generic_subprogram_declaration ::= generic_formal_part subprogram_specification [aspect_specification];

[AARM NOTE: a generic package can have an aspect_specification because a package_specification allows an aspect_specification.]

Replace 12.4(2/3) by:

formal_object_declaration ::= defining_identifier_list : mode [null_exclusion] subtype_mark [:= default_expression] [aspect_specification]; | defining_identifier_list : mode access_definition [:= default_expression] [aspect_specification];

Replace 12.5(2) by:

formal_type_declaration ::= type defining_identifier[discriminant_part] is formal_type_definition [aspect_specification];

Replace 12.6(2.1/2-2.2/2) by:

formal_concrete_subprogram_declaration ::= with subprogram_specification [is subprogram_default] [aspect_specification];

formal_abstract_subprogram_declaration ::= with subprogram_specification is abstract [subprogram_default] [aspect_specification];

Replace 12.7(2) by:

formal_package_declaration ::= with package defining_identifier is new generic_package_name formal_package_actual_part [aspect_specification];

Add the following at the end of 13.1(0.1/1):

In addition to representation and operational items, aspects of entities may be specified using an aspect_specification (see 13.3.1), which is an optional element of certain kinds of declarations.

Add the following section:

13.3.1 Aspect Specifications

[Redundant: Certain representation or operational aspects of an entity may be specified as part of its declaration using an aspect_specification, rather than using a separate representation or operational item. The declaration with the aspect_specification is termed the associated declaration.]

Syntax

aspect_specification ::= with aspect_mark [=> expression] {, aspect_mark [=> expression] }

aspect_mark ::= aspect_identifier['Class]

AARM NOTE: The aspect_specification is an optional element in the following

kinds of declarations:

* object_declaration;

* full_type_declaration;

* subtype_declaration;

* component_declaration;

* subprogram_declaration;

* abstract_subprogram_declaration;

* null_procedure_declaration;

* package_declaration;

* private_type_declaration;

* private_extension_declaration;

* task_type_declaration;

* single_task_declaration;

* protected_type_declaration;

* single_protected_declaration;

* entry_declaration;

* generic_declaration.

End AARM Note.

Name Resolution

The expected type for an expression associated with a given aspect_mark is the type of the identified aspect of the entity defined by the associated declaration (the associated entity). The names in such an expression [Redundant: are not resolved at the point of the associated declaration, but rather] are resolved at the end of the immediately enclosing declaration list or at the first freezing point of the associated entity, whichever comes first.

If the associated declaration is for a subprogram or entry, the names of the formal parameters are visible within the expression, as are certain attributes, as specified elsewhere in this International Standard for the identified aspect. If the associated declaration is a type_declaration, within the expression the names of any components are visible, and the name of the first subtype denotes the current instance of the type (see 8.6).

Legality Rules

At most one occurrence of each aspect_mark is allowed within a single aspect_specification. The aspect identified by the aspect_mark shall be an aspect that can be specified for the associated entity.

The expression associated with a given aspect_mark may be omitted only when the aspect_mark identifies an aspect of a boolean type, in which case it is equivalent to the expression being specified as True.

If the aspect_mark includes 'Class, then the associated entity shall be a tagged type, or the primitive subprogram of a tagged type.

Additional legality rules may apply, as specified elsewhere in this International Standard for particular aspects.

Static Semantics

Depending on the aspect identified by the aspect_mark, an aspect_specification specifies either a single value, or an expression (such as a precondition) that is to be evaluated at particular points during later execution. The identified aspect of the associated entity is as specified by the expression (or by the default of True when boolean). If the aspect_mark includes 'Class, then:

* if the associated entity is a tagged type, the specification applies to all descendants of the type;

* if the associated entity is a primitive subprogram of a tagged type T, the specification applies to the corresponding primitive subprogram of all descendants of T.

Dynamic Semantics

At the freezing point of the associated entity, the aspect_specification is elaborated. The elaboration of the aspect_specification includes the evaluation of the expression, if the corresponding aspect is a value rather than an expression. If the corresponding aspect represents an expression, the elaboration has no effect; the expression is evaluated later at points within the execution as specified elsewhere in this International Standard for the particular aspect.

!discussion

This syntax was invented to allow pre- and postconditions to be specified for subprograms without worrying about overloading, and without resorting to pragmas. The syntax allows additional aspect names to be added without introducing additional reserved words. Various uses are imagined over and above pre- and postconditions. Here are a number of examples:

function Pop(S : in out Stack) return Elem with Pre => not Is_Empty(S), Post => not Is_Full(S);

type Atomic_Array is array(Positive range <>) of Natural with Atomic_Components;

type Set is interface with Invariant'Class => (Is_Empty(X)) = (Count(X) = 0);

function Union(X, Y : Set) return Set is abstract with Post'Class => Count(Union'Result) = Count(X) + Count(Y);

type R is record X : Positive := 0 with Independent; -- Independence? Y : Natural := 77 with Atomic; -- Atomicity? end record;

type Shared_Bit_Vector is array(0..15) of Boolean with Packing, Independent_Components;

type Bit_Vector is array(0..15) of Boolean with Component_Size => 1;

This presumes that aspect identifiers generally match attribute names or pragma names. However, particularly in the case of pragmas, we may prefer to choose nouns rather than adjectives for aspect names, so the names work better after the preposition "with". Hence, perhaps "Atomicity" or "Independence" rather than "Atomic" and "Independent."

We use "'Class" as an indication that the aspect specification applies to all descendants of the type, or for a subprogram, the corresponding primitive subprogram for all descendants of the type. Other alternatives would be names such as "Inherited_Pre", but Pre'Class meaning it applies to T'Class seems more natural.

Much of the semantics is left to the particular aspects, as it is hard to talk about such things in a general way.

!example

(See discussion.)

!ACATS test

!appendix


From: Yannick Moy
Sent: Tuesday, April 20, 2010  8:58 AM

I would like to question the following legality rule for user-defined kinds of
aspect_mark:

"At most one occurrence of each aspect_mark is allowed within a single
aspect_specification."

Indeed, it could be useful to have multiple user aspects of the same kind. This
is the case, e.g., for an aspect we could add to GNAT, which would give the
ability to specify unit tests, as in:

function Sqrt (X : Integer) return Integer
  with Test => if X > 100 then Sqrt'Result >= 10,
       Test => if X < 100 then Sqrt'Result < 10,
       Test => if X = 100 then Sqrt'Result = 10,
       Test => Sqrt'Result >= 0;

Notice that this aspect is essentially a special kind of postcondition. The goal
in having a special aspect for it and allowing multiple occurrences of this
aspect on the same subprogram is to allow compilers and analysis tools to treat
differently postconditions and these sorts of specifications for unit tests.

As a side note, notice that, although not needed in the example above, it will
in general be necessary to use attribute 'Old to refer to the pre-state of the
call, like in:

procedure Sqrt (X : in out Integer)
  with Test => if X'Old > 100 then X >= 10;

I was told that the "with Blah => ..." syntax is meant to be more-or-less
equivalent to "for ...'Blah use ...". Then, allowing multiple aspects of the
same kind could require that such aspects are named in some way, so that you can
access them in the code with 'Blah("name")?

As Bob suggested that I submit an exact wording, I'll only propose for now:

"Unless specified otherwise for a specific aspect_mark, more than one occurrence
of each aspect_mark is allowed within a single aspect_specification."

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

From: Yannick Moy
Sent: Tuesday, April 27, 2010  11:38 AM

I'll answer my own question, thanks to an idea that Cyrille Comar gave me. He
proposed that we use different identifiers for different aspects of the same
kind that apply to the same declaration, so that the Sqrt example I gave in my
previous email would read:

function Sqrt (X : Integer) return Integer
  with Test_1 => if X > 100 then Sqrt'Result >= 10,
       Test_2 => if X < 100 then Sqrt'Result < 10,
       Test_3 => if X = 100 then Sqrt'Result = 10,
       Test_4 => Sqrt'Result >= 0;

This is already allowed in the current wording, and it fits our needs well, so
please ignore the previous request for allowing multiple user aspects of the
same kind within a single aspect_specification.

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

From: Tucker Taft
Sent: Wednesday, April 28, 2010  2:19 AM

Here is an update to the AI on aspect specifications.
Comments welcome. (yeah, right ;-)
[This is version /03 of the AI - Editor.]

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

From: Bob Duff
Sent: Wednesday, April 28, 2010  6:32 PM

> Here is an update to the AI on aspect specifications.
> Comments welcome. (yeah, right ;-)

;-)

Looks great.  Thanks.

I think we need an Impl Perm to add impl-def aspects.

> !subject Aspect Specifications

>   [AARM NOTE: The aspect_specification is an optional element in the following
>    kinds of declarations:
>     * object_declaration;
>     * full_type_declaration;
>     * subtype_declaration;
>     * component_declaration;
>     * subprogram_declaration;
>     * abstract_subprogram_declaration;
>     * null_procedure_declaration;
>     * package_declaration;
>     * private_type_declaration;
>     * private_extension_declaration;
>     * task_type_declaration;
>     * single_task_declaration;
>     * protected_type_declaration;
>     * single_protected_declaration;
>     * entry_declaration;
>     * generic_declaration.]

It would be useful to list all the kinds of declarations that do not allow
aspect_specs.

I suppose they're not allowed on bodies, even if the body acts as a spec
(subps).

>             Name Resolution
>
>   The expected type for an expression associated with a given
>   aspect_mark is the type of the identified aspect of the entity defined
>   by the associated declaration (the *associated entity*). The names in
>   such an expression [Redundant: are not resolved at the point of the
>   associated declaration, but rather] are resolved at the end of the
>   immediately enclosing declaration list or at the first freezing point
>   of the associated entity, whichever comes first.
>
>   If the associated declaration is for a subprogram or entry, the names of the
>   formal parameters are visible within the expression, as are certain
>   attributes, as specified elsewhere in this International Standard for
>   the identified aspect.  If the associated declaration is a type_declaration,
>   within the expression the names of any components are visible, and the
>   name of the first subtype denotes the current instance of the type (see 8.6).

I think you want "directly visible" above.

We need "current instances" for subtypes, too:

    subtype Nonzero is Integer
        with Predicate => Nonzero /= 0;

>      function Union(X, Y : Set) return Set
>        is abstract with
>          Post'Class =>
>            Count(Union'Result) = Count(X) + Count(Y);

I think "<=" would be more correct than "=" in this example.

> This presumes that aspect identifiers generally match attribute names
> or pragma names.  However, particularly in the case of pragmas, we may
> prefer to choose nouns rather than adjectives for aspect names, so the
> names work better after the preposition "with".  Hence, perhaps
> "Atomicity" or "Independence" rather than "Atomic" and "Independent."

I'm not sure what my opinion is on this.  I'm sure we can discuss it endlessly.
"with Pack" looks funny, but it's a simple rule to say that it matches the
pragma name.

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

From: Randy Brukardt
Sent: Wednesday, April 28, 2010  6:44 PM

> I'm not sure what my opinion is on this.  I'm sure we can discuss it
> endlessly.  "with Pack" looks funny, but it's a simple rule to say
> that it matches the pragma name.

The current Ada aspect name for pragma Pack is "Packing". Ada 95 explicitly
defined this (not sure why). So we have "with Packing =>", not "with Pack". Most
of the others don't have names, however. The question of whether to bother
giving them names probably is an endless pit, as you suggest.

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

From: Bob Duff
Sent: Wednesday, April 28, 2010  7:15 PM

We can have "with Packing" or "with Pack", (with or without "=> True") as we
wish.

Or even "with Packed" or "with Packedness".  ;-)

I think the "packing" in 13.2:

    A pragma Pack specifies the packing aspect of representation; the type (or
    the extension part) is said to be packed.

is my handiwork.  It's not cast in stone.  I think I just wanted it to fit in
with whatever rule forbids specifying the same aspect twice.

> Most of the others don't have names, however. The question of whether
> to bother giving them names probably is an endless pit, as you suggest.

So let's defer that discussion, and concentrate on more important things, like
"Are there any decls that don't allow aspect_clauses, and if so, is there a good
reason, or just because we forgot about them?"

What about formal params?

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

From: Randy Brukardt
Sent: Wednesday, April 28, 2010  7:34 PM

> What about formal params?

I don't think we want those; it would require new kinds of generic matching. And
we don't allow rep clauses or operational clauses on them now; why change that?

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

From: Tucker Taft
Sent: Wednesday, April 28, 2010  7:34 PM

> ...
> So let's defer that discussion, and concentrate on more important
> things, like "Are there any decls that don't allow aspect_clauses, and
> if so, is there a good reason, or just because we forgot about them?"
>
> What about formal params?

And discriminants.

And loop indices.

I didn't include those, but I don't have a strong feeling either way.  Putting
them on formals does add complexity to conformance.

I guess my instinct would be to leave them off, and rely on putting them on
subtypes rather than individual parameters or discriminants.

Randy is right we need to address static matching of subtypes.  It seems we
could allow matching when the same aspects are specified with equal static
expressions.  Alternatively, don't provide static matching at all if the two
subtypes have different sets of aspect_specifications applying to them (include
even "confirming" aspect_specifications).

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

From: Tucker Taft
Sent: Wednesday, April 28, 2010  7:53 PM

Actually I did allow them on generic formal parameters, but not on subprogram
formals. They seem like they might be important on generic formals, but I agree
they will need some generic matching rules if we allow them. At this point we
can simply say that matching rules are specific to each aspect that is allowed
on a generic formal.

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

From: Randy Brukardt
Sent: Wednesday, April 28, 2010  8:03 PM

That might be OK, but then we'll have to check every existing aspect for whether
or not we need to add wording about this case. Which I don't find very
appealing, because I know who will get stuck with the job. :-)

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

From: Bob Duff
Sent: Wednesday, April 28, 2010  8:13 PM

> > What about formal params?
>
> I don't think we want those; ...

I'm not saying we want those.  I'm just saying we want to think about  whether
we want those.  And I'd like to have a complete list of which ones need thinking
about.

(I have an uneasy feeling I'm going to be assigned the task of coming up with
that complete list.  Sigh.  I guess that's fair.)

>... it would require new kinds of generic matching.
> And we don't allow rep clauses or operational clauses on them now; why
>change that?

Well, I recall Robert griping that pragmas are not allowed in formal parts.  I
don't remember the context, but I guess it's related.

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

From: Randy Brukardt
Sent: Wednesday, April 28, 2010  10:02 PM

> Here is an update to the AI on aspect specifications.
> Comments welcome. (yeah, right ;-)

Wording that appears to be missing based on the minutes of the St. Pete meeting:

(1) List of declarations that these are *not* allowed on. It appears currently
    to be renames and bodies. Explain any missing ones.

(2) How does this relate to conformance and static matching? It seems to be
    ignored for subprograms (if it isn't on the body); do we need to say that
    somewhere? Probably need an AARM note even if nothing else changes. Static
    matching surely needs wording (even if to put it off to the individual
    aspects).

(3) There is no wording explaining what identifier an "aspect_mark" is. We've
    put this off, we need an actual answer. (I've always assumed it was the
    aspect names, which are fully defined by the language now, but in any case
    there needs to be wording to say that. I cannot find any now.)

(4) Unrecognized aspects are an error; something needs to be said about this.

(5) We need a standard style for introducing new aspects. That probably should
    be mentioned in the !discussion of this one.

(6) We want to add an index of aspects that can be used here. That probably
    could be another AI (someone needs to propose that formally).

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

From: Randy Brukardt
Sent: Wednesday, April 28, 2010  10:21 PM

> I'm not saying we want those.  I'm just saying we want to think about
> whether we want those.  And I'd like to have a complete list of which
> ones need thinking about.
>
> (I have an uneasy feeling I'm going to be assigned the task of coming
> up with that complete list.  Sigh.  I guess that's fair.)

Bob, come up with that complete list! :-)

Seriously, given Tucker's difficulty in finding time to do things, it would be
best if the rest of us pitched in on "easy" things, which this appears to be. So
go for it.

> >... it would require new kinds of generic matching.
> > And we don't allow rep clauses or operational clauses on
> them now; why
> >change that?
>
> Well, I recall Robert griping that pragmas are not allowed in formal
> parts.  I don't remember the context, but I guess it's related.

I also recall that we convinced him that it was a bad idea, and we didn't do
anything about it (I believe you can find the mail in the second AI about pragma
placement).

I'm against allowing these on any kind of formal parameter; we don't allow any
such things currently on any of the things Tucker listed (subprogram formal
parameters, discriminants, loop parameters, etc.) and it would be a significant
amount of work to change that. (Do you want people to specify how many bits you
can use to pass a parameter? I didn't think so.)

I'm also against allowing it on generic formal parameters, for similar reasons.
Plus the massive number of generic matching rules that would be needed. I
suppose it would be OK to say:

Unless otherwise specified, aspects cannot be given on generic formals.

So that it is illegal unless something really needs it and then specifies what
it means. I surely don't want to be doing matching of preconditions for formal
subprograms!!

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

Questions? Ask the ACAA Technical Agent