!standard 6.1.2(0) 21-01-14 AI12-0079-3/07 !class Amendment 19-10-05 !status Amendment 1-2012 20-03-11 !status ARG Approved 11-0-3 20-03-11 !status work item 19-10-05 !status received 19-10-05 !priority High !difficulty Hard !subject Global-in and global-out annotations !summary Annotations are provided to describe the use of global objects by subprograms, entries, tasks, and protected units, with a default specifiable at the library unit level. A new section in the Core of the Standard defines the Global and Global'Class aspects. In Annex H, two restrictions are defined to enforce stricter requirements on the completeness of the global aspects, along with some additional capabilities for the global aspects to provide more precision regarding use of generic formal parameters and dispatching calls. !problem Here is the original problem statement: Ada 2012 added many kinds of assertions to Ada in order to increase the ability of a programmer to specify contracts for types and subprograms. These contracts are defined to be checked at runtime, but are intended to be potentially checked (at least in part) statically. However, without knowledge of side effects of functions used in the aspects, a tool has to assume the worst about any user-defined functions. For example, that the result of a function can change even when called with the same operands. Other assumptions could cause incorrect programs to be accepted as correct, and if the assumptions were used to omit "proved" aspects, to cause erroneous execution. Both of these results are unacceptable for a feature intended to improve the correctness of programs. The worst-case assumptions pretty much prevent any analysis unless the bodies of any user-defined functions used in the aspects are available. This is troublesome, as it prevents analysis of programs as they are constructed. If the body is not available, no analysis is possible. Moreover, analysis depending on a body requires creating implicit body dependencies (if the body is changed, any analysis depending on the properties of that body would have to be performed again). Ideally, analysis at the initial compile-time of a unit would be possible, as it is important to detect errors as soon as possible. More information about function side effects is needed in the specification of subprograms in order to accomplish that goal. --- Additional challenges addressed in this version of the AI: Simplify the proposal, at least in the core, so few if any Global aspects need to be specified by the typical user. Provide a way for more advanced users to impose on themselves stricter requirements should they so choose, but minimize the burden on programmers who want to use the new features of Ada 202X without worrying about Global specifications. Allow more sophisticated implementations, like the SPARK tools, to do additional analysis without requiring the user to specify explicitly all of the Global effects. In so far as possible, achieve compatibility with use of Global in existing SPARK code, so that no significant change in syntax or semantics is required for existing SPARK code to make it Ada 202X compatible. !proposal (See summary.) !wording Add the following section: 6.1.2 The Global and Global'Class Aspects For a subprogram, an entry, an access-to-subprogram type, a task unit, a protected unit, or a library package or generic library package, the following language-defined aspect may be specified with an aspect_specification (see 13.1.1): Global The syntax for the aspect_definition used to define a Global aspect is as follows: global_aspect_definition ::= NULL | Unspecified | global_group_designator | global_mode global_designator | (global_aspect_element{, global_aspect_element}) | extended_global_aspect_definition -- see H.7 global_aspect_element ::= global_mode global_set | extended_global_aspect_element -- see H.7 global_mode ::= basic_global_mode | extended_global_mode -- see H.7 basic_global_mode ::= IN | IN OUT | OUT global_set ::= global_designator {, global_designator} global_designator ::= global_group_designator | global_name global_group_designator ::= ALL | SYNCHRONIZED global_name ::= /object_/name | /package_/name The Global aspect identifies the set of variables (which, for the purposes of this clause includes all constants with some part being immutably limited, or of a controlled type, private type, or private extension) that are global to a callable entity or task body, and that are read or updated as part of the execution of the callable entity or task body. If specified for a protected unit, it refers to all of the protected operations of the protected unit. Constants of any type may also be mentioned in a Global aspect. If not specified or otherwise defined below, the aspect defaults to the Global aspect for the enclosing library unit if the entity is declared at library level, and to Unspecified otherwise. If not specified for a library unit, the aspect defaults to Global => NULL for a library unit that is declared Pure, and to Global => Unspecified otherwise. For a dispatching subprogram, the following language-defined aspect may be specified with an aspect_specification (see 13.1.1): Global'Class The syntax for the aspect_definition used to define a Global'Class aspect is the same as that defined above for global_aspect_definition. This aspect identifies an upper bound on the set of variables global to a dispatching operation that can be read or updated as a result of a dispatching call on the operation. If not specified, the aspect defaults to the Global aspect for the dispatching subprogram. Name Resolution Rules A global_name shall resolve to statically denote an object or a package (including a limited view of a package). Static Semantics A global_aspect_definition defines the Global or Global'Class aspect of some entity. The Global aspect identifies the sets of global variables that can be read, written, or modified as a side effect of executing the operation(s) associated with the entity. The Global'Class aspect associated with a dispatching operation of type T represents a restriction on the Global aspect on a corresponding operation of any descendant of type T. The Global aspect for a callable entity defines the global variables that might be referenced as part of a call on the entity, including any assertion expressions that might be evaluated as part of the call, including preconditions, postconditions, predicates, and type invariants. The Global aspect for an access-to-subprogram object (or subtype) identifies the global variables that might be referenced when calling via the object (or any object of that subtype) including assertion expressions that apply. For a predefined operator of an elementary type, or the function representing an enumeration literal, the Global aspect is NULL. For a predefined operator of a composite type, the Global aspect of the operator defaults to that of the enclosing library unit (unless a Global aspect is specified for the type -- see H.7). The following is defined in terms of operations; the rules apply to all of the above kinds of entities. The global variables associated with any global_mode can be read as a side effect of an operation. The IN OUT and OUT global_modes together identify the set of global variables that can be updated as a side effect of an operation. Creating an access-to-variable value that designates an object is considered an update of the designated object, and creating an access-to-constant value that designates an object is considered a read of the designated object. The overall set of objects associated with each global_mode includes all objects identified for the mode in the global_aspect_definition. A global_set identifies a global variable set as follows: * ALL identifies the set of all global variables; * SYNCHRONIZED identifies the set of all synchronized variables (see 9.10), as well as variables of a composite type all of whose non-discriminant subcomponents are synchronized; * global_name{, global_name} identifies the union of the sets of variables identified by the global_names in the list, for the following forms of global_name: + /object_/name that identifies the specified global variable (or constant); + /package_/name identifies the set of all variables declared in the private part or body of the package, or anywhere within a private descendant of the package. Legality Rules Within a global_aspect_definition, a given global_mode shall be specified at most once. Similarly, within a global_aspect_definition, a given entity shall be named at most once by a global_name. If an entity (other than a library package or generic library package) has a Global aspect other than Unspecified or IN OUT ALL, then the execution of the associated operation(s) shall read only those variables global to the entity that are within the global variable set associated with the IN, IN OUT, or OUT global_modes, and the operation(s) shall update only those variables global to the entity that are within the global variable set associated with either the IN OUT or OUT global_modes. In the absence of the No_Hidden_Indirect_Globals restriction (see H.4), this ignores objects reached via a dereference of an access value. The above rule includes any possible Global effects of calls occurring during the execution of the operation, except for the following excluded calls: * calls to formal subprograms; * calls associated with operations on formal subtypes; * calls through formal objects of an access-to-subprogram type; * calls through access-to-subprogram parameters; * calls on operations with Global aspect Unspecified. The possible Global effects of these excluded calls (other than those that are Unspecified) are taken into account by the caller of the original operation, by presuming they occur at least once during its execution. For calls that are not excluded, the possible Global effects of the call are those permitted by the Global aspect of the associated entity, or by its Global'Class aspect if a dispatching call. AARM Ramification: For a predefined equality operator of a composite type, the possible Global effects includes those of the equality operations invoked as part of the evaluation of the operator (which might not be predefined and thus might have a different Global specification than the component types). If a Global aspect other than Unspecified or IN OUT ALL applies to an access-to-subprogram type, then the prefix of an Access attribute_reference producing a value of such a type shall denote a subprogram whose Global aspect is not Unspecified and is /covered/ by that of the result type, where a global aspect G1 is /covered/ by a global aspect G2 if the set of variables that G1 identifies as readable or updatable is a subset of the corresponding set for G2. Similarly on a conversion to such a type, the operand shall be of a named access-to-subprogram type whose Global aspect is covered by that of the target type. For a subprogram that is a dispatching operation of a tagged type T, each mode of its Global aspect shall identify a subset of the variables identified by the corresponding mode, or by the IN OUT mode, of the Global'Class aspect of a corresponding dispatching subprogram of any ancestor of T, unless the aspect of that ancestor is Unspecified. Implementation Permissions An implementation need not require that all references to a constant object be accounted for by the Global or Global'Class aspect when it is considered a variable in the above rules if the implementation can determine that the object is in fact immutable. Implementations may perform additional checks on calls to operations with an Unspecified Global aspect to ensure that they do not violate any limitations associated with the point of call. AARM Discussion: In this sense, Global => Unspecified is not permission to violate the caller's Global restrictions. It is rather that the implementor of the subprogram is presuming other means are being used to ensure safety. Note the No_Unspecified_Globals Restriction (H.4), which prevents the use of Unspecified with the Global aspect in a given partition. Implementations may extend the syntax or semantics of the Global aspect in an implementation-defined mannerRedundant[; for example, supporting additional global_modes]. AARM Reason: This is intended to allow preexisting usages from SPARK 2014 to remain acceptable in conforming implementations, as well as to provide flexibility for future enhancements. Note the word “extend” in this permission; we expect that any aspect usage that conforms with the (other) rules of this clause will be accepted by any full Ada implementation, regardless of any implementation-defined extensions. NOTES 7 For an example of the use of these aspects and attributes, see the Vector container definition in A.18.2. ---- Add after H.4 (23): No_Unspecified_Globals No library-level entity shall have a Global aspect of Unspecified, either explicitly or by default. No library-level entity shall have a Global'Class aspect of Unspecified, explicitly or by default, if it is used as part of a dispatching call. AARM Ramification: Global'Class need not be specified on an operation if there are no dispatching calls to the operation, or if all of the dispatching calls are covered by dispatching_operation_specifiers for operations with such calls (see H.7). No_Hidden_Indirect_Globals When within a context where the applicable Global aspect is neither Unspecified nor IN OUT ALL, any execution within such a context does neither of the following: * Update a variable that is reachable via a sequence of zero or more dereferences of access-to-object values from a formal parameter of mode IN (after any OVERRIDING -- see H.7), or from a global that is not within the applicable global variable set, or has mode IN; * Read a variable that is updatable via a sequence of zero or more dereferences of access-to-object values from a global that is not within the applicable global variable set. AARM Ramification: The above two rules specify that any indirect references are covered by the Global or formal parameter modes that apply, and are *not* subject to alternative paths of access (such as aliasing) that could result in conflicts. For the purposes of the above rules, if an applicable global variable set includes a package name, and the collection of some pool-specific access type (see 7.6.1) is implicitly declared in a part of the declarative region of the package included within the global variable set, then all objects allocated from that collection are considered included within the global variable set. The consequences of violating the No_Hidden_Indirect_Globals restriction is implementation-defined. Any aspects or other means for identifying such violations prior to or during execution are implementation-defined. AARM Discussion: We do not make violations automatically erroneous, because if the implementation chooses to never fully trust it, there is nothing erroneous that can happen. If an implementation chooses to trust the restriction, and performs some optimization as a result of the restriction, the implementation would define such a violation as erroneous. Such an implementation might also endeavor to detect most violations, perhaps by providing additional aspects, thereby reducing the situations which result in erroneous execution. Implementations might detect some but not all violations of the restrictions. Implementations that completely ignore the restriction should treat the restriction as an unsupported capability of Annex H. Add the following section: H.7 Extensions to Global and Global'Class Aspects In addition to the entities specified in 6.1.2, the Global aspect may be specified for a subtype (including a formal subtype), formal package, formal subprogram, and formal object of an anonymous access-to-subprogram type. Syntax The following additional syntax is provided for specifying Global and Global'Class aspects, to more precisely describe the use of generic formal parameters and dispatching calls within the execution of an operation: extended_global_aspect_definition ::= USE formal_parameter_designator | DO dispatching_operation_specifier extended_global_aspect_element ::= USE formal_parameter_set | DO dispatching_operation_set extended_global_mode ::= OVERRIDING basic_global_mode formal_parameter_designator ::= formal_group_designator | formal_parameter_name formal_parameter_set ::= formal_group_designator | formal_parameter_name{, formal_parameter_name} formal_group_designator ::= NULL | ALL formal_parameter_name ::= /formal_/subtype_mark | /formal_subprogram_/name | /formal_access_to_subprogram_object_/name dispatching_operation_set ::= dispatching_operation_specifier{, dispatching_operation_specifier} dispatching_operation_specifier ::= /dispatching_operation_/name (/object_/name) Name Resolution Rules A formal_parameter_name shall resolve to statically denote a formal subtype, a formal subprogram, or a formal object of an anonymous access-to-subprogram type. The /object_/name that is associated with an OVERRIDING mode shall resolve to statically denote a formal object, or a formal parameter of the associated entity. The /object_/name of a dispatching_operation_specifier shall resolve to statically name an object (including possibly a formal parameter) of a tagged class-wide type T'Class; the /dispatching_operation_/name of the dispatching_operation_specifier shall resolve to statically denote a dispatching operation associated with T. Static Semantics The presence of the reserved word OVERRIDING in a global mode indicates that the specification is overriding the mode of a formal parameter with another mode to reflect the overall effect of an invocation of the callable entity on the state associated with the corresponding actual parameter. The extended_global_aspect_definition and extended_global_aspect_element can be used to define as part of the Global aspect the *formal parameter set* and the *dispatching operation set* used within an operation. The formal parameter set is identified by a set of formal parameter names after the reserved word USE. Alternatively, the reserved word NULL may be used to indicate none of the generic formal parameters, or ALL to indicate all of the generic formal parameters, of any enclosing generic unit (or visible formal package) might be used within the execution of the operation. If there is no formal parameter set specified for an operation declared within a generic unit, it defaults to USE ALL. The dispatching operation set is identified by a set of dispatching_operation_specifiers after the reserved word DO. It indicates that the Global effects of dispatching calls that *match* one of the specifiers need not be accounted for by other elements of the Global aspect, but are instead to be accounted for by the invoker of the operation. A dispatching call *matches* a dispatching_operation_specifier if the name or prefix of the call statically denotes the same operation(s) as that of the dispatching_operation_specifier, and at least one of the objects controlling the call is denoted by a name that statically names the same object as that denoted by the /object_/name of the dispatching_operation_specifier. In the absence of any dispatching_operation_specifiers, all dispatching calls within the operation are presumed to have the effects determined by the set of Global'Class aspects that apply to the invoked dispatching operation. AARM Ramification: The object "controlling the call" is not necessarily a controlling parameter of the call if the call is a function with a controlling result or has parameters that is such a function. It *is* one of the objects that provide the dispatching tag used for the call; that could, for example, be a parameter of a function used as a parameter to the call, or an object being assigned to, or a parameter of an enclosing call. End AARM Ramification. The Global aspect for a subtype identifies the global variables that might be referenced during default initialization, adjustment as part of assignment, finalization of an object of the subtype, or conversion to the subtype, including the evaluation of any assertion expressions that apply. If not specified for the first subtype of a derived type, the aspect defaults to that of the ancestor subtype; if not specified for a nonderived first subtype the aspect defaults to that of the enclosing library unit. If not specified for a nonfirst subtype S, the Global aspect defaults to that of the subtype identified in the subtype_indication defining S. The Global'Class aspect may be specified for the first subtype of a tagged type T, indicating an upper bound on the Global aspect of any descendant of T. If not specified, it defaults to Unspecified. Legality Rules For a tagged subtype T, each mode of its Global aspect shall identify a subset of the variables identified by the corresponding mode, or by the in out mode, of the Global'Class aspect of the first subtype of any ancestor of T. If the formal parameter set is anything but ALL in the Global aspect for an operation declared within a generic unit, then the only generic formal subtypes that may be used, the only formal subprograms that may be called, and the only formal objects of an anonymous access-to-subprogram type that may be dereferenced as part of a call or passed as the actual for an access parameter, are those included in the formal parameter set. Any dispatching call occurring within the operation that does not match a dispatching_operation_specifier is checked using the Global'Class aspect(s) applicable to the dispatching operation; if there is a match, there is no checking against other elements of the Global aspect(s) applicable at the point of call. !discussion Global annotations are critical to being able to perform any sort of modular static analysis. The intent is that all of the global IN, IN OUT, OUT, USE, and DO annotations proposed can be statically checked. This new version of this AI incorporates changes defined by AI12-0240-6 (overriding), AI12-0303-1 (mutable constants), AI12-0310-1 (package private part), and AI12-0334-2 (subtypes and predicates). In this new version, we have dropped the notion of a Global attribute (i.e. X'Global) in favor of somewhat different defaults, and have incorporated more precise forms of Global aspect elements (USE ... and DO ...) into the High-Integrity Annex H where they need not be supported in initial implementations of the new standard. We have also added two restrictions in H.4, one to enable a user to disallow use of the new Unspecified value for the Global aspect for any library-level entities, and one to enable a user to indicate that all objects reached via access values are covered by the formal parameter or Global aspect modes. We allow Global specifications on packages or generic packages only if they are library units, analogous to the same limitation of where Pure can be specified, to establish a default for library-level entities. More details on the new defaults are detailed below. The overall goal is that a programmer who specifies nothing gets something reasonable. Another goal is that existing SPARK programs use of Global should be acceptable largely as is, except for the slight change in syntax to use reserved words "IN" and "OUT" rather than the non-reserved "Input", "In_Out", and "Output" currently used in the SPARK Global aspect. In any case, a compiler could accept both the old syntax and the new syntax, as they are unambiguously distinguishable at compile time. The most critical new "default" in this new version is that entities not within a declared-pure library unit, or not at library-level, have Unspecified as their default Global aspect. This effectively implies that the caller may assume the best, but no checking is necessarily being performed at the point of call (though implementations are permitted to effectively inline the call to do additional checks). We provide a restriction of No_Unspecified_Globals in Annex H to allow a user to disallow any library-level entities with Global => Unspecified within a partition. Note that for non library-level entities, even if their own Global aspect is Unspecified, they must still honor any Global aspects of lexically enclosing entities, if these entities have an explicit or implicit Global aspect other than Unspecified. For example, a nested subprogram with Global => Unspecified still cannot violate the Global aspect of its enclosing subprogram, so if the enclosing subprogram specifies Global => SYNCHRONIZED, the nested subprogram cannot reference a variable that is global to its enclosing subprogram unless it is synchronized. It *may* reference variables local to its enclosing subprogram with no restrictions. The other critical new "default" is that entities declared within a generic unit are presumed to make use of *all* generic formal parameters associated with any enclosing generic unit, while not worrying about any of the possible Global effects of that usage in their Global aspect. These additional effects are handled at the point of instantiation, rather than at the point of definition of the generic, much in the same way that "purity" of an instantiation is determined by a combination of the "purity" of the generic and the purity of the actual parameters to the generic. In annex H, we provide ways to specify upper bounds on the effects of generic formal parameters, and we provide an ability to limit which generic formal parameters are actually used within an entity defined within a generic unit (USE formal_parameter_name, ...). This allows us to say that all entities declared at library level within a declared-pure library unit default to Global => null, even if they are within a generic unit, because the USE ALL is implicit for such entities. We have also included in Annex H an ability to specify that certain dispatching calls might be performed as part of the execution of an entity, allowing the invoker to more precisely deal with the possible effects of such a call, rather than the entity itself having to fall back on the Global'Class effects, which are likely to be very pessimistic, if specified at all. Some overall notes on the above: This version of this AI was based on work done by Tuck and Claire to reach some kind of simpler consensus position on Global. Probably the biggest change that came from that work was the introduction of the notion of Global => Unspecified to better match existing SPARK usage where few if any Global specifications are required. We have coupled that with a restriction No_Unspecified_Globals to accommodate those users who want to impose on themselves a requirement to specify Global, explicitly or implicitly, at least on all library-level entities. A related change was to move concerns about use of generic formals to the point of instantiation, so operations in a "pure" generic unit can be (implicitly or explicitly) simply "Global => null". The additions relative to the consensus report are relatively few. We have held on to a way to establish an overall default, but we now limit it to a library unit as a whole, as that is the level at which Pure can be declared, and the default only applies to library-level elements, not to any non library-level declarations. Non library-level entities always default to Global => Unspecified, but we believe that that is not a significant loss in functionality, as these nested entities must still abide by any Global aspect of their enclosing library-level entity. As proposed in our consensus document, we have allowed all dereferences of access values to be ignored in the Global aspect. However in this AI we allow the user to specify a restriction stating that in fact all such dereferences are accounted for by Globals or parameters. We do not specify how that claim should be enforced. Implementations have to define how they deal with violations of the No_Hidden_Indirect_Globals restriction; however, ignoring it completely means the capability is not supported, and should be identified by the implementation as such. We have eliminated the need for a Global attribute (X'Global) and moved all functionality that depended on that into Annex H. We have ensured that the functionality in the Annex is optional in the sense that it only adds precision; it doesn't provide critical functionality for typical use. Certain of the language-defined packages (such as those related to streaming) might use these features to describe their effects more precisely, but implementations that do not support these Annex H features can choose how to reflect the Global effects of these language-defined packages in a way that is appropriate to typical usage patterns. !example For an example of the use of these aspects and attributes, see the Vector container definition in A.18.2 (of draft 25 or later). !corrigendum 6.1.2(0) @dinsc Dummy to force a conflict; the wording changes are in the conflict file. !corrigendum H.4(23) @dinsa @xhang<@xtermDuring the execution of a subprogram by a task, no other task invokes the same subprogram.> @dinss @xhang<@xterm> Find the rest in the conflict file. !corrigendum H.7(0) @dinsc In addition to the entities specified in 6.1.2, the Global aspect may be specified for a subtype (including a formal subtype), formal package, formal subprogram, and formal object of an anonymous access-to-subprogram type. @s8<@i> The following additional syntax is provided for specifying Global and Global'Class aspects, to more precisely describe the use of generic formal parameters and dispatching calls within the execution of an operation: @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @ @b @fa@hr @ @ |@ @b @fa> @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @ @b @fa@hr @ @ |@ @b @fa> @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @ @b @fa> @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @ @fa@hr @ @ |@ @fa> @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @ @fa@hr @ @ |@ @fa{, @fa}> @xindent<@fa@fa<@ ::=@ >@b | @b> @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @ @i@fa@hr @ @ |@ @i@fa@hr @ @ |@ @i@fa> @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @ @fa{, @fa}> @xindent<@fa@fa<@ ::=@ >@hr @ @ @ @ @i@fa (@i@fa)> @s8<@i> A @fa shall resolve to statically denote a formal subtype, a formal subprogram, or a formal object of an anonymous access-to-subprogram type. The @i@fa that is associated with an @b mode shall resolve to statically denote a formal object, or a formal parameter of the associated entity. The @i@fa of a @fa shall resolve to statically name an object (including possibly a formal parameter) of a tagged class-wide type @i'Class; the @i@fa of the @fa shall resolve to statically denote a dispatching operation associated with @i. @s8<@i> The presence of the reserved word @b in a global mode indicates that the specification is overriding the mode of a formal parameter with another mode to reflect the overall effect of an invocation of the callable entity on the state associated with the corresponding actual parameter. The @fa and @fa can be used to define as part of the Global aspect the @i and the @i used within an operation. The formal parameter set is identified by a set of formal parameter names after the reserved word @b. Alternatively, the reserved word @b may be used to indicate none of the generic formal parameters, or @b to indicate all of the generic formal parameters, of any enclosing generic unit (or visible formal package) might be used within the execution of the operation. If there is no formal parameter set specified for an operation declared within a generic unit, it defaults to @b. The dispatching operation set is identified by a set of @fas after the reserved word @b. It indicates that the Global effects of dispatching calls that @i one of the specifiers need not be accounted for by other elements of the Global aspect, but are instead to be accounted for by the invoker of the operation. A dispatching call @i a @fa if the @fa or @fa of the call statically denotes the same operation(s) as that of the @fa, and at least one of the objects controlling the call is denoted by a name that statically names the same object as that denoted by the @i@fa of the @fa. In the absence of any @fas, all dispatching calls within the operation are presumed to have the effects determined by the set of Global'Class aspects that apply to the invoked dispatching operation. The Global aspect for a subtype identifies the global variables that might be referenced during default initialization, adjustment as part of assignment, finalization of an object of the subtype, or conversion to the subtype, including the evaluation of any assertion expressions that apply. If not specified for the first subtype of a derived type, the aspect defaults to that of the ancestor subtype; if not specified for a nonderived first subtype the aspect defaults to that of the enclosing library unit. If not specified for a nonfirst subtype @i, the Global aspect defaults to that of the subtype identified in the @fa defining @i. The Global'Class aspect may be specified for the first subtype of a tagged type @i, indicating an upper bound on the Global aspect of any descendant of @i. If not specified, it defaults to Unspecified. @s8<@i> For a tagged subtype @i, each mode of its Global aspect shall identify a subset of the variables identified by the corresponding mode, or by the @b mode, of the Global'Class aspect of the first subtype of any ancestor of @i. If the formal parameter set is anything but @b in the Global aspect for an operation declared within a generic unit, then the only generic formal subtypes that may be used, the only formal subprograms that may be called, and the only formal objects of an anonymous access-to-subprogram type that may be dereferenced as part of a call or passed as the actual for an access parameter, are those included in the formal parameter set. Any dispatching call occurring within the operation that does not match a @fa is checked using the Global'Class aspect(s) applicable to the dispatching operation; if there is a match, there is no checking against other elements of the Global aspect(s) applicable at the point of call. !ASIS New functions will be needed. Details still to be determined. !ACATS test ACATS tests should be created to test that the new annotations are correctly enforced. !appendix From: Tucker Taft Sent: Sunday, February 9, 2020 2:18 PM Here is a modest reformulation of the Global aspect as defined by AI12-0079-2. The main change is to remove all access-type checking from the core, and add a restriction called "No_Hidden_Indirect_Globals" to H.4 which a user can specify to indicate that in fact all references via a sequence of access value dereferences are actually covered by Global or formal parameter modes that apply to the starting point of the sequence. Implementations must define the consequences of violating the restriction -- such violations could be erroneous, or they could be ignored, or the implementation could in fact detect the violations at compile time or run time, probably by relying on additional aspect specifications and/or run-time checks. Comments, questions, fixes, etc. welcome. Hopefully this will be a topic at the upcoming ARG phone meeting in March. [This is version /01 of the AI - Editor.] **************************************************************** From: Richard Wai Sent: Sunday, February 9, 2020 3:38 PM I think "No_Hidden_Indirect_Globals" is an elegant way to bring global contracts into Ada, without being too ambitious or onerous with the peculiarities of indirection. However, I'm a little uncomfortable with a restriction being defined such that the implementation may "ignore" violations. I think it would be safer if _any_ language defined restriction that is optionally implemented (this being first such restriction) caused any non-supporting implementation to reject the compilation if the unsupported restriction appears. This way the user is fully aware that the restriction is not supported, and if they are ok with that lack of support, can remove the restriction, or use some kind of implementation-specified override (i.e. command-line switches). I think this agrees with higher-level Ada design goals, specifically that a given program should not become less safe simply by using a different (conformant) implementation. The only real trouble this kind of requirement would cause would be a minor inconvenience at compile-time. It seems very un Ada-like to worry about inconveniencing the user during compilation if doing so significantly improves safety and reliability. Implementing this requirement is almost certainly trivial. I'd propose something like this, following paragraph to 13.12, Implementation Permissions (after 9.2/1): [Some language-defined restrictions (not including those defined in the Specialized Needs Annexes), are deemed to be optionally implemented. Support for optionally implemented language-defined restrictions may be omitted from an implementation. If an implementation omits an optionally implemented restriction, it shall reject any compilation containing any of the optionally implemented restrictions that are not implemented.] With the above general requirements of all restrictions, I feel "No_Hidden_Indirect_Globals" should then be more explicitly "all or nothing". If the implementation implements the restriction, then it must promise to detect violations, either at compile time or at run-time. If the implementation decides to not implement the restriction, then as per above, it should reject the compilation outright. Finally, I think No_Hidden_Indirect_Globals then should be more specific about what runtime exception(s) could be expected if the implantation choses to use runtime checking, as this could otherwise impact portability. With all the above, there will be no surprises, or worse, a false sense of security, if a user applies No_Hidden_Indirect_Globals. **************************************************************** From: Tucker Taft Sent: Sunday, February 9, 2020 4:36 PM Thanks for your comments. I am a bit on the fence here. One reason to use the restriction is to indicate that the program was written to conform to this model, and that can be useful independent of whether the restriction is actually enforced. To some extent assertions serve the same purpose when the Assertion_Policy is Ignore. Perhaps we could have a way of saying that the program obeys the restrictions, while acknowledging that they might not be checked (equivalent of Assertion_Policy of Ignore). The presumption is that there might be another kind of tool, other than the compiler, that helps to enforce the restriction. This is how certain other SPARK annotations work in general. The compiler may completely ignore them, leaving therm for the "gnat-prove" tool to enforce. Note that already everything in a specialized-needs annex is "optional" so it would be a bit weird to make something doubly optional. The fact that the consequences of violations are "implementation defined" means that the compiler must come with documentation that indicates how the restriction is enforced, so it becomes a quality-of-implementation issue. I am also very reluctant to try to specify what the consequences should be at this point, given that specifying them could add significant complexity to the standard, and probably not exactly match what any real implementation will do in the near term. I would rather get this restriction out there, and then at some later point think about standardizing the consequences. My guess is that over time tools will get better and better at detecting violations, and trying to anticipate now what they will do or should do is a waste of energy. Having an all or nothing situation seems like a bad approach. I would be happy to see gradually improving support for the restriction. **************************************************************** From: Tucker Taft Sent: Sunday, February 9, 2020 4:42 PM Note that this is somewhat like the situation now with the No_Exceptions restriction, per H.4(25): "If a pragma Restrictions(No_Exceptions) is specified, the implementation shall document the effects of all constructs where language-defined checks are still performed automatically (for example, an overflow check performed by the processor)." The documentation could say that all hell breaks loose if an exception actually gets raised. Or it could give some more reasonable behavior. Since we are requiring implementations to document how they support this newly proposed restriction, a user can decide whether they find it helpful or harmful to specify the restriction. **************************************************************** From: Jean-Pierre Rosen Sent: Monday, February 10, 2020 2:21 AM > Note that already everything in a specialized-needs annex is "optional" > so it would be a bit weird to make something doubly optional. Not really. The annex as a whole is optional, but if you claim conformance, then a number of things are required. **************************************************************** From: Tucker Taft Sent: Monday, February 10, 2020 9:53 AM But there is also the notion of partial support of annex features, per 1.1.3(17): "... However, it shall not provide any aspect, attribute, library unit, or pragma having the same name as an aspect, attribute, library unit, or pragma (respectively) specified in a Specialized Needs Annex unless the provided construct is either as specified in the Specialized Needs Annex or is more limited in capability than that required by the Annex. A program that attempts to use an unsupported capability of an Annex shall either be identified by the implementation before run time or shall raise an exception at run time. " So "limited capability" support of an annex restriction is already fine. **************************************************************** From: Jean-Pierre Rosen Sent: Monday, February 10, 2020 10:11 AM This paragraph says that if you do not claim support to an annex, but just to the core language, you are not allowed to provide an incompatible version of something provided in the annex. You cannot claim conformance to an annex and "pick and choose" any feature from the annex (which you seemed to imply by saying that "everything in a specialized-needs annex is "optional" "). If you don't claim conformance, of course, you can do anything you please, except being incompatible. **************************************************************** From: Richard Wai Sent: Monday, February 10, 2020 10:11 AM > Thanks for your comments.  I am a bit on the fence here.  One reason to > use the restriction is to indicate that the program was written to conform > to this model, and that can be useful independent of whether the restriction > is actually enforced.  To some extent assertions serve the same purpose > when the Assertion_Policy is Ignore.   My reasoning here was that Restriction pragmas, being configuration pragmas, are much heavier, but also less "visible" to the programmer than the scope-based Assertion_Policy pragma, so they aren’t really in the same category. My concern being that one doesn't write pragma Assertion_Policy (Check) and then have the compiler decide by itself to just say "nah, I'll ignore it anyways". So I don't really see the comparison here, since Assertion_Policy Ignore is just a default, but if the user specifies Check, then the compiler cannot optionally ignore it. > Perhaps we could have a way of saying that the program obeys the > restrictions, while acknowledging that they might > not be checked (equivalent of Assertion_Policy of Ignore).  The > presumption is that there might be another kind of > tool, other than the compiler, that helps to enforce the restriction. > This is how certain other SPARK annotations work > in general.  The compiler may completely ignore them, leaving therm > for the "gnat-prove" tool to enforce. This was my reasoning for implementation-specified methods of "overriding" the lack of checking where the unimplemented restriction exists. > Note that already everything in a specialized-needs annex is > "optional" so it would be a bit weird to make something > doubly optional. Indeed, and I made note of that in the additional RM paragraph I have. My reasoning here is not only that Special Needs Annexes are optional, but the configuration pragmas (specifically Restriction pragmas) defined within them are very specific to those Annexes, so users of such Restrictions are expecting the Annex to be implemented. **************************************************************** From: Richard Wai Sent: Monday, February 10, 2020 10:41 AM > But there is also the notion of partial support of annex features, per > 1.1.3(17): > > "... However, it shall not provide any aspect, attribute, library > unit, or pragma having the same name as an aspect, attribute, library > unit, or pragma > (respectively) specified in a Specialized Needs Annex unless the > provided construct is either as specified in the Specialized Needs > Annex or is more limited in capability than that required by the > Annex. A program that attempts to use an unsupported capability of an > Annex shall either be identified by the implementation before run time > or shall raise an exception at run time. " That last part of 1.1.3(17) is interestingly essentially what I was proposing. The Annexes are optional, but if the use tries to use an unsupported capability, the compilation fails or there is an exception at run-time. My original suggestion being exactly that - language defined Restrictions that are "optional" should nevertheless cause the compiler to "identify" any (unsupported) use before run time, or else raise an exception. In the case of SPARK, if the tools could prove the Global aspects, it seems to me that it would satisfy the restriction, and users of SPARK should then be justified to remove the restriction if they are using a compiler that doesn't support that Restriction, or else use the compiler documented overrides. **************************************************************** From: Tucker Taft Sent: Monday, February 10, 2020 11:03 AM I guess I would agree that if the restriction is completely ignored then it should be rejected. But if it is even supported in a very limited way, it serves a purpose. And in any case, expressing the intent to readers of the program is always an important benefit to specifying such a restriction. **************************************************************** From: Randy Brukardt Sent: Monday, February 10, 2020 8:27 PM ... > I think "No_Hidden_Indirect_Globals" is an elegant way to bring global > contracts into Ada, without being too ambitious or onerous with the > peculiarities of indirection. I agree. > However, I'm a little uncomfortable with a restriction being defined > such that the implementation may "ignore" violations. Me too. But in a different way than Richard. Your reason for allowing "ignore the restriction" is that the compiler doesn't take any advantage of the restriction. But the Legality Rules associated with parallel checking are "taking advantage of the restriction". More specifically, if one is desiring to get useful parallel usage checking, it's required to have access types included in the Global specifications. Such a user would use the No_Hidden_Indirect_Globals restriction (and possibly the "No_Unspecified_Globals" restriction as well, depending on the compiler implementation). In such a case, completely ignoring the restriction is wrong. Even a bad (but simple) implementation (for instance, rejecting any dereference outside of "all" or "unspecified") would be preferable to ignoring it. I think it is OK to say that all code that violates the restriction is erroneous (thus giving an incentive to find ways to eliminate that, but still allowing the lazy implementer to do nothing), but to say it is "ignored" sends the wrong message. **************************************************************** From: Randy Brukardt Sent: Monday, February 10, 2020 8:35 PM ... > You cannot claim conformance to an annex and "pick and choose" any > feature from the annex (which you seemed to imply by saying that > "everything in a specialized-needs annex is "optional" "). If you > don't claim conformance, of course, you can do anything you please, > except being incompatible. This is a very important point. Stuff in an Annex is only "optional" if one doesn't support the Annex or if there is an explicit statement that it is optional. You can, for instance, claim support for Annex D and still not support Priority_Specific_Dispatching, because D.2.1(19/2) says it doesn't have to be supported on incompatible targets. On the other hand, claiming support for Annex D and not supporting the EDF policy is not allowed (there's no rule allowing that policy to be optional). [I note that since we were told that no one has supported that policy, that therefore no compiler has ever supported Annex D for Ada 2005 or later, despite vendor claims to the contrary. I'm surprised that no one has ever tried to get the ARG to fix this...] As I noted before, this restriction is integral to having useful parallelism checking within Ada, so it seems rather important that some sort of support is mandated. It's fine to leave the details to the implementation, however. **************************************************************** From: Tucker Taft Sent: Monday, February 10, 2020 10:47 PM > ... > > I think it is OK to say that all code that violates the restriction is > erroneous (thus giving an incentive to find ways to eliminate that, > but still allowing the lazy implementer to do nothing), but to say it > is "ignored" sends the wrong message. Another way to do this is to say that if the parallel Conflict_Check_Policy is anything other than No_Parallel_Conflict_Checks, then any execution in a parallel context that violates the No_Hidden_Indirect_Globals is erroneous. Analogous rules would apply for tasking conflict checks. We should probably also move the Conflict_Check stuff into Annex H. Meaningful conflict checks clearly depend on obeying No_Hidden_Indirect_Globals. **************************************************************** From: Tucker Taft Sent: Thursday, February 13, 2020 7:37 PM Here is a slight update to AI12-0079-3, incorporating suggestions from internal AdaCore review, and from comments here. I have removed the permission to completely ignore the No_Hidden_Indirect_Globals, without identifying it as an unsupported capability. I also made some minor changes to eliminate incompatibilities with SPARK's definition of what is represented by a package name. In particular, public children are considered completely independent of their parent and of each other, even though they do have visibility on the private declarations in the specs of their ancestor units. If a subprogram wants to indicate it depends on the private state of a public child, it can name it explicitly, so I think this approach makes sense. Finally, I moved any mention of dereferences of pool-specific access types to Annex H. It seemed somewhat out of place in the "core" description. I also changed it so it talks in terms of the "collection" associated with the pool-specific access type, which focuses on the allocated objects, rather on the way you denote them. [This is version /02 of the AI.] **************************************************************** From: Christoph Grein Sent: Sunday, February 16, 2020 9:22 AM Excuse me, but I did not follow precisely the whole discussion and I did not really work with SPARK. As fas as I understood, a global variable in SPARK need not really exist in order to not violate privacy. Instead a pseudoname is used that is resolved in the body to existing variables hidden in the body. In this version of the AI, I read in the Name Resolution Rules that a name shall statically denote an object or package. Isn't this a violation of privacy? **************************************************************** From: Tucker Taft Sent: Sunday, February 10, 2020 10:11 AM In SPARK there is the notion of "state abstraction" which can be declared in the package spec and defined in the package body in terms of specific variables. Rather than introducing the full complexity of the state abstraction concept into Ada, we have instead permitted the use of the name of a package to stand in for all of the hidden global state of the package. In SPARK terms, it means the name of the package is treated like an abstract-state identifier that maps to the full set of package-level variables of the package private part and body (and private descendants). **************************************************************** From: Randy Brukardt Sent: Wednesday, February 19, 2020 10:11 PM > Here is a slight update to AI12-0079-3, incorporating suggestions from > internal AdaCore review, and from comments here. ... > !proposal > > ** TBD. Similar to AI12-0079-1 and it's later fixups > (AI12-0240-6 [overriding], AI12-0303-1, AI12-0310-1, and AI12-0334-2), > but with some in the core and some in an annex. Ahem. I don't think this will get past Editorial Review. ;-) Probably you need to replace this with some sort of summary of the proposal. (Perhaps move some of the text about "simplify the proposal" in the !problem here.) The !summary probably also needs an update (not a major change, though). If you put enough detail in the !summary, then "(See summary.)" would be a sufficient !proposal. **************************************************************** From: Tucker Taft Sent: Saturday, February 22, 2020 8:37 AM Here is an updated !summary: Annotations are provided to describe the use of global objects by subprograms, entries, tasks, and protected units, with a default specifiable at the library unit level. A new section in the Core of the Standard defines the Global and Global'Class aspects. In Annex H two restrictions are defined to enforce stricter requirements on the completeness of the global aspects, along with some additional capabilities for the global aspects to provide more precision regarding use of generic formal parameters and dispatching calls. And as you suggest, !proposal will simply be "See !summary." **************************************************************** From: Tucker Taft Sent: Tuesday, March 10, 2020 2:31 PM One minor "typo" in AI12-0079-3. In the 7th paragraph of the !discussion it says "USE => ALL" and it should say merely "USE ALL". I realize you all already caught that subtlety! ;-) **************************************************************** From: Brad Moore Sent: Wednesday, March 11, 2020 1:12 PM The following are my editorial comments for AI12-0079-3 + one for AI12-0363-1 that were not presented during our phone meeting. - AI12-0079-3: Summary: 2nd sentence. "In Annex H{,}" 3rd para, Summary, penultimate sentence. "to {cause} erroneous execution." 4th para. "about function side{-}effects" 4th para. last sentence. "subprograms{, } in order to accomplish that goal." Wording after global_name 1st para. (is also a single sentence, a long one) Can we break it up? Otherwise, quite a mouthful to parse for the reader. Suggest bulletizing. as in; "The Global aspect identifies the set of variables (which, for the purposes of this clause includes all constants with some part being immutably limited, or of a controlled type, private type, or private extension) global to an operation, task unit, or protected unit, that are potentially read or updated as part of the execution of: - the operation; or - the body of the task; or - a protected operation of the protected unit." It feels like the next sentence (beginning with "Constants") should be a new/separate paragraph. 1st AARM Discussion in Implementation Permissions, last sentence. "Note the No_Unspecified_Globals Restriction (H.4){, which prevents}[to prevent] the use of Unspecified with the Global aspect in a given partition." Also, I had a typo in AI12-0363-1, that I didn't mention in our phone meeting. AARM Ramification: 1st sentence, "a subcomponent that is specified to be atomic is considered to also specify that {it} is independently addressable." **************************************************************** From: Tucker Taft Sent: Wednesday, March 11, 2020 4:36 PM Thanks, Brad! A few comments below... ... > - AI12-0079-3: > > Summary: 2nd sentence. "In Annex H{,}" A comma after "In blah ... " seems optional... > 3rd para, Summary, penultimate sentence. "to {cause} erroneous execution." Agreed. > 4th para. "about function side{-}effects" Gary might disagree on this one. ;-) > 4th para. last sentence. "subprograms{, } in order to accomplish that goal." Comma also seems optional here. > Wording after global_name > > 1st para. (is also a single sentence, a long one) Can we break it up? > Otherwise, quite a mouthful to parse for the reader. Suggest > bulletizing. as in; > > "The Global aspect identifies the set of variables (which, for > the purposes of this clause includes all constants with some > part being immutably limited, or of a controlled type, private > type, or private extension) global to an operation, task unit, > or protected unit, that are potentially read or updated as part > of the execution of: > - the operation; or > - the body of the task; or > - a protected operation of the protected > unit." Might want to refactor the sentence a bit. Having done that, the sentence might be short enough to avoid bullet-izing. Perhaps: The Global aspect identifies the set of variables (which, for the purposes of this clause includes all constants with some part being immutably limited, or of a controlled type, private type, or private extension) that are global to a callable entity or task body, and that are read or updated as part of the execution of the callable entity or task body. If specified for a protected unit, it refers to all of the protected operations of the protected unit. > It feels like the next sentence (beginning with "Constants") should be > a new/separate paragraph. Agreed. > 1st AARM Discussion in Implementation Permissions, last sentence. > > "Note the No_Unspecified_Globals Restriction (H.4){, which > prevents}[to prevent] the use of Unspecified with the Global > aspect in a given partition." Fine. > Also, I had a typo in AI12-0363-1, that I didn't mention in our phone > meeting. > > AARM Ramification: 1st sentence, > "a subcomponent that is specified to be atomic is considered to also > specify that {it} is independently addressable." Good catch. **************************************************************** From: Gary Dismukes Sent: Wednesday, March 11, 2020 4:54 PM ... > > - AI12-0079-3: > > > > Summary: 2nd sentence. "In Annex H{,}" > > A comma after "In blah ... " seems optional... FWIW, I would put a comma. > > > > 3rd para, Summary, penultimate sentence. "to {cause} erroneous execution." > > Agreed. > > > > > 4th para. "about function side{-}effects" > > Gary might disagree on this one. ;-) Yep, should be a space, so fine as is. :-) > > 4th para. last sentence. "subprograms{, } in order to accomplish that > > goal." > > Comma also seems optional here. I agree, comma is optional. **************************************************************** From: Brad Moore Sent: Wednesday, March 11, 2020 4:56 PM ... >> 4th para. "about function side{-}effects" > > Gary might disagree on this one. ;-) I thought I was channeling my inner Gary here... :-). But I am not entirely sure. If two or more words serve as a single adjective before a noun, one would generally use a hyphen. Apparently the general rule is that when compound modifiers come after a noun, they are not hyphenated: as in; The peanuts were chocolate covered. The author was well known. But these examples have a verb in-between, so it seems like a different case. I'd be curious to hear what Gary thinks... ... > Might want to refactor the sentence a bit. Having done that, the > sentence might be short enough to avoid bullet-izing. Perhaps: > > The Global aspect identifies the set of variables (which, for > the purposes of this clause includes all constants with some > part being immutably limited, or of a controlled type, private > type, or private extension) that are global to a callable entity > or task body, and that are read or updated as part of the execution > of the callable entity or task body. If specified for a protected unit, > it refers to all of the protected operations of the protected unit. That works for me. **************************************************************** From: Gary Dismukes Sent: Wednesday, March 11, 2020 5:40 PM > >> 4th para. "about function side{-}effects" > > > > Gary might disagree on this one. ;-) > > I thought I was channeling my inner Gary here... :-). > > But I am not entirely sure. If two or more words serve as a single > adjective before a noun, one would generally use a hyphen. Apparently > the general rule is that when compound modifiers come after a noun, > they are not hyphenated: as in; > > The peanuts were chocolate covered. > The author was well known. > > But these examples have a verb in-between, so it seems like a different case. > > I'd be curious to hear what Gary thinks... The noun here is "side effects" (a compound noun, but one that is normally spelled with a space), which is modified by the adjective "function", so a hyphen isn't appropriate here. OTOH, if it was "side-effect function", then a hyphen would be appropriate. :-) **************************************************************** From: Brad Moore Sent: Thursday, March 12, 2020 10:19 AM > The noun here is "side effects" (a compound noun, but one that is > normally spelled with a space), which is modified by the adjective > "function", so a hyphen isn't appropriate here. OTOH, if it was > "side-effect function", then a hyphen would be appropriate. :-) Of course you are correct! and thanks for the explanation. **************************************************************** From: Randy Brukardt Sent: Sunday, March 22, 2020 8:08 PM The meeting minutes say we need to add a rule for access-to-subprogram types. Tucker provided the following: Add to the Legality Rules immediately after the AARM Ramification about equality operators: If a Global aspect other than Unspecified or IN OUT ALL applies to an access-to-subprogram type, then the prefix of an Access attribute_reference producing a value of such a type shall denote a subprogram whose Global aspect is not Unspecified and is /covered/ by that of the result type, where a global aspect G1 is /covered/ by a global aspect G2 if the set of variables that G1 identifies as readable or updatable is a subset of the corresponding set for G2. Similarly on a conversion to such a type, the operand shall be of a named access-to-subprogram type whose Global aspect is covered by that of the target type. Tucker also noticed that we're missing a rule. If the user writes Global => all or Global => synchronized the intent was to interpret that as "in out all" or "in out synchronized". He suggested adding the following to the paragraph immediately following the BNF: If a global_aspect_definition consists of a single global_group_designator, the global_mode is implicitly IN OUT. This second change seems to be a clear oversight that should not be controversial, so I am processing it as an Editorial Review change. **************************************************************** Editor's note: Not everyone agreed with me on the idea that this second topic was a clear oversight, so that topic is now in AI12-0375-1. **************************************************************** Editor's notes: [May 8th, 2020] The following non-trival editorial review changes were made to this AI (with concurrence from Tucker Taft): (1) The "implementation_defined_mode" production and rules were removed. These are covered by the blanket permission to extend the syntax, and thus were redundant with that permission. In addition, there was no definition of the non-terminal "implementation_defined_mode", which violates the construction standards of the RM. A suggestion of additional global_modes as an application of that permission is added to the permission. (2) Only calls with parameters have a prefix, so the third paragraph of the Static Semantics of H.7 needs to say "name or prefix" in order that we are supporting parameterless function calls (which can be dispatching). We use "name or prefix" as that is the order used in 6.4 (Subprogram Calls). We also add an AARM note to clarify that the object in question is the one that controls the call, which may not directly be a controlling parameter of the call (in cases where functions with controlling results are involved). (3) In that same paragraph, we change "statically denotes" to "statically names" for the object_name, as we want the widest possible application. (Statically names allows record components and static array indexing, while statically denotes does not.) The last paragraph of the resolution rules is updated the same way. **************************************************************** From the AARM review of Steve Baird, October 2020 In 6.1.1's first paragraph, when listing all the constructs for which these aspects can be specified, we say "an access-to-subproram type". The analogous wording in 6.1.2 for Globals says "a named access-to-subprogram type". They should be consistent. We probably want to add the word "named" in 6.1.1 . [Editor's response: I'd expect that we'd want to specify these for anonymous access types if we had a syntax for doing so. So I don't see much point in making future (and/or implementer-defined stuff) harder. If I was going to do anything, I'd remove "named" from 6.1.2. Tucker concurs with me. This was processed as an editorial review on AI12-0079-3.] Commas look odd in 6.1.2(40/5): Implementations need not require that references to a constant object that are considered variables in the above rules, be accounted for by the Global or Global'Class aspect, if the implementation can determine that the constant object is immutable. [Editor's response: To me, it looks like some words are missing. Tucker says it is correct, but hard to parse. He suggests reordering it and making most of the uses singular: An implementation need not require that all references to a constant object be accounted for by the Global or Global'Class aspect when it is considered a variable in the above rules if the implementation can determine that the object is in fact immutable. This was applied as an Editorial Review change in AI12-0079-3. End Editor's Response.] ****************************************************************