!standard 3.9.3(1.1/2) 09-12-28 AI05-0183-1/02 !standard 6.1(2/2) !standard 6.7(2/2) !standard 9.5.2(2/2) !standard 13.1 (0.1/2) !standard 13.3.1 (0) !class amendment 09-11-01 !status work item 09-11-01 !status received 09-11-01 !priority Medium !difficulty Medium !subject Aspect Specifications !summary To support the specification of pre- and postconditions, as well as invariants on types and object, we propose a general notation for specifying "aspects" of an entity as part of its declaration, rather than with a separate aspect clause. !problem Specifying aspects for subprograms using an attribute_definition_clause (or other representation or operational item) 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 ::= defining_identifier_list : object_definition [aspect_specification]; | single_task_declaration | single_protected_declaration object_definition ::= [aliased] [constant] subtype_indication [:= expression] | [aliased] [constant] access_definition [:= expression] | [aliased] [constant] array_type_definition [:= expression] full_type_declaration ::= type defining_identifier [known_discriminant_part] is type_definition [aspect_specification]; | task_type_declaration | protected_type_declaration component_declaration ::= defining_identifier_list : component_definition [:= default_expression] [aspect_specification]; subprogram_declaration ::= [overriding_indicator] subprogram_specification [aspect_specification]; abstract_subprogram_declaration := subprogram_specification IS ABSTRACT [aspect_specification]; null_procedure_declaration ::= procedure_specification IS NULL [aspect_specification]; private_type_declaration ::= type defining_identifier [discriminant_part] is [[abstract] tagged] [limited] private [aspect_specification]; private_extension_declaration ::= type defining_identifier [discriminant_part] is [abstract] [limited | synchronized] new ancestor_subtype_indication [and interface_list] with private [aspect_specification]; entry_declaration ::= [overriding_indicator] ENTRY defining_identifier [(discrete_subtype_definition)] parameter_profile [aspect_specification]; [TBD: Should we include package, task, and protected declarations? (Yes.) What about renaming declarations? (Yes or justify.)] 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 Modify 3.9.3(1.1/2): abstract_subprogram_declaration := subprogram_specification IS ABSTRACT [aspect_specification]; Modify 6.1(2/2): subprogram_declaration ::= [overriding_indicator] subprogram_specification [aspect_specification] Modify 6.7(2/2): null_procedure_declaration ::= procedure_specification IS NULL [aspect_specification]; Modify 9.5.2(2/2): entry_declaration ::= [overriding_indicator] ENTRY defining_identifier [(discrete_subtype_definition)] parameter_profile [aspect_specification]; Add the following at the end of 13.1(0.1/1): In addition to representation and operational items, aspects of entities may be specified using an aspect_specification (see 13.3.1), which is an optional element of certain kinds of declarations. Add the following section: 13.3.1 Aspect Specifications [Redundant: Certain representation or operational aspects of an entity may be specified as part of its declaration using an aspect_ specification, rather than using a separate representation or operational item. The declaration with the aspect_specification is termed the *associated declaration*.] Syntax aspect_specification ::= WITH aspect_mark [=> expression] {, aspect_mark [=> expression] } aspect_mark ::= aspect_identifier['Class] [Redundant: The aspect_specification is an optional element in the following kinds of declarations: * object_declaration; * full_type_declaration; * component_declaration; * subprogram_declaration; * abstract_subprogram_declaration; * null_procedure_declaration; * private_type_declaration; * provate_extension_declaration; * entry_declaration. ] Name Resolution The expected type for an expression associated with a given aspect_mark is the type of the identified aspect of the entity defined by the associated declaration (the *associated entity*). The names in such an expression [Redundant: are not resolved at the point of the associated declaration, but rather] are resolved at the end of the immediately enclosing declaration list or at the first freezing point of the associated entity, whichever comes first. If the associated declaration is for a subprogram or entry, the names of the formal parameters are visible within the expression, as are certain attributes, as specified elsewhere in this International Standard for the identified aspect. If the associated declaration is a type_declaration, within the expression the names of any components are visible, and the name of the first subtype denotes the current instance of the type (see 8.6). Legality Rules At most one occurrence of each aspect_mark is allowed within a single aspect_specification. The aspect identified by the aspect_mark shall be an aspect that can be specified for the associated entity. The expression associated with a given aspect_mark may be omitted only when the aspect_mark identifies an aspect of a boolean type, in which case it is equivalent to the expression being specified as True. If the aspect_mark includes 'Class, then the associated entity shall be a tagged type, or the primitive subprogram of a tagged type. Additional legality rules may apply, as specified elsewhere in this International Standard for particular aspects. Static Semantics The identified aspect of the associated entity is as specified by the expression (or by the default of True when boolean). If the aspect_mark includes 'Class, then: * if the associated entity is a tagged type, the specification applies to all descendants of the type; * if the associated entity is a primitive subprogram of a tagged type T, the specification applies to the corresponding primitive subprogram of all descendants of T. Dynamic Semantics At the freezing point of the associated entity, the aspect_specification is elaborated. The elaboration of the aspect_specification includes the evaluation of the expression, if the corresponding aspect is a value rather than an expression. If the corresponding aspect is an expression, the elaboration has no effect. !discussion This syntax was invented to allow pre- and postconditions to be specified for subprograms without worrying about overloading, and without resorting to pragmas. The syntax allows additional aspect names to be added without introducing additional reserved words. Various uses are imagined over and above pre- and postconditions. Here are a number of examples: function Pop(S : in out Stack) return Elem with Pre => not Is_Empty(S), Post => not Is_Full(S); type Atomic_Array is array(Positive range <>) of Natural with Atomic_Components; type Set is interface with Invariant'Class => (Is_Empty(X)) = (Count(X) = 0); function Union(X, Y : Set) return Set is abstract with Post'Class => Count(Union'Result) = Count(X) + Count(Y); type R is record X : Positive := 0 with Independent; -- Independence? Y : Natural := 77 with Atomic; -- Atomicity? end record; type Shared_Bit_Vector is array(0..15) of Boolean with Packing, Independent_Components; type Bit_Vector is array(0..15) of Boolean with Component_Size => 1; This presumes that aspect identifiers generally match attribute names or pragma names. However, particularly in the case of pragmas, we may prefer to choose nouns rather than adjectives for aspect names, so the names work better after the preposition "with". Hence, perhaps "Atomicity" or "Independence" rather than "Atomic" and "Independent." We use "'Class" as an indication that the aspect specification applies to all descendants of the type, or for a subprogram, the corresponding primitive subprogram for all descendants of the type. Other alternatives would be names such as "Inherited_Pre", but Pre'Class meaning it applies to T'Class seems more natural. Much of the semantics is left to the particular aspects, as it is hard to talk about such things in a general way. !example (See discussion.) !ACATS test !appendix ****************************************************************