Version 1.11 of ai05s/ai05-0183-1.txt
!standard 3.2.1(3) 10-10-25 AI05-0183-1/06
!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 11.1(2)
!standard 12.1(3)
!standard 12.3(2/2)
!standard 12.4(2/2)
!standard 12.5(2)
!standard 12.6(2.1/2)
!standard 12.6(2.2/2)
!standard 12.7(2)
!standard 13.1(0.1/2)
!standard 13.3(5/1)
!standard 13.3.1(0)
!class amendment 09-11-01
!status Amendment 2012 10-09-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;
* exception_declaration;
* generic_declaration;
* generic_instantiation;
* generic_formal_parameter_declaration.
Aspect specification are not permitted on renaming declarations, as
that would seem to break the underlying model of renaming (that properties are
the same as the renamed entity).
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(3) 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 11.1(2) by:
exception_declaration ::= defining_identifier_list : exception
[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.3(2/2) by:
generic_instantiation ::=
package defining_program_unit_name is
new generic_package_name [generic_actual_part]
[aspect_specification];
| [overriding_indicator]
procedure defining_program_unit_name is
new generic_procedure_name [generic_actual_part]
[aspect_specification];
| [overriding_indicator]
function defining_designator is
new generic_function_name [generic_actual_part]
[aspect_specification];
Replace 12.4(2/2) 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.
Modify 13.1(9, 9.1/1) as follows:
A representation item that directly specifies an aspect of a subtype
or type shall appear after the type is completely defined (see
3.11.1), and before the subtype or type is frozen (see 13.14). If a
representation item {or aspect_specification} is given that directly
specifies an aspect of an entity, then it is illegal to give another
representation item {or aspect_specification} that directly specifies
the same aspect of the entity.
An operational item that directly specifies an aspect of a type shall
appear before the type is frozen (see 13.14). If an operational item
is given that directly specifies an aspect of a type, then it is
illegal to give another operational item {or aspect_specification}
that directly specifies the same aspect of the type.
Revise 13.3(5/1) as follows:
... Each specifiable attribute constitutes an operational aspect or
aspect of representation{; the name of the aspect is that of the
attribute}.
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 [=> aspect_definition] {,
aspect_mark [=> aspect_definition] }
aspect_mark ::= aspect_identifier['Class]
aspect_definition ::= name | expression
AARM NOTE: The aspect_specification is an optional element
in most kinds of declarations. Here is a list of all kinds of
declarations and an indication of whether or not they allow aspect clauses,
and in some cases a short discussion of why (* = allowed, NO = not allowed)
basic_declaration
type_declaration
full_type_declaration*
...
task_type_declaration*
protected_type_declaration*
incomplete_type_declaration -- NO
private_type_declaration*
private_extension_declaration*
subtype_declaration*
object_declaration*
...
single_task_declaration*
single_protected_declaration*
number_declaration -- NO
subprogram_declaration*
abstract_subprogram_declaration*
null_procedure_declaration*
package_declaration*
renaming_declaration -- NO
-- Allowing a renaming to change operational or representational
-- aspects would seem to break the underlying model of renaming.
exception_declaration*
generic_declaration*
generic_instantiation*
enumeration_literal_specification -- NO
discriminant_specification -- NO
component_declaration*
loop_parameter_specification -- NO
parameter_specification -- NO
subprogram_body -- NO
entry_declaration*
entry_index_specification -- NO
choice_parameter_specification -- NO
generic_formal_parameter_declaration*
-- There are no language-defined aspects that
-- may be specified on generic formals, but implementations
-- might support some. The implementation would have to
-- define the matching rule.
extended_return_statement -- NO
end of AARM Note.
Name Resolution
An aspect_mark identifies an aspect of the entity defined by the
associated declaration (the associated entity); the aspect denotes
an object, a value, an expression, a subprogram, or some other kind of
entity. If the aspect_mark identifies:
* an aspect that denotes an object, the aspect_definition shall be a
name; the expected type for the name
is the type of the identified aspect of the associated entity;
* an aspect that is a value or an expression, the aspect_definition
shall be an expression; the expected type for the expression
is the type of the identified aspect of the associated entity;
* an aspect that denotes a subprogram, the aspect_definition shall
be a name; the expected profile for the name
is the profile required for the aspect of the associated entity;
* an aspect that denotes some other kind of entity, the aspect_definition
shall be a name, and the name shall resolve to denote an entity of
the appropriate kind.
The usage names in an aspect_definition [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 directly visible within the
aspect_definition, 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
aspect_definition the names of any visible components, protected
subprograms, and entries are directly visible, and the name of the
first subtype denotes the current instance of the type (see 8.6). If
the associated declaration is a subtype_declaration, within the
aspect_definition the name of the new subtype denotes the current
instance of the (sub)type.
Legality Rules
If the freezing point of the associated entity comes before the end of
the immediately enclosing declaration list, then each usage name in the
aspect_definition shall resolve to the same entity at both places.
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 aspect_definition 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 aspect_definition 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.
Static Semantics
Depending on which aspect is identified by the aspect_mark, an
aspect_definition specifies a name that denotes a subprogram, object,
or other kind of entity, or an expression, which is either evaluated
to produce a single value, or which (as in a precondition) is to be
evaluated at particular points during later execution. The identified
aspect of the associated entity is as specified by the
aspect_definition (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.
All specifiable operational and representation attributes may be
specified with an aspect_specification instead of an
attribute_definition_clause (see 13.3). The attribute_designator is
used for the aspect_mark. In addition, other operational and
representation aspects not associated with specifiable attributes may
be specified, as specified elsewhere in this International Standard.
In the case of aspects specifiable with pragmas, the pragma identifier
is used for the aspect_mark.
Alternative legality and semantics rules may apply for particular
aspects, as specified elsewhere in this International Standard.
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 name or expression, unless the aspect itself is an
expression. If the corresponding aspect represents an expression (as in a
precondition), 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 => True;
Y : Natural := 77
with Atomic => True;
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. We considered, in the case of pragmas, choosing nouns
rather than adjectives for aspect names, so the names might work better
after the preposition "with". Hence, we considered "Atomicity" or
"Independence" rather than "Atomic" and "Independent." However, that
seemed to be introducing unnecessary complexity, and adding "=> True"
makes the adjectives work grammatically, so by default the aspect
name will be presumed to be the same as the pragma. Pragma Pack
currently specifies that its aspect is "packing," but we might want to
change that for consistency. See AI05-0112-1.
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.
We defer resolving the names in the aspect_definition to the first
freezing point or end of the declaration list because in many cases the
entities referenced in the aspect_definition will necessarily, or more
conveniently, be declared after the entity with the aspect
specification. For example, for a type, any aspect that refers to an
operation of the type will be a forward reference. For a subprogram, an
aspect that refers to another subprogram will often be a forward
reference, as ordering the subprograms based on the aspect_definitions
would be painful and sometimes impossible.
If the freezing point comes before the end of the enclosing declaration
list, we require the usage names in the aspect_definition to resolve to
the same entities at the two places. Because there is no explicit
indication of where a freezing point occurs in the source, we felt it
would be too confusing if we didn't require this. This means that if a
freezing point "moves" and thereby crosses over, for example, the
overriding of an inherited subprogram (of a non-tagged type), the
compiler would complain rather than silently reinterpreting the name in
the aspect_definition. For example:
type New_T is new T
with Type_Invariant => Is_Valid(New_T);
Default_Obj : New_T; --
function Is_Valid(Y : New_T) return Boolean;
--
private -- Here we reach the end of the declaration list.
In a case like this, the user almost certainly wants to refer to the
overriding of Is_Valid, but since the freezing happens before the
overriding, without the rule to require that the names in the
aspect_definition resolve to the same thing, they would not get what
they expected. With this rule, the compiler would complain, and the
user would (hopefully ;-) realize they need to move the declaration of
Default_Obj down a little further so Is_Valid can be overridden first.
We don't bother talking about the case of a declaration with multiple
defining_identifiers in its defining_identifier_list, because RM
3.3.1(7) already says such a multi-defining-identifier declaration is
equivalent to a sequence of single-defining-identifier declarations.
Much of the semantics is left to the particular aspects, as it is hard
to talk about such things in a general way.
!corrigendum 3.2.1(3)
Replace the paragraph:
full_type_declaration ::=
type defining_identifier [known_discriminant_part] is type_definition;
| task_type_declaration
| protected_type_declaration
by:
full_type_declaration ::=
type defining_identifier [known_discriminant_part] is type_definition
[aspect_specification];
| task_type_declaration
| protected_type_declaration
!corrigendum 3.2.2(2)
Replace the paragraph:
subtype_declaration ::=
subtype defining_identifier is subtype_indication;
by:
subtype_declaration ::=
subtype defining_identifier is subtype_indication
[aspect_specification];
!corrigendum 3.3.1(2/2)
Replace the paragraph:
object_declaration ::=
defining_identifier_list : [aliased] [constant] subtype_indication [:= expression];
| defining_identifier_list : [aliased] [constant] access_definition [:= expression];
| defining_identifier_list : [aliased] [constant] array_type_definition [:= expression];
| single_task_declaration
| single_protected_declaration
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
!corrigendum 3.8(6)
Replace the paragraph:
component_declaration ::=
defining_identifier_list : component_definition [:= default_expression];
by:
component_declaration ::=
defining_identifier_list : component_definition [:= default_expression]
[aspect_specification];
!corrigendum 3.9.3(1.1/2)
Replace the paragraph:
abstract_subprogram_declaration ::=
[overriding_indicator]
subprogram_specification is abstract;
by:
abstract_subprogram_declaration ::=
[overriding_indicator]
subprogram_specification is abstract
[aspect_specification];
!corrigendum 6.1(2/2)
Replace the paragraph:
subprogram_declaration ::=
[overriding_indicator]
subprogram_specification;
by:
subprogram_declaration ::=
[overriding_indicator]
subprogram_specification
[aspect_specification];
!corrigendum 6.7(2/2)
Replace the paragraph:
null_procedure_declaration ::=
[overriding_indicator]
procedure_specification is null;
by:
null_procedure_declaration ::=
[overriding_indicator]
procedure_specification is null
[aspect_specification];
!corrigendum 7.1(3)
Replace the paragraph:
package_specification ::=
package defining_program_unit_name is
{basic_declarative_item}
[private
{basic_declarative_item}]
end [[parent_unit_name.]identifier]
by:
package_specification ::=
package defining_program_unit_name
[aspect_specification] is
{basic_declarative_item}
[private
{basic_declarative_item}]
end [[parent_unit_name.]identifier]
!corrigendum 7.3(2)
Replace the paragraph:
private_type_declaration ::=
type defining_identifier [discriminant_part] is [[abstract] tagged] [limited] private;
by:
private_type_declaration ::=
type defining_identifier [discriminant_part] is [[abstract] tagged] [limited] private
[aspect_specification];
!corrigendum 7.3(3/2)
Replace the paragraph:
private_extension_declaration ::=
type defining_identifier [discriminant_part] is
[abstract] [limited | synchronized] new ancestor_subtype_indication
[and interface_list] with private;
by:
private_extension_declaration ::=
type defining_identifier [discriminant_part] is
[abstract] [limited | synchronized] new ancestor_subtype_indication
[and interface_list] with private
[aspect_specification];
!corrigendum 9.1(2/2)
Replace the paragraph:
task_type_declaration ::=
task type defining_identifier [known_discriminant_part] [is
[new interface_list with]
task_definition];
by:
task_type_declaration ::=
task type defining_identifier [known_discriminant_part]
[aspect_specification] [is
[new interface_list with]
task_definition];
!corrigendum 9.1(3/2)
Replace the paragraph:
single_task_declaration ::=
task defining_identifier [is
[new interface_list with]
task_definition];
by:
single_task_declaration ::=
task defining_identifier
[aspect_specification] [is
[new interface_list with]
task_definition];
!corrigendum 9.4(2/2)
Replace the paragraph:
protected_type_declaration ::=
protected type defining_identifier [known_discriminant_part] is
[new interface_list with]
protected_definition;
by:
protected_type_declaration ::=
protected type defining_identifier [known_discriminant_part]
[aspect_specification] is
[new interface_list with]
protected_definition;
!corrigendum 9.4(3/2)
Replace the paragraph:
single_protected_declaration ::=
protected defining_identifier is
[new interface_list with]
protected_definition;
by:
single_protected_declaration ::=
protected defining_identifier
[aspect_specification] is
[new interface_list with]
protected_definition;
!corrigendum 9.5.2(2/2)
Replace the paragraph:
entry_declaration ::=
[overriding_indicator]
entry defining_identifier [(discrete_subtype_definition)] parameter_profile;
by:
entry_declaration ::=
[overriding_indicator]
entry defining_identifier [(discrete_subtype_definition)] parameter_profile
[aspect_specification];
!corrigendum 11.1(2)
Replace the paragraph:
exception_declaration ::= defining_identifier_list : exception;
by:
exception_declaration ::= defining_identifier_list : exception
[aspect_specification];
!corrigendum 12.1(3)
Replace the paragraph:
generic_subprogram_declaration ::=
generic_formal_part subprogram_specification
[aspect_specification];
by:
generic_subprogram_declaration ::=
generic_formal_part subprogram_specification
[aspect_specification];
!corrigendum 12.3(2/2)
Replace the paragraph:
generic_instantiation ::=
package defining_program_unit_name is
new generic_package_name [generic_actual_part];
| [overriding_indicator]
procedure defining_program_unit_name is
new generic_procedure_name [generic_actual_part];
| [overriding_indicator]
function defining_designator is
new generic_function_name [generic_actual_part];
by:
generic_instantiation ::=
package defining_program_unit_name is
new generic_package_name [generic_actual_part]
[aspect_specification];
| [overriding_indicator]
procedure defining_program_unit_name is
new generic_procedure_name [generic_actual_part]
[aspect_specification];
| [overriding_indicator]
function defining_designator is
new generic_function_name [generic_actual_part]
[aspect_specification];
!corrigendum 12.4(2/2)
Replace the paragraph:
formal_object_declaration ::=
defining_identifier_list : mode [null_exclusion] subtype_mark [:= default_expression];
| defining_identifier_list : mode access_definition [:= default_expression];
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];
!corrigendum 12.5(2)
Replace the paragraph:
formal_type_declaration ::=
type defining_identifier[discriminant_part] is formal_type_definition;
by:
formal_type_declaration ::=
type defining_identifier[discriminant_part] is formal_type_definition
[aspect_specification];
!corrigendum 12.6(2.1/2)
Replace the paragraph:
formal_concrete_subprogram_declaration ::=
with subprogram_specification [is subprogram_default];
by:
formal_concrete_subprogram_declaration ::=
with subprogram_specification [is subprogram_default]
[aspect_specification];
!corrigendum 12.6(2.2/2)
Replace the paragraph:
formal_abstract_subprogram_declaration ::=
with subprogram_specification is abstract [subprogram_default];
by:
formal_abstract_subprogram_declaration ::=
with subprogram_specification is abstract [subprogram_default]
[aspect_specification];
!corrigendum 12.7(2)
Replace the paragraph:
formal_package_declaration ::=
with package defining_identifier is new generic_package_name formal_package_actual_part;
by:
formal_package_declaration ::=
with package defining_identifier is new generic_package_name formal_package_actual_part
[aspect_specification];
!corrigendum 13.1(0.1/1)
Replace the paragraph:
Representation and operational items can
be used to specify aspects of entities. Two kinds of aspects of entities can be
specified: aspects of representation and operational aspects. Representation
items specify how the types and other entities of the language are to be mapped
onto the underlying machine. Operational items specify other properties of
entities.
by:
Representation and operational items can
be used to specify aspects of entities. Two kinds of aspects of entities can be
specified: aspects of representation and operational aspects. Representation
items specify how the types and other entities of the language are to be mapped
onto the underlying machine. Operational items specify other properties of
entities. In addition to representation and operational
items, aspects of entities may be specified using an aspect_specification
13.3.1), which is an optional element of certain
kinds of declarations.
!corrigendum 13.3(5/1)
Replace the paragraph:
An attribute_designator is allowed in an attribute_definition_clause
only if this International Standard explicitly allows it, or for an
implementation-defined attribute if the implementation allows it. Each
specifiable attribute constitutes an operational aspect or an aspect of
representation.
by:
An attribute_designator is allowed in an attribute_definition_clause
only if this International Standard explicitly allows it, or for an
implementation-defined attribute if the implementation allows it. Each
specifiable attribute constitutes an operational aspect or an aspect of
representation; the name of the aspect is that of the
attribute.
!corrigendum 13.3.1(0)
Insert new clause:
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 [=> aspect_definition] {,
aspect_mark [=> aspect_definition] }
aspect_mark ::= aspect_identifier['Class]
aspect_definition ::= name | expression
Name Resolution Rules
An aspect_mark identifies an aspect of the entity defined by the
associated declaration (the associated entity); the aspect denotes
an object, a value, an expression, a subprogram, or some other kind of
entity. If the aspect_mark identifies:
- an aspect that denotes an object, the aspect_definition shall be a
name. The expected type for the name is the type of the identified
aspect of the associated entity.
- an aspect that is a value or an expression, the aspect_definition
shall be an expression. The expected type for the expression
is the type of the identified aspect of the associated entity.
- an aspect that denotes a subprogram, the aspect_definition shall
be a name; the expected profile for the name is the profile required
for the aspect of the associated entity.
- an aspect that denotes some other kind of entity, the aspect_definition
shall be a name, and the name shall resolve to denote an entity of
the appropriate kind.
The usage names in an aspect_definition 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 aspect_definition, 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 aspect_definition the names of any components are visible, and the name of
the first subtype denotes the current instance of the type (see 8.6). If the
associated declaration is a subtype_declaration, within the
aspect_definition the name of the new subtype denotes the current instance
of the (sub)type.
Rest of this text TBD
!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!!
****************************************************************
From: Bob Duff
Sent: Monday, May 10, 2010 2:25 PM
This is my response to this homework item:
AI05-0183-1: Work with Tucker on a list of declarations that don't allow
aspect_specifications, and why not.
which was assigned to me at the April 29 telephone meeting.
I'm not sure about the "why not" part.
There is a list of declarations that include aspect_spec in the !proposal, and
again in the AARM. The latter is missing generic_formal_parameter_declaration.
It's also missing from the syntax rules.
Seems like it should be included.
I suggest putting the list only in the AARM, and put something like this in the
proposal:
The aspect_specification is an optional element allowed by the syntax rules
for many kinds of declarations.
Here's the list:
* 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?]
I did not carefully review the syntax rules in the AI to see if they in fact
match the above list.
Here's a list of all the kinds of declaration, with "*" marking the ones
mentioned above, and NO marking the ones that currently do not allow an
aspect_specification.
basic_declaration
type_declaration
full_type_declaration*
...
task_type_declaration*
protected_type_declaration*
incomplete_type_declaration -- NO
private_type_declaration*
private_extension_declaration*
subtype_declaration*
object_declaration*
...
single_task_declaration*
single_protected_declaration*
number_declaration -- NO
subprogram_declaration*
abstract_subprogram_declaration*
null_procedure_declaration*
package_declaration*
renaming_declaration -- NO
exception_declaration -- NO
generic_declaration*
generic_instantiation -- NO
enumeration_literal_specification -- NO
discriminant_specification -- NO
component_declaration*
loop_parameter_specification -- NO
parameter_specification -- NO
subprogram_body -- NO
entry_declaration*
entry_index_specification -- NO
choice_parameter_specification -- NO
generic_formal_parameter_declaration* (or NO -- not clear)
extended_return_statement -- NO
I guess we should add renaming_declaration and exception_declaration.
I guess generic_formal_parameter_declaration should be included.
It seems a little odd to allow component_declaration, but not
discriminant_specification. Not sure about parameter_specification.
Please discuss. When that's done, we should add AARM text after the list of
declarations that allow it, like:
The syntax rules do not allow aspect_specifications on the other kinds of
declarations, which are:
... (list them)
Also, aspect_specifications are not allowed on bodies or accept statements,
even though these things are sort of like declarations, and in the case of
subprogram_bodies can actually be declarations. If you want an
aspect_specification on a subprogram, you have to give an explicit
declaration before the body.
****************************************************************
From: Gary Dismukes
Sent: Monday, May 10, 2010 7:09 PM
> I guess we should add renaming_declaration and exception_declaration.
I agree those should be included.
> I guess generic_formal_parameter_declaration should be included.
Dunno. Doesn't that get into matching complexities?
> It seems a little odd to allow component_declaration, but not
> discriminant_specification. Not sure about parameter_specification.
It does seem inconsistent to disallow them for discriminants. Is there any
significant argument for not allowing them on discriminants and parameter specs?
I suppose it tends to interfere with readability, plus there's the issue of
conformance for spec/body and multipart declarations.
****************************************************************
From: Tucker Taft
Sent: Monday, May 10, 2010 9:12 PM
I am reluctant to allow specifying aspects on a renaming declaration. That
could really confuse the model and add a lot of complexity to handling renames,
which are already pretty tricky. I agree that exception declarations should
allow aspect specifications.
Randy suggested that by default, aspect specifications would not be permitted on
generic_formal_parameter_decls, but that they could be permitted for particular
aspects. We would have to define the matching rules for any aspects that we
allow being specified on a generic formal. But it seems like it could be useful
at least in some cases.
Allowing them on discriminants or parameters definitely adds complexity to
conformance rules. It doesn't seem so odd that discriminants are special, since
they have other unique properties, such as being read-only, and being
specifiable in a subtype indication, etc.
****************************************************************
From: Jean-Pierre Rosen
Sent: Tuesday, May 11, 2010 1:44 AM
> I am reluctant to allow specifying aspects on a renaming declaration.
> That could really confuse the model and add a lot of complexity to
> handling renames, which are already pretty tricky. I agree that
> exception declarations should allow aspect specifications.
I fully agree here. Aspects are a property of the entity, not of the view. We
already have the problem that constraints on the subtype of a renaming are
ignored, let's not make it worse.
****************************************************************
From: Bob Duff
Sent: Tuesday, May 11, 2010 8:46 PM
> I am reluctant to allow specifying aspects on a renaming declaration.
> That could really confuse the model and add a lot of complexity to
> handling renames, which are already pretty tricky.
If we have no aspects that are specifiable on renames, we could still allow the
syntax, just in case an implementation wants to do it for an impl-def aspect.
Then whatever complexity there is belongs to the implementer.
Renames can be dispatching ops. So you can't put a precondition on one? Hmm...
>...I agree that exception declarations
> should allow aspect specifications.
>
> Randy suggested that by default, aspect specifications would not be
> permitted on generic_formal_parameter_decls, but that they could be
> permitted for particular aspects.
But that's true for everything. That is, we define the syntax to allow
aspect_specs on certain decls. Then, for each aspect, we say "this is allowed
on so-and-so decls".
If there are no language-defined aspects that are allowed on
generic_formal_parameter_decls, we can still allow the syntax.
> We would have to define the matching rules for any aspects that we
> allow being specified on a generic formal.
If there are no language-defined ones, we can let implementers worry about that.
>...But it seems like it could be useful at least in some cases.
>
> Allowing them on discriminants or parameters definitely adds
> complexity to conformance rules. It doesn't seem so odd that
> discriminants are special, since they have other unique properties,
> such as being read-only, and being specifiable in a subtype
> indication, etc.
Again, all the complexity can be placed on the implementer, if all we do is
allow the syntax. On the other hand, the syntax gets pretty ugly in these
cases.
I don't feel strongly about any of this, except that I strongly believe we
should have a list in the AARM of the decls (and bodies) that don't allow
aspects syntactically, so we can be sure we did it deliberately. I suggested
wording in my previous e-mail.
****************************************************************
From: Randy Brukardt
Sent: Wednesday, May 19, 2010 10:14 PM
> This is my response to this homework item:
>
> AI05-0183-1: Work with Tucker on a list of declarations that don't
> allow aspect_specifications, and why not.
>
> which was assigned to me at the April 29 telephone meeting.
> I'm not sure about the "why not" part.
I think you were supposed to explain why each basic declaration that doesn't
allow aspect clauses doesn't allow aspect clauses. (I can't think of any way to
say this that isn't redundant!) Maybe it would be better to say that there needs
to be an explanation for each declaration on the list of declarations that don't
allow aspect_clauses -- the idea being that the default is that they *are*
allowed. This seems like useful information for the AARM.
****************************************************************
From: Bob Duff
Sent: Friday, May 20, 2010 7:07 AM
Right, I understood that, and my "I'm not sure..." comment was meant to mean "I
don't know the answer to those questions".
I'm the one who raised the issue, and I'm happy with just having the list, so I
can look at it and say "yeah, OK, seems reasonable I guess". If Tuck can put
coherent reasons on them, that's fine too.
****************************************************************
From: Randy Brukardt
Sent: Wednesday, May 19, 2010 10:24 PM
> > Randy suggested that by default, aspect specifications would not be
> > permitted on generic_formal_parameter_decls, but that they could be
> > permitted for particular aspects.
>
> But that's true for everything. That is, we define the syntax to
> allow aspect_specs on certain decls. Then, for each aspect, we say
> "this is allowed on so-and-so decls".
Sadly, we don't do a good job of that for the existing aspects in Ada 95 and
2005. However, the rule added by AI05-0106-1 (13.1(9.2/3)) should cover it, so
we don't need any additional wording for this AI.
****************************************************************
From: Bob Duff
Sent: Friday, May 14, 2010 8:08 AM
I think AI05-0183-1 (Aspect Specifications) needs some verbiage about
visibility. In particluar, this (from Yannick's recent ada-comment@ e-mail):
type Part (Max_Players : Positive) is record
...
Num_Players : Positive; -- Number of players
Pos : Positions (1 .. Max_Players); -- Position of each player
end record
with Predicate => Num_Players in 1 .. Max_Players;
should be legal. So should this:
with Predicate => Part.Num_Players in 1 .. Part.Max_Players;
****************************************************************
From: Tucker Taft
Sent: Monday, June 7, 2010 2:58 PM
Here is an update to the aspect specification AI. [This is version /04 - Editor.]
There are still some things missing, such as the
Annex of specifiable aspects. I am
also a little unclear how we should
indicate in the body of the RM
(as opposed to in the eventual annex) which aspects can be specified.
My guess is that all specifiable attributes should be specifiable using an
aspect_specification. But it is not clear which pragmas nor
which of the other aspects associated
with record and enum rep clauses should
be specifiable with an aspect_specification.
****************************************************************
From: Randy Brukardt
Sent: Thursday, June 10, 2010 9:22 PM
> Here is an update to the aspect
> specification AI. There are still
> some things missing, such as the
> Annex of specifiable aspects. I am
> also a little unclear how we should
> indicate in the body of the RM
> (as opposed to in the eventual annex)
> which aspects can be specified.
So are the rest of us! Someone needs to invent something, and you're one of the
best inventors.
> My guess is that all specifiable attributes should be specifiable
> using an aspect_specification.
> But it is not clear which pragmas nor
> which of the other aspects associated
> with record and enum rep clauses should be specifiable with an
> aspect_specification.
I think a straw-man here would be helpful. I'm not even sure that most of us are
considering everything that might be possible to specify.
So I think it would be helpful if you would make a stab at figuring how these
things might work. (But only after the rest of your homework is done, the two
remaining AIs are more important than these details of this one.)
****************************************************************
From: Tucker Taft
Sent: Monday, October 25, 2010 2:55 PM
Here is a relatively minor update to AI05-0183-1. [This is version /06 of
the AI.]
I added a requirement that all usage_names that appear in an aspect_definition
resolve to the same thing if freezing happens before the end of the declaration
list, along with an example in the !discussion.
I added some general statements about attribute-defs and pragmas that can be
replaced by aspect_specs.
I made some other minor fixes as requested in the minutes.
****************************************************************
From: Robert Dewar
Sent: Monday, October 25, 2010 3:13 PM
> If the freezing point comes before the end of the enclosing
> declaration list, we require the usage names in the aspect_definition
> to resolve to the same entities at the two places. Because there is
> no explicit indication of where a freezing point occurs in the source,
> we felt it would be too confusing if we didn't require this.
I really have NO idea how to implement this without a major earthquake.
I think we will just leave this unimplemented in GNAT and not bother with it. At
this stage ACATS tests are merely useful tools anway, formal validation has
entirely disappeared as an issue.
Perhaps Ed has some ideas.
****************************************************************
From: Tucker Taft
Sent: Monday, October 25, 2010 3:19 PM
Did you take a look at the example in the !discussion?
It does seem pretty convincing (at least to me) that this is a legitimate
concern. Here it is again.
===
If the freezing point comes before the end of the enclosing declaration list, we
require the usage names in the aspect_definition to resolve to the same entities
at the two places. Because there is no explicit indication of where a freezing
point occurs in the source, we felt it would be too confusing if we didn't
require this. This means that if a freezing point "moves" and thereby crosses
over, for example, the overriding of an inherited subprogram (of a non-tagged
type), the compiler would complain rather than silently reinterpreting the name
in the aspect_definition. For example:
type New_T is new T
with Type_Invariant => Is_Valid(New_T);
Default_Obj : New_T; -- Here we freeze New_T
function Is_Valid(Y : New_T) return Boolean;
-- Here we override Is_Valid
private -- Here we reach the end of the declaration list.
In a case like this, the user almost certainly wants to refer to the overriding
of Is_Valid, but since the freezing happens before the overriding, without the
rule to require that the names in the aspect_definition resolve to the same
thing, they would not get what they expected. With this rule, the compiler
would complain, and the user would (hopefully ;-) realize they need to move the
declaration of Default_Obj down a little further so Is_Valid can be overridden
first.
****************************************************************
From: Robert Dewar
Sent: Monday, October 25, 2010 3:54 PM
Are these things really called Type_Invariant, rather than just Invariant? I
don't really mind, but it is a pain to change and I prefer the shorter name
anyway.
****************************************************************
From: Robert Dewar
Sent: Monday, October 25, 2010 3:55 PM
> Did you take a look at the example in the !discussion?
> It does seem pretty convincing (at least to me) that this is a
> legitimate concern. Here it is again.
I think whenever you cause a major impossible pain to an existing implementation
(Ed agrees with me that this is that category), then you have to be sure it is
worth it. To recall, for Ada 95, we went out of our way to accomodate displays
because one implementation demanded it, despite the fact that it
a) really damaged expressive power
b) turned out to be quite unnecessary, the one implementation involved never
made it to Ada 95 anyway.
I don't think this begins to be in the category of critical things that are
worth causing major pain to an implementation (especially considering that you
can't really do that any more, implementations will just ignore things they
can't implement, especially when it is just a matter of diagnosing unexpected
behavior).
To me this is more in the warning category anyway I would just settle for
implementation advice that says it is desirable to warn in this situation.
Yes, I see the example, but as I say, it is more a case where a warning is more
appropriate anyway, I am always nervous when I see a language designer say
"the user almost certainly wants to ..."
which is more likely worth a warning if true.
In this case, what GNAT could do, and actually it seems a good idea, is to have
optional information messages that say
"warning: Invariant expression from line 12 is resolved here"
"warning: since type& is frozen here"
****************************************************************
Questions? Ask the ACAA Technical Agent