CVS difference for ai12s/ai12-0079-2.txt
--- ai12s/ai12-0079-2.txt 2019/10/18 05:03:35 1.1
+++ ai12s/ai12-0079-2.txt 2020/01/14 02:42:17 1.2
@@ -1,4 +1,4 @@
-!standard 6.1.2(0) 19-10-05 AI12-0079-2/00
+!standard 6.1.2(0) 20-01-13 AI12-0079-2/01
!class Amendment 19-10-05
!status work item 19-10-05
!status received 19-10-05
@@ -8,36 +8,55 @@
!summary
-Annotations are provided to describe the use of global objects by subprograms.
+Annotations are provided to describe the use of global objects by
+subprograms, entries, tasks, and protected units.
!problem
-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 erroneous execution.
-Both of these results are unacceptable for a feature intended to improve the
+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 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
-bad, 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 pseudo body dependencies (if the body is changed, any analysis
-depending on the properties of that body would have to be performed again); but
-the language does not allow these to be "real" body dependencies (any
-recompilation needed has to occur automatically).
-
-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.
+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
@@ -46,20 +65,620 @@
and some in an annex.
!wording
+
+Add the following section:
-** TBD.
+6.1.2 The Global and Global'Class Aspects
+For a subprogram, an entry, a named access-to-subprogram type, a task
+unit, a protected unit, or a library package or generic 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 ::=
+ [ OVERRIDING ] basic_global_mode
+ | implementation_defined_mode
+
+ 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 | ALIASED
+
+ 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) global to an operation, task unit,
+ or protected unit, that are potentially read or updated as part
+ of the execution of the operation or of the execution of
+ the body of the task or a protected operation 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. The presence of the reserved word OVERRIDING
+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.
+
+An implementation-defined global_mode may be specified, which limits the
+use of the global objects to which it applies according to an
+implementation-defined rule.
+
+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;
+
+ * ALIASED identifies the set of all aliased variables, which
+ includes any dereference of a value of an access-to-object type;
+
+ * 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 is not associated with an OVERRIDING mode
+ identifies the specified global variable (or constant);
+
+ + /object_/name that is associated with an OVERRIDING mode identifies
+ the variable parts associated with the specified formal parameter
+ whose parameter mode is being overridden;
+
+ + /package_/name identifies the set of all variables declared in the
+ private part or body of the package or of a descendant
+ 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 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 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. This 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 called by the operator (which might not be predefined and
+ thus might have a different Global specification than the component
+ types).
+
+For the purposes of these checks:
+
+ * if a formal parameter P of a callable entity C is of an anonymous
+ access-to-object type, no check against the Global aspect occurs
+ within C for the dereference of P, but a check against the Global
+ aspect applies at the point of call of C, presuming that P is
+ dereferenced at least once and then read if of an access-to-constant
+ type or updated if of an access-to-variable type; if the actual
+ parameter is of the form X'Access (explicitly or implicitly), then at
+ the point of call the presumed dereference of P is treated as a read
+ or update of X; if the actual parameter A is of any other form, it is
+ treated as a read or update of A.all;
+
+ AARM Ramification: An access parameter ACCESS T is treated somewhat
+ like a parameter specified as IN OUT T while access constant T is
+ treated somewhat like IN T. There is no burden to mention the
+ dereference of an access parameter in the Global aspect, as the
+ effects of the dereference are presumed at the call site, just like
+ the effects on “normal” parameters.
+
+ * if a function returns an object of a type for which the
+ Implicit_Dereference aspect is True (see 4.1.5), or an object of an
+ anonymous access-to-object type, the Global aspect of the function
+ shall reflect the effects of dereferencing the result of the
+ function, if these are over and above reads or updates of parts of
+ aliased formal parameters (or dereferences of access parameters)
+ passed to the function. The effects to be reflected include reading
+ the designated object, and updating the designated object in the case
+ of an access-to-variable result or an Implicit_Dereference result
+ with an access-to-variable access discriminant. A dereference
+ (explicit or implicit) of a function_call on such a function is not
+ further checked at the point of call against any Global or
+ Global'Class aspects that apply to the caller.
+
+ AARM Reason: The function is in a better position than the caller
+ to enumerate the objects affected by dereferencing the result.
+ Because the access discriminant is often of an anonymous type,
+ there is no other place to declare these effects. In most cases,
+ these effects will already be reflected in the aliased or access
+ parameters passed to the function, so nothing need be added to the
+ Global aspect for these.
+
+ AARM Ramification: The last sentence is talking specifically about
+ dereferences associated directly with a function_call. Other
+ dereferences (such as those associated with a rename of a call, or
+ an allocated result of a call) are not included — they have to be
+ covered in the Global or Global'Class aspect in the normal way.
+
+ * if an object of a pool-specific access-to-object type is dereferenced
+ within an operation, and the dereference would violate the
+ restrictions inherent in a Global aspect applicable to the
+ operation, the dereference is nevertheless permitted under the
+ following circumstances:
+ + the pool-specific access type is declared within the private
+ part or body of an enclosing package;
+ + the dereferenced object:
+ * is a part of a formal parameter of the operation whose mode
+ (after any overriding) would allow the operation performed on
+ the dereference;
+ * is a part of a dereference of an object that satisfies these
+ same circumstances; or
+ * is a local object of the operation all of whose
+ assignments are from an object that satisfies these
+ same circumstances.
+
+ AARM Ramification: This exemption of Global checks for dereferences of
+ pool-specific access-to-object values is intended to allow the
+ typical case where a private type uses multiple objects connected
+ internally with access values to represent a single logical
+ object. Here we allow the operation if the access value is reached
+ from a formal parameter whose parameter mode would have allowed
+ the operation. We give an implementation permission below to
+ extend these exemptions to other dereferences based on additional
+ analysis (such as that provided by newer versions of SPARK).
+
+If an implementation-defined global_mode applies to a given
+set of objects, an implementation-defined rule determines what sort of
+references to them are permitted.
+
+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
+
+For a call on a subprogram that has a Global aspect that indicates that
+there are no references to global variables, the implementation may omit
+the call:
+
+ * if the results are not needed after the call; or
+
+ * simply reuse the results produced by an earlier call on the same
+ subprogram, provided that none of the parameters nor any object
+ accessible via access values from the parameters have any part that
+ is of a type whose full type is an immutably limited type, and the
+ addresses and values of all by-reference actual parameters, the
+ values of all by-copy-in actual parameters, and the values of all
+ objects accessible via access values from the parameters, are the
+ same as they were at the earlier call.
+
+[Redundant: This permission applies even if the subprogram produces
+other side effects when called.]
+
+ AARM Discussion: This permission doesn't really allow a compiler to do
+ anything that it couldn't do anyway (as any optimization that gives
+ the required semantics for program executions that aren't erroneous is
+ always allowed), but we considered it important to make Ada
+ programmers aware that such optimizations are possible. Specifically,
+ an implementation can trust the information given in a Global aspect,
+ as any subprogram that violates it is either illegal or would result
+ in erroneous execution. Specifically, the Global contract can be
+ violated by erroneous execution resulting from dereferencing a
+ dangling reference (see 13.11.2), by giving an incorrect contract on
+ an interfaced subprogram (see B.1), by specifying the address of a
+ global object for a local object (see 13.1), or by using
+ Unchecked_Conversion (see 13.9) or Address_to_Access_Conversions (see
+ 13.7.2) to create local accesses to global objects.
+
+ Since optimizations like these don't require a special permission,
+ implementations can also use similar optimizations that go beyond the
+ permission above. For instance, if there are two calls with the same
+ parameters on a subprogram whose Global aspect only indicates reading
+ of a global object G, then the second call can be omitted and reuse
+ the result of the first call if the compiler can prove (with the help
+ of the Global aspect of any subprograms called) that G is not written
+ to between the calls.
+
+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) to prevent the use of Unspecified with the Global aspect in a given
+ partition.
+
+Implementations may provide additional (or fewer) exemptions to Global
+aspect checks on dereferences based on additional analysis of safety.
+
+Implementations may extend the syntax or semantics of the Global aspect
+in an implementation-defined manner.
+
+ 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 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).
+
+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.
+
+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_operator_specifier
+
+ extended_global_aspect_element ::=
+ USE formal_parameter_set
+ | DO dispatching_operation_set
+
+ 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 of a dispatching_operation_specifier shall resolve to
+statically denote 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 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 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 denotes 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.
+
+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, and out annotations
+The intent is that all of the global IN, IN OUT, OUT, USE, and DO annotations
proposed can be statically checked.
-
-** Rest TBD.
+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 a
+restriction in H.4 to allow users to disallow use of the new Unspecified
+value for the Global aspect for any library-level entities. 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 next 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.
+
+The final critical new "default" is that private types are presumed to
+be "Compound" in the sense that any components of a pool-specific access
+type declared in the same private part are presumed to be "Internal" to
+the type, and only give access to other elements of the same conceptual
+Compound object. Visible access types, and general access types (as
+opposed to pool-specific ones) are never considered to be "Internal" and
+any dereference of such an access value is presumed to reference some
+aliased object which might not be part of the current conceptual
+"Compound" object and must be accounted for in the Global aspect of the
+operation. We give an implementation permission to allow other special
+cases of dereferences to be exempted from normal checks, based on
+additional analysis.
+
+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 overal 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 very few, and are
+justified based on a strong belief we need to ensure that even if very
+imprecise, the Global aspect can be presumed to be an *over*
+approximation of the true set of global effects. This led us to add
+ALIASED as an option, to cover all dereferences of general access types
+without going all the way to ALL. We also 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.
+
+We have exempted certain dereferences of pool-specific access values
+from being accounted for in the Global aspect. We do not require any
+special aspect specifications to make use of these exemptions. We only
+require that the access type be declared in a private part or a body, and
+that any dereference be reachable from a formal parameter whose
+parameter mode allows for the operation performed on the dereference.
+This meets the expressed goal that existing code that "does the right
+thing" as far as using access types for implementing abstract data types
+does not need any additional aspect specifications and can still specify
+a Global aspect of NULL on primitive operations of the abstract data
+type.
+
+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
Questions? Ask the ACAA Technical Agent