!standard 3.2.1(3) 11-03-16 AI05-0183-1/09 !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 8.2(10.1/2) !standard 8.3(23.1/2) !standard 8.5.1(2/2) !standard 8.5.2(2) !standard 8.5.3(2) !standard 8.5.4(2/2) !standard 8.5.5(2) !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.1(8.1/1) !standard 13.1(9) !standard 13.1(9.1/1) !standard 13.1(11/2) !standard 13.1(15.1/2) !standard 13.3(5/1) !standard 13.3(73.11/1) !standard 13.3.1(0) !standard 13.13.2(1/1) !standard 13.14(7.1/2) !class amendment 09-11-01 !status Amendment 2012 10-09-01 !status work item 10-11-19 !status ARG Approved 8-0-2 10-10-29 !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 objects, 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; * renaming_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. 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 end of the immediately enclosing declaration list, or the first freezing point, whichever comes first. 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]; Modify 8.2(10.1/2): The scope of an attribute_definition_clause is identical to the scope of a declaration that would occur at the point of the attribute_definition_clause. {The scope of an aspect_specification is identical to the scope of the associated declaration.} Modify 8.3(23.1/2): An attribute_definition_clause {or an aspect_specification} is visible everywhere within its scope. Replace 8.5.1(2/2) by: object_renaming_declaration ::= defining_identifier : [null_exclusion] subtype_mark renames object_name [aspect_specification]; | defining_identifier : access_definition renames object_name [aspect_specification]; Replace 8.5.2(2) by: exception_renaming_declaration ::= defining_identifier : exception renames exception_name [aspect_specification]; Replace 8.5.3(2) by: package_renaming_declaration ::= package defining_program_unit_name renames package_name [aspect_specification]; Replace 8.5.4(2/2) by: subprogram_renaming_declaration ::= [overriding_indicator] subprogram_specification renames callable_entity_name [aspect_specification]; Replace 8.5.5(2) by: generic_renaming_declaration ::= generic package defining_program_unit_name renames generic_package_name [aspect_specification]; | generic procedure defining_program_unit_name renames generic_procedure_name [aspect_specification]; | generic function defining_program_unit_name renames generic_function_name [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(8.1/1) as follows: An operational item directly specifies an operational aspect of the [type of the subtype]{entity} denoted by the local_name{, except in the case of a type-related operational item, whose local_name shall denote a first subtype, and which directly specifies an aspect of the subtype's type. [The local_name of an operational item shall denote a first subtype. An operational item that names a subtype is type-related.] 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]{an entity} shall appear before the [type]{entity} is frozen (see 13.14). If an operational item {or aspect_specification} is given that directly specifies an aspect of [a type]{an entity}, then it is illegal to give another operational item {or aspect_specification} that directly specifies the same aspect of the [type]{entity}. Modify 13.1(11/2) as follows: Operational and representation aspects of a generic formal parameter are the same as those of the actual. [Operational and r]{R}epresentation aspects are the same for all views of a type. {If an operational aspect is specified for a partial view of a type, then it applies to the full view as well.} A type-related representation item is not allowed for a descendant of a generic formal untagged type. Modify 13.1(15.1/2) as follows: In contrast, whether operational aspects are inherited by a[n untagged] derived type depends on each specific aspect{; unless specified, an operational aspect is not inherited}. [[Operational aspects are never inherited for a tagged type.]] When operational aspects are inherited by a[n untagged] derived type, aspects that were directly specified by operational items that are visible at the point of the derived type declaration, or (in the case where the parent is derived) that were inherited by the parent type from the grandparent type are inherited. An inherited operational aspect is overridden by a subsequent operational item that 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}. Modify 13.3(73.11/1) as follows: The following {type-related} operational attribute is defined: External_Tag. 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 | identifier 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* -- There are no -- language-defined aspects specifiable on renames. 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; * an aspect that is given by an identifier specific to the aspect, the aspect_definition shall be an identifier, and the identifier shall be one of the identifiers specific to the identified aspect. 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. 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 first 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 the first freezing point as it does at the end of the immediately enclosing declaration list. 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 (or view of the entity defined by the associated declaration). 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 a 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; * 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; or * an identifier specific to the aspect. The identified aspect of the associated entity, or in some cases, the view of the entity defined by the declaration, is as specified by the aspect_definition (or by the default of True when boolean). Whether an aspect_specification applies to an entity or only to the particular view of the entity defined by the declaration is determined by the aspect_mark and the kind of entity. The following aspects are view specific: * An aspect specified on an object_declaration; * An aspect specified on a subprogram_declaration; * The Address aspect; * An aspect specified on a renaming_declaration. Other aspect_specifications are associated with the entity, and apply to all views of the entity, unless otherwise specified in this International Standard. 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, certain 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, unless otherwise specified in this International Standard. If an aspect of a derived type is inherited from an ancestor type and has the boolean value True, the inherited value shall not be overridden to have the value False for the derived type, unless otherwise specified in this International Standard. There are no language-defined aspects that may be specified on a renaming_declaration nor on a formal_type_declaration. 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, if any, 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. Modify 13.13.2(1/1): The {type-related} operational attributes Write, Read, Output, and Input attributes convert values to a stream of elements and reconstruct values from a stream. Add after 13.14(7.1/2): * At the freezing point of the entity associated with an aspect_specification, any expressions or names within the aspect_specification cause freezing. !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 end of the enclosing 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; -- 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. 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) @drepl @xcode<@fa@b<@ft>@fa< defining_identifier [known_discriminant_part] >@b<@ft>@fa< type_definition; | task_type_declaration | protected_type_declaration>> @dby @xcode<@fa@b<@ft>@fa< defining_identifier [known_discriminant_part] >@b<@ft>@fa< type_definition [aspect_specification]; | task_type_declaration | protected_type_declaration>> !corrigendum 3.2.2(2) @drepl @xcode<@fa@b<@ft>@fa< defining_identifier >@b<@ft>@fa< subtype_indication;>> @dby @xcode<@fa@b<@ft>@fa< defining_identifier >@b<@ft>@fa< subtype_indication [aspect_specification];>> !corrigendum 3.3.1(2/2) @drepl @xcode<@fa@b<@ft>@fa<] [>@b<@ft>@fa<] subtype_indication [:= expression]; | defining_identifier_list : [>@b<@ft>@fa<] [>@b<@ft>@fa<] access_definition [:= expression]; | defining_identifier_list : [>@b<@ft>@fa<] [>@b<@ft>@fa<] array_type_definition [:= expression]; | single_task_declaration | single_protected_declaration>> @dby @xcode<@fa@b<@ft>@fa<] [>@b<@ft>@fa<] subtype_indication [:= expression] [aspect_specifocation]; | defining_identifier_list : [>@b<@ft>@fa<] [>@b<@ft>@fa<] access_definition [:= expression] [aspect_specification]; | defining_identifier_list : [>@b<@ft>@fa<] [>@b<@ft>@fa<] array_type_definitirn [:= expression] [aspect_specification]; | single_task_declaration | single_protected_declaration>> !corrigendum 3.8(6) @drepl @xcode<@fa> @dby @xcode<@fa> !corrigendum 3.9.3(1.1/2) @drepl @xcode<@fa@b<@ft>@fa<;>> @dby @xcode<@fa@b<@ft>@fa< [aspect_specification];>> !corrigendum 6.1(2/2) @drepl @xcode<@fa> @dby @xcode<@fa> !corrigendum 6.7(2/2) @drepl @xcode<@fa@b<@ft>@fa<;>> @dby @xcode<@fa@b<@ft>@fa< [aspect_specification];>> !corrigendum 7.1(3) @drepl @xcode<@fa@b<@ft>@fa< defining_program_unit_name >@b<@ft>@fa< {basic_declarative_item} [>@b<@ft>@fa< {basic_declarative_item}] >@b<@ft>@fa< [[parent_unit_name.]identifier]>> @dby @xcode<@fa@b<@ft>@fa< defining_program_unit_name [aspect_specification] >@b<@ft>@fa< {basic_declarative_item} [>@b<@ft>@fa< {basic_declarative_item}] >@b<@ft>@fa< [[parent_unit_name.]identifier]>> !corrigendum 7.3(2) @drepl @xcode<@fa@b<@ft>@fa< defining_identifier [discriminant_part] >@b<@ft>@fa< [[>@b<@ft>@fa<] >@b<@ft>@fa<] [>@b<@ft>@fa<] >@b<@ft>@fa<;>> @dby @xcode<@fa@b<@ft>@fa< defining_identifier [discriminant_part] >@b<@ft>@fa< [[>@b<@ft>@fa<] >@b<@ft>@fa<] [>@b<@ft>@fa<] >@b<@ft>@fa< [aspect_specification];>> !corrigendum 7.3(3/2) @drepl @xcode<@fa@b<@ft>@fa< defining_identifier [discriminant_part] >@b<@ft>@fa< [>@b<@ft>@fa<] [>@b<@ft>@fa< | >@b<@ft>@fa<] >@b<@ft>@fa< ancestor_subtype_indication [>@b<@ft>@fa< interface_list] >@b<@ft>@fa<;>> @dby @xcode<@fa@b<@ft>@fa< defining_identifier [discriminant_part] >@b<@ft>@fa< [>@b<@ft>@fa<] [>@b<@ft>@fa< | >@b<@ft>@fa<] >@b<@ft>@fa< ancestor_subtype_indication [>@b<@ft>@fa< interface_list] >@b<@ft>@fa< [aspect_specification];>> !corrigendum 8.2(10.1/2) @drepl The scope of an @fa is identical to the scope of a declaration that would occur at the point of the @fa. @dby The scope of an @fa is identical to the scope of a declaration that would occur at the point of the @fa. The scope of an @fa is identical to the scope of the associated declaration. !corrigendum 8.3(23.1/2) @drepl An @fa is @i everywhere within its scope. @dby An @fa or an @fa is @i everywhere within its scope. !corrigendum 8.5.1(2/2) @drepl @xcode<@fa@ft<@b @i>@fa@ft<@b @i>@fa> @dby @xcode<@fa@ft<@b @i>@fa@ft<@b @i>@fa> !corrigendum 8.5.2(2) @drepl @xcode<@fa@ft<@b @i>@fa> @dby @xcode<@fa@ft<@b @i>@fa> !corrigendum 8.5.2(3) @drepl @xcode<@fa@ft<@b>@fa< defining_program_unit_name >@ft<@b>@fa< package_>>@fa> @dby @xcode<@fa@ft<@b>@fa< defining_program_unit_name >@ft<@b>@fa< package_>>@fa> !corrigendum 8.5.4(2/2) @drepl @xcode<@fa@ft<@b @i>@fa> @dby @xcode<@fa@ft<@b @i>@fa> !corrigendum 8.5.5(2) @drepl @xcode<@fa@ft<@b>@fa< defining_program_unit_name >@ft<@b @i>@fa@ft<@b>@fa< defining_program_unit_name >@ft<@b @i>@fa@ft<@b>@fa< defining_program_unit_name >@ft<@b @i>@fa> @dby @xcode<@fa@ft<@b>@fa< defining_program_unit_name >@ft<@b @i>@fa@ft<@b>@fa< defining_program_unit_name >@ft<@b @i>@fa@ft<@b>@fa< defining_program_unit_name >@ft<@b @i>@fa> !corrigendum 9.1(2/2) @drepl @xcode<@fa@b<@ft>@fa< defining_identifier [known_discriminant_part] [>@b<@ft>@fa< [>@b<@ft>@fa< interface_list >@b<@ft>@fa<] task_definition];>> @dby @xcode<@fa@b<@ft>@fa< defining_identifier [known_discriminant_part] [aspect_specification] [>@b<@ft>@fa< [>@b<@ft>@fa< interface_list >@b<@ft>@fa<] task_definition];>> !corrigendum 9.1(3/2) @drepl @xcode<@fa@b<@ft>@fa< defining_identifier [>@b<@ft>@fa< [>@b<@ft>@fa< interface_list >@b<@ft>@fa<] task_definition];>> @dby @xcode<@fa@b<@ft>@fa< defining_identifier [aspect_specification] [>@b<@ft>@fa< [>@b<@ft>@fa< interface_list >@b<@ft>@fa<] task_definition];>> !corrigendum 9.4(2/2) @drepl @xcode<@fa@b<@ft>@fa< defining_identifier [known_discriminant_part] >@b<@ft>@fa< [>@b<@ft>@fa< interface_list >@b<@ft>@fa<] protected_definition;>> @dby @xcode<@fa@b<@ft>@fa< defining_identifier [known_discriminant_part] [aspect_specification] >@b<@ft>@fa< [>@b<@ft>@fa< interface_list >@b<@ft>@fa<] protected_definition;>> !corrigendum 9.4(3/2) @drepl @xcode<@fa@b<@ft>@fa< defining_identifier >@b<@ft>@fa< [>@b<@ft>@fa< interface_list >@b<@ft>@fa<] protected_definition;>> @dby @xcode<@fa@b<@ft>@fa< defining_identifier [aspect_specification] >@b<@ft>@fa< [>@b<@ft>@fa< interface_list >@b<@ft>@fa<] protected_definition;>> !corrigendum 9.5.2(2/2) @drepl @xcode<@fa@b<@ft>@fa< defining_identifier [(discrete_subtype_definition)] parameter_profile;>> @dby @xcode<@fa@b<@ft>@fa< defining_identifier [(discrete_subtype_definition)] parameter_profile [aspect_specification];>> !corrigendum 11.1(2) @drepl @xcode<@fa@b<@ft>@fa<;>> @dby @xcode<@fa@b<@ft>@fa< [aspect_specification];>> !corrigendum 12.1(3) @drepl @xcode<@fa> @dby @xcode<@fa> !corrigendum 12.3(2/2) @drepl @xcode<@fa@b<@ft>@fa< defining_program_unit_name >@b<@ft>@fa< >@b<@ft>@fa< generic_package_name [generic_actual_part]; | [overriding_indicator] >@b<@ft>@fa< defining_program_unit_name >@b<@ft>@fa< >@b<@ft>@fa< generic_procedure_name [generic_actual_part]; | [overriding_indicator] >@b<@ft>@fa< defining_designator >@b<@ft>@fa< >@b<@ft>@fa< generic_function_name [generic_actual_part];>> @dby @xcode<@fa@b<@ft>@fa< defining_program_unit_name >@b<@ft>@fa< >@b<@ft>@fa< generic_package_name [generic_actual_part] [aspect_specification]; | [overriding_indicator] >@b<@ft>@fa< defining_program_unit_name >@b<@ft>@fa< >@b<@ft>@fa< generic_procedure_name [generic_actual_part] [aspect_specification]; | [overriding_indicator] >@b<@ft>@fa< defining_designator >@b<@ft>@fa< >@b<@ft>@fa< generic_function_name [generic_actual_part] [aspect_specification];>> !corrigendum 12.4(2/2) @drepl @xcode<@fa> @dby @xcode<@fa> !corrigendum 12.5(2) @drepl @xcode<@fa@b<@ft>@fa< defining_identifier[discriminant_part] >@b<@ft>@fa< formal_type_definition;>> @dby @xcode<@fa@b<@ft>@fa< defining_identifier[discriminant_part] >@b<@ft>@fa< formal_type_definition [aspect_specification];>> !corrigendum 12.6(2.1/2) @drepl @xcode<@fa@b<@ft>@fa< subprogram_specification [>@b<@ft>@fa< subprogram_default];>> @dby @xcode<@fa@b<@ft>@fa< subprogram_specification [>@b<@ft>@fa< subprogram_default] [aspect_specification];>> !corrigendum 12.6(2.2/2) @drepl @xcode<@fa@b<@ft> @fa@b<@ft>@fa< [subprogram_default];>> @dby @xcode<@fa@b<@ft> @fa@b<@ft>@fa< [subprogram_default] [aspect_specification];>> !corrigendum 12.7(2) @drepl @xcode<@fa@b<@ft> @fa@b<@ft>@fa< generic_package_name formal_package_actual_part;>> @dby @xcode<@fa@b<@ft> @fa@b<@ft>@fa< generic_package_name formal_package_actual_part [aspect_specification];>> !corrigendum 13.1(0.1/1) @drepl 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. @dby 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 @fa 13.3.1), which is an optional element of certain kinds of declarations. !corrigendum 13.3(5/1) @drepl An @fa is allowed in an @fa 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. @dby An @fa is allowed in an @fa 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) @dinsc Certain representation or operational aspects of an entity may be specified as part of its declaration using an @fa, rather than using a separate representation or operational item. The declaration with the @fa is termed the @i. @i<@s8> @xcode<@fa@b<@ft>@fa< aspect_mark [=@> aspect_definition] {, aspect_mark [=@> aspect_definition] }>> @xcode<@fa@i<@ft>@fa@ft@fa<]>> @xcode<@fa> @i<@s8> An @fa identifies an aspect of the entity defined by the associated declaration (the @i); the aspect denotes an object, a value, an expression, a subprogram, or some other kind of entity. If the @fa identifies: @xbullet shall be a @fa. The expected type for the @fa is the type of the identified aspect of the associated entity;> @xbullet shall be an @fa. The expected type for the @fa is the type of the identified aspect of the associated entity;> @xbullet shall be a @fa; the expected profile for the @fa is the profile required for the aspect of the associated entity;> @xbullet shall be a @fa, and the @fa shall resolve to denote an entity of the appropriate kind;> @xbullet shall be an @fa, and the @fa shall be one of the identifiers specific to the identified aspect.> The usage names in an @fa are not resolved at the point of the associated declaration, but rather are resolved at the end of the immediately enclosing declaration list. If the associated declaration is for a subprogram or entry, the names of the formal parameters are visible within the @fa, as are certain attributes, as specified elsewhere in this International Standard for the identified aspect. If the associated declaration is a @fa, within the @fa 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 @fa, within the @fa the name of the new subtype denotes the current instance of the (sub)type. @i<@s8> If the first freezing point of the associated entity comes before the end of the immediately enclosing declaration list, then each usage name in the @fa shall resolve to the same entity at the first freezing point as it does at the end of the immediately enclosing declaration list. At most one occurrence of each @fa is allowed within a single @fa. The aspect identified by the @fa shall be an aspect that can be specified for the associated entity (or view of the entity defined by the associated declaration). The @fa associated with a given @fa may be omitted only when the @fa identifies an aspect of a boolean type, in which case it is equivalent to the @fa being specified as True. If the @fa includes 'Class, then the associated entity shall be a tagged type or a primitive subprogram of a tagged type. @i<@s8> @i<@b> !example (See discussion.) !ACATS test ACATS B-Tests should be generated for the legality rules here. ACATS C-Tests will be generated for specific aspects; there isn't a need to see if the clauses are supported individually. !ASIS [From Tucker.] !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 subtype