CVS difference for ai05s/ai05-0186-1.txt

Differences between 1.3 and version 1.4
Log of other versions for file ai05s/ai05-0186-1.txt

--- ai05s/ai05-0186-1.txt	2010/01/21 05:13:50	1.3
+++ ai05s/ai05-0186-1.txt	2010/01/28 04:39:09	1.4
@@ -1,4 +1,4 @@
-!standard 13.3.4 (0)                                10-01-20  AI05-0186-1/02
+!standard 13.3.4 (0)                                10-01-26  AI05-0186-1/03
 !class amendment 09-11-02
 !status work item 09-11-02
 !status received 09-11-02
@@ -42,70 +42,169 @@
 
 !proposal
 
-Add global in and global out annotations to Ada, for subprograms and
-access-to-subprogram types. Add global_init in and global_init out annotations
-for packages and types.
+Add global in and global out annotations to Ada, for subprograms, packages,
+and types. Add related annotations for dispatching subprograms and
+access-to-subprogram types.
+
+The global annotations for types cover default initialization/adjustment/finalization.
+The global annotations for packages cover operations that occur as part of the
+elaboration for packages.
 
-The global_init annotations cover default initialization/adjustment/finalization
-for types; and cover operations that occur as part of the elaboration for packages.
-
 !wording
+
+Add a new section:
+
+13.3.4 Global usage annotation
 
-Semi-formal description (presumably in Section 13.3.4):
+Semi-formal description: [Editor's note: This part depends heavily on the unfinished
+AI05-0183-1; it's not worth trying to describe these rules until that AI is finished.]
 
-Add to the aspect syntax given in AI05-0184-1:
+Add to the aspect syntax given in AI05-0183-1:
 
-    Aspect_Mark [in|out] => Annotation_List
+    Aspect_Mark [in|out|in out] => Annotation_List
 
     Annotation_List ::= ( Annotation_Item {, Annotation_Item} )
 
     Annotation_Item ::= *object_*name | *access_*subtype_mark |
-                         NULL | OTHERS [IN *package*name]
+                         NULL | OTHERS [IN *package*name] |
+                         GENERIC *formal_parameter_*name
 
 The names in these items resolve with the same visibility as other aspect
 expressions (that usually is the end of the visible part). The names must
 resolve without context.
+
+[Editor's note: We need the keyword GENERIC here, so that we can tell the
+difference between references to the initialization and the referenced data
+for formal access types in annotations. Both use the access type name.
+An alternative would be to add a keyword to the *access_*subtype_mark
+case instead, but nothing that isn't ambiguous seems appropriate. My best
+idea was *access_*subtype_mark.ALL .]
+
+Aspect_Mark in out => Annotation_List is semantically equivalent to
+Aspect_Mark in => Annotation_List, Aspect_Mark out => Annotation_List.
+
+AARM Discussion: All of the rules are defined in terms of "Aspect_Mark in"
+and "Aspect_Mark out". The rules are applied twice to "Aspect_Mark in out".
+
+Aspects Global, Global'Class, and Global'Access are defined.
 
-Aspects Global and Global_Init are defined.
+[End semi-fomal description. From here to the end is intended to be actual wording.]
 
 Static Semantics
 
 A read or write of an object O is *covered by an annotation* in an
 Annotation_List if:
     * O statically denotes a part of an object named in the Annotation_List;
-    * The annotation OTHERS without a package name occurs in the list;
-    * The annotation OTHERS with a package name P occurs in the list, and
+    * The annotation item OTHERS without a package name occurs in the list;
+    * The annotation item OTHERS with a package name P occurs in the list, and
       O denotes part of an object declared in P, or O denotes a part of an object
-      produced by a dereference of an object of an access type declared in P; or
+      produced by a dereference of an object of an pool-specific access type whose
+      pool is declared in P; or
     * O denotes a part of an object produced by a dereference of an object of
       an access type named in the Annotation_List.
 
 AARM Ramification: "others" by itself allows anything to be read or written.
 
+"Statically denotes" does not include dereferences, so the first rule only
+applies to statically declared objects.
+
 An annotation A1 is *compatible* with another annotation A2 if:
     * A1 contains NULL; or
-    * A2 contains the annotation OTHERS without a package name; or
+    * A2 contains the annotation item OTHERS without a package name; or
     * All of the following must be true:
-      -- Each *object_*name in A1 is covered by an annotation in A2;
-      -- Each *access_subtype_*name in A1 is found in A2; and
-      -- For each OTHERS annotation with a package name P, there is
-         a OTHERS annotation in A2 that statically denotes P.
+      -- Each *object_*name in A1 is covered by an annotation item in A2 or is
+         an object that would not need to be included in A1 if it was explicitly
+         referenced within the entity defining A1;
+
+         AARM Reason: The latter part means that local objects in a subprogram S
+         do not need to be included its annotation when they are included in
+         the annotation for a nested subprogram of S that S calls.
+
+      -- Each *formal_parameter_*name item in A1 is found in A2;
+      -- Each *access_*subtype_mark item in A1 is found in A2 or, if the
+         the subtype_mark denotes a pool-specific access type, 
+         an OTHERS annotation item in A2 naming the package P in which the
+         pool of the access type is declared; and
+      -- For each OTHERS annotation item with a package name P, there is
+         an OTHERS annotation item in A2 that statically denotes P.
+
+AARM Ramification: This definition is not symmetrical; A2 may allow more than
+A1 requires (such as having an annotation of (others)).
+
+A type T is *compatible* with an annotation A of an aspect if:
+    * T is a generic formal type, and A contains the *formal_parameter_*name
+      of the formal type; or
+    * The annotation for the same aspect of T is compatible with A.
+
+
+The result of a *union* of annotation A1 with annotation A2 is:
+    * if A1 contains NULL, A2;
+    * if A2 contains NULL, A1;
+    * if either A1 or A2 contains an OTHERS annotation
+      without a package name, an annotation with a single item of OTHERS without a package name;
+    * Otherwise, an annotation with all of the Annotation_Items of A1 and A2 with any duplicates
+      removed.
+
+AARM Ramification: This definition is symmetrical; the order of the operands does
+not matter.
+
+
+Unless otherwise specified (either explicitly or defined by this International Standard),
+the annotation for each defined aspect is (others).
+
+AARM Ramification: (others) allows all global references, so it is completely
+compatible with earlier versions of Ada.
+
+An inherited subprogram (see 3.4) inherits the annotations of the primitive subprogram
+of the parent or progenitor type. Redundant[The annotations can be changed on an
+overriding subprogram, with some restrictions.]
+
+
+When determining the Global in annotations of entities declared in an instantiation of a
+generic G, each *formal_parameter_*name item F of every Global in annotation A of any
+entities declared in the instance that references a formal parameter of G is removed from
+A and:
+   * if F is a formal type, the result is the union of A and the Global in annotation
+     of the actual type;
+
+   * if F is a formal subprogram, the result is the union of A and the Global in annotation
+     of the actual subprogram;
+
+   * if F is a formal IN OUT parameter, the *object_*name of the actual parameter is added
+     to A if that *object_*name would need to be included in a Global in annotation
+     for the enclosing entity when it is read at the point of the instance, Redundant[and
+     nothing is added otherwise].
+
+Analogous rules apply to a Global out annotation (replacing "in" by "out" and
+"read" by "written" everywhere).
 
-AARM Ramification: This is not symeterical.
+AARM Discussion: At the point of an instance, all of the references to the formal parameters
+are replaced by the annotations of the actual. This does not require re-analyzing the
+generic.
 
+
 Legality Rules
+
+An annotation_list can be given if and only if the aspect is Global, Global'Class,
+or Global'Access.
+
+The aspect Global shall be given only on subprograms, types, packages, and
+generic packages.
 
-An annotation_list can be given if and only if the aspect is Global or Global_Init.
+The aspect Global'Access shall be given only on access-to-subprogram types.
 
-The aspect Global shall be given only on subprograms and on access-to-subprogram types.
-The aspect Global_Init shall be given only on types, packages, and generic packages.
+The aspect Global'Class shall be given only on primitive subprograms of a tagged
+type.
 
-The Annotation_Item NULL has to be the only item in an Annotation_List if
-it is given.
+The Annotation_Item NULL shall appear alone in an Annotation_List.
 
 An *object*_name given in an Annotation_List shall statically denote some
 object.
 
+A *formal_parameter_*name given in an Annotation_List shall statically denote
+some generic formal parameter of an enclosing generic unit; the formal parameter
+shall be a formal type, a formal subprogram, or a formal IN OUT object.
+
 If a subprogram contains a Global in annotation, then:
   * Every object that is read by the subprogram body shall either be accessible
     from the function call, be a constant object of an elementary type, or be
@@ -113,15 +212,23 @@
   * The subprogram corresponding to each dispatching call in the subprogram body
     which has a dynamically tagged controlling operand shall have a compatible
     Global'Class in annotation; the access-to-subprogram type for each call of
-    a dereference of an access value shall have a compatible Global in annotation;
-    the subprogram corresponding to every other call in the subprogram body shall
-    have a compatible Global in annotation.
-  * The type of every stand-alone object declared by the subprogram shall have
-    a compatible Global_Init in annotation.
+    a dereference of an access value shall have a compatible Global'Access in
+    annotation; the *formal_parameter_*name for each call of a formal subprogram
+    is present in the annotation; and the subprogram corresponding to every other
+    call in the subprogram body shall have a compatible Global in annotation.
+  * The type of every stand-alone object declared by the subprogram shall be
+    compatible with the annotation.
   * Every nested package and package instantiation declared by the subprogram
-    shall have a compatible Global_Init in annotation.
-  * The type of each assignment_statement shall have a compatible Global_Init in
-    annotation.
+    shall have a compatible Global in annotation.
+  * The type of each assignment_statement in the subprogram body shall be compatible
+    with the annotation. In addition, if the target of the
+    assignment_statement is a dereference of some access type A, the Allocate
+    and Deallocation routines associated with the storage pool of type A in
+    the subprogram body shall have a compatible Global in annotation.
+
+    AARM Reason: Allocate and Deallocate can be called here if the implementation
+    chooses; we have to assume the worst.
+
   * The Allocate routine associated with the storage pool for the type of
     each allocator in the subprogram body shall have a compatible Global in
     annotation.
@@ -136,24 +243,30 @@
 AARM Ramification: Local objects, elementary constant objects (declared anywhere)
 and the parameters of the call do not need to appear in a Global in annotation.
 Note that this is referring to constant objects, not just constant views of an
-object. End Ramification.
+object.
+
+A write of a dereference of an object P *reads* the object P (and writes the 
+designated object).
+End AARM Ramification.
 
 AARM Discussion: We don't need a rule for Deallocate calls in Unchecked_Deallocation,
 as it is a call and does not have annotations defined. Thus the above rule will
 always fail and thus we don't care about the annotations on Deallocate.
 
-Analogous rules apply to a Global_init out annotation (replacing "in" by "out" and
+Analogous rules apply to a Global out annotation (replacing "in" by "out" and
 "read" by "written" everywhere).
 
 [Editor's note: I don't want to duplicate the rules, they're complex enough as it is.]
 
-For an attribute P'Access of access-to-subprogram type S that has a Global in
+For an attribute P'Access of access-to-subprogram type S that has a Global'Access in
 annotation, subprogram P shall have a compatible Global in annotation. Similarly,
-for a type S that has a Global out annotation, subprogram P shall have a compatible
-Global out annotation.
+for a type S that has a Global'Access out annotation, subprogram P shall have a
+compatible Global out annotation.
+
+[Editor's note: One could argue that this belongs in 3.10.2; I put it here to keep
+all of the relevant rules together.]
 
-Global'Class annotations shall be given only on primitive subprograms of
-a tagged type Redundant[; they provide annotations for dispatching calls].
+Redundant[Global'Class annotations provide annotations for dispatching calls.]
 The Global in annotation of a subprogram shall be compatible with the Global'Class in
 annotation of the subprogram; similarly Global out annotation of a subprogram
 shall be compatible with the Global'Class in annotation of the subprogram.
@@ -171,9 +284,9 @@
     compatible with the Global'Class out annotation for PP.
 
 
-If a type includes a Global_init in annotation:
-  * If the full type is composite, the type of each component shall have a compatible
-    Global_init in annotation.
+If a type includes a Global in annotation:
+  * If the full type is composite, the type of each component shall be compatible
+    with the annotation.
   * If the full type is controlled, the associated Initialize and Finalize routines
     shall have compatible Global in annotations.
   * If the full type is controlled and not limited, the associated Adjust routine
@@ -181,20 +294,21 @@
   * If the full type is composite, for each default expression E for a component of
     the type:
      * every object that is read by E shall be a constant object of an elementary
-       type, or be covered by the Global_init in annotation; and
+       type, or be covered by the Global in annotation; and
      * the subprogram corresponding to each dispatching call in E
        which has a dynamically tagged controlling operand shall have a compatible
        Global'Class in annotation; the access-to-subprogram type for each call in E
-       of a dereference of an access value shall have a compatible Global in
-       annotation; the subprogram corresponding to every other call in E shall
-       have a compatible Global in annotation; and
+       of a dereference of an access value shall have a compatible Global'Access in
+       annotation; the *formal_parameter_*name for each call of a formal subprogram
+       in E is present in the annotation; the subprogram corresponding to every other
+       call in E shall have a compatible Global in annotation; and
      * the Allocate routine associated with the storage pool for the type of
        each allocator in E shall have a compatible Global in annotation.
      * For each attribute A'Storage_Size in E where A is an access type, the
        Storage_Size routine associated with the storage pool of A shall have a
        compatible Global in annotation.
-   * If the full type is a task type, the body shall conform to the rules for a subprogram
-     body (given previously).
+   * If the full type is a task type, the rules for a subprogram body (given previously)
+     shall be applied to the task body and the Global in annotation.
 
 [We do not need to worry about assignment, stand-alone objects, and instances here,
 none of those are possible inside of types, other than task bodies, which we handle
@@ -206,74 +320,158 @@
 above rules). In practice, Adjust and Finalize are usually very similar in design,
 and are likely to depend on the same set of globals, so this isn't much of a limitation.
 
-Analogous rules apply to a Global_init out annotation (replacing "in" by "out" and
+Analogous rules apply to a Global out annotation (replacing "in" by "out" and
 "read" by "written" everywhere).
 
 
-If a package or generic package includes a Global_init in annotation:
+If a package or generic package includes a Global in annotation:
   * For each expression or call E in every declarative_item (but not including
     those in nested units) and the sequence of statements of the package body:
      * every object that is read by E shall be declared in the package, a constant
-       object of an elementary type, or be covered by the Global_init in annotation;
+       object of an elementary type, or be covered by the Global in annotation;
        and
      * the subprogram corresponding to each dispatching call in E
        which has a dynamically tagged controlling operand shall have a compatible
        Global'Class in annotation; the access-to-subprogram type for each call in E
-       of a dereference of an access value shall have a compatible Global in
-       annotation; the subprogram corresponding to every other call in E shall
-       have a compatible Global in annotation; and
+       of a dereference of an access value shall have a compatible Global'Access in
+       annotation; the *formal_parameter_*name for each call of a formal subprogram
+       is present in the annotation; the subprogram corresponding to every other
+       call in E shall have a compatible Global in annotation; and
      * the Allocate routine associated with the storage pool for the type of
        each allocator in E shall have a compatible Global in annotation.
      * For each attribute A'Storage_Size in E where A is an access type, the
        Storage_Size routine associated with the storage pool of A shall have a
        compatible Global in annotation.
-  * The type of every stand-alone object declared by the package shall have
-    a compatible Global_Init in annotation.
+  * The type of every stand-alone object declared by the package shall be compatible
+    with the annotation.
   * Every nested package and package instantiation declared by the package
-    shall have a compatible Global_Init in annotation.
+    shall have a compatible Global in annotation.
   * The type of each assignment_statement in the sequence_of_statements of the
-    package body shall have a compatible Global_Init in annotation.
+    package body shall be compatible with the annotation. In addition,
+    if the target of the assignment_statement is a dereference of some access
+    type A, the Allocate and Deallocation routines associated with the storage
+    pool of type A in the subprogram body shall have a compatible Global in
+    annotation.
 
-Analogous rules apply to a Global_init out annotation (replacing "in" by "out" and
+Analogous rules apply to a Global out annotation (replacing "in" by "out" and
 "read" by "written" everywhere).
 
+** Wording TBD:
+
+I hate the duplication of rules here. I tried and tried to find some way to
+eliminate the duplication for expressions and calls (for which most of the
+rules apply). But I continually got stuck by the fact that there are essentially
+3 parameters: the expression E; the accessibility/locality of objects to exclude
+(that is, the definition of what is local is different for subprograms [we need
+to include the parameters], packages [we need to exclude anything outside of the
+package, even though at the same accessibility level, as packages are invisible
+to accessibility], and types [locals only for tasks, and nothing special needed
+otherwise]; and the kind of annotation (either "in" or "out"). It's just too
+much to do in any understandable way. And I couldn't find a way to factor out
+the accessibility without getting overlapping rules. Maybe someone else has a
+better idea.
+
+** End Wording TBD.
 
+
+
 [Generic rules; these apply to the entire Legality Rules section]
 
 In addition to the places where Legality Rules normally apply, these rules also
 apply in the private part of an instance of a generic unit.
 
-For the purposes of enforcing these rules in a generic body, the Global_Init
-annotations for a formal type are assumed to be (others); the Global annotations
-for formal subprograms and formal access types are assumed to be (others); the
+For the purposes of enforcing these rules in a generic body, the
 Global annotations on the storage pool operations for formal access types are
-assumed to be (others).
+assumed to be (others), the Global annotations on generic formal elementary
+types are assumed to be (null).
 
 [This last paragraph is not talking about inside of instances; rechecking is
 done there with the actual annotations. This is the assume-the-worst rule needed
-in generic bodies.]
+in generic bodies. We can assume the latter because no elementary type can
+have a "significant" default initialization; and the actual has to be known
+to be elementary. Note that an elementary type could have some other annotations
+that are explicitly specified; those might be ignored inside of the generic.]
+
+
+Implementation Permissions
+
+An implementation is permitted to omit a call on a subprogram whose Global out
+annotation is (null) and the results are not needed after the call. In addition,
+the implementation may omit the call on such a subprogram and simply reuse the
+results produced by an earlier call on the same subprogram provided:
+* No globals that are indicated as read by the Global in annotation for the
+  subprogram are modified between the eariler call and the omitted call;
+* None of the parameters are of a limited type;
+* The addresses and values of all by-reference actual parameters, the values
+  of all by-copy-in actual parameters, and the values of all object accessible
+  via the values of any access parameters, are the same as they were at the
+  earlier call.
+Redunant[This permission applies even if the subprogram produces other
+side-effects when called.]
+
+AARM Discussion: This is intended to be the same rules as applies to calls on
+subprograms defined in declared Pure packages (see 10.2.1). Note that we don't
+need to talk about access values embedded in the parameter objects (as we have to
+for Pure), or about objects access from parameters of named access types, as those
+have to be covered by the global annotations.
+
+AARM Ramification: The part about indicating that no globals read are modified
+via Global in annotations is trivially true for Global in => (null). This makes
+this rule easier to use than the corresponding Pure rule.
+
+The part about side-effects is barely necessary. The only possible side effects
+from a call with Global out => (null) would be through machine code insertions
+modifying objects, imported subprograms with untruthful annotations,
+Address_to_Access_Conversions, and similar features. The compiler may omit a call
+to such a subprogram even if such side effects exist; it is allowed to presume the
+annotations are accurate, even though this cannot be 100% certain. 
 
 ---
 
-[Define the default annotations. Effectively, all annotations default to  "others"
-because all of the rules above treat absense of an annotation like "others", unless
-we say otherwise. - Editor.]
+[Now define the default annotations. Above we said that all entities default to having
+an annotation of (others); here we're going to say otherwise for particular cases
+where we can do better without introducing compatibility problems.]
 
 Add to 3.5:
+
+Unless otherwise specified, elementary types that do not have a partial view have
+annotations (see 13.3.4) of Global in out => (null).
 
-Elementary types of the language have implied annotations of Global_Init in => (null),
-Global_Init out => (null).
+AARM Ramification: If the elementary type does have a partial view, the type has
+annotations of Global in => (others), Global out => (others)); this is the default
+for all entities and is necessary to avoid breaking privacy. Annotations are part
+of the contract of the type, and should be carefully thought out to avoid problems
+with future maintenance.
+
+Add to 3.6:
+
+Unless otherwise specified, array types that do not have a partial view have
+Global in and out annotations (see 13.3.4) that are copies of those of the
+component type.
+
+AARM Ramification: If the array type does have a partial view, the type has
+annotations of Global in => (others), Global out => (others)); this is the default
+for all entities and is necessary to avoid breaking privacy. Annotations are part
+of the contract of the type, and should be carefully thought out to avoid problems
+with future maintenance.
+
+AARM Discussion: Note that there is no such rule for record or other composite types.
+The annotations needed for them are complex in general, and leaving them out of the
+source code is not going to help the human reader. [Editor's note: It is also fairly
+rare that they would be generated; most record types in well-designed programs do have
+partial views, so it is not a big hardship to write them by hand in the rare case
+where that is not the case.]
 
 Add to 4.5:
 
 Unless otherwise specified, the predefined operators of the language that have
-at operands of an elementary type all have implied annotations of Global in => (null),
-Global out => (null).
+all operands of an elementary type all have implied annotations (see 13.3.4)
+of Global in out => (null).
 
 Add after 4.5.2:
 
 The predefined equality and ordering operators for discrete array types have implied
-annotations of Global in => (null), Global out => (null).
+annotations (see 13.3.4) of Global in out => (null).
 
 AARM Ramification: The global rule means that equality and ordering operators for
 elementary types also have such annotations. Composition of equality for
@@ -284,7 +482,7 @@
 Add after 4.5.3:
 
 If C is an elementary type, the predefined concatenation operators have implied
-annotations of Global in => (null), Global out => (null).
+annotations (see 13.3.4) of Global in out => (null).
 
 [We could go further, but it gets messy, as any controlled component may drag
 Adjustment into the equation.]
@@ -294,18 +492,19 @@
 Static Semantics
 
 Each subprogram that is declared pure or is declared in a language-defined
-package or generic package that is declared pure has implied annotations of
-Global in => (null), Global out => (null) unless the subprogram has one or
-more parameters of an access type.
+package or generic package that is declared pure has implied annotations (see
+13.3.4) of Global in out => (null) unless the subprogram has one or more
+parameters of an access type or the annotations are specified elsewhere
+in this International Standard.
 
-AARM Compatibility Note: This could be imcompatible if a composite object
+AARM Compatibility Note: This could be incompatible if a composite object
 passed as a parameter to such a subprogram has an access component. This does
-not seem likely for the language defined packages.
+not seem likely for the language defined Pure packages.
 
 [Editor's note: I'm not sure the exception is actually needed, but I didn't
 check.
 
-Here the list of such packages approved as of this writing;
+Here the list of declared Pure packages as of this writing;
 I don't intend to put the list into the AARM as it would require constant
 maintenance. I'm ignoring Wide_ and Wide_Wide_ versions of packages for this
 list, as well as bounded and unbounded string versions.
@@ -347,78 +546,177 @@
     System.Storage_Elements
 
 
-I'm assuming that we adopt AI-142-4 and/or AI-139-2, both of
-which require the bounded containers to be preelaborable (so that the
-accessors and iterators work). We would like to explicitly provide annotations
-for the bounded containers as appropriate (I suspect unbounded is nasty because
-of the access types involved).
-
-I suspect that we need to exclude the generic sorts, as the annotations of
-element types or the formal subprograms come into play for these, and we don't
-want to restrict them. Not sure of the best way to do that.
+Containers are discussed below; I'm assuming that they will end up with explicit
+annotations.
 
+I suspect that we need to give explicit annotations for the generic sorts, as the
+annotations of element types or the formal subprograms come into play for these,
+and we don't want to restrict them.
+
 We probably also want to exclude the generic real and complex array packages;
 adding these annotations would prevent sparse matrix representations. I don't
-think we want to go that far (although they'd be hard to implement within the
-restrictions of Pure).
+think we want to go that far (although sparse matrixes would be hard to implement
+within the restrictions of Pure, so maybe it doesn't matter).
 
 End really long Editor's note. Probably should move some of this to !discussion
 after we make decisions.]
-
-** Wording TBD:
 
-I don't quite see how to take into account (or if we have to) the storage pool
-of an access type.
-
-The intended rules are:
-
-For pool-specific types, only the storage pool can be accessed by a dereference.
-For general access types, any aliased object of the designated type (and the
-storage pool) can be accessed by a dereference.
-
-The current wording "covers" dereferences by naming their access type. The above
-rules would seem necessary for tools depending on these annotations, but doesn't
-seem necessary for the rules defining the annotations themselves. I handled
-calls to Allocate and Storage_Size explicitly. This latter set of rules doesn't
-handle implicitly called Allocate/Deallocate calls in assignement statements,
-but that could be handled explicitly as well if the approach is OK.
-
-If there is a problem with this strategy, it is that there isn't any way to
-localize access types to a particular pool (when that is known but the type
-isn't visible). You would have to use a package name for a local access type
-(usually youself). For instance, all of the operations of Ada.Containers.Vectors
-would need Global in => (others in Vectors) because of the (presumably) local
-access type declared to implement the unbounded-ness.
-
-I don't think there is enough benefit to further complications here (especially
-as the containers example, the pool isn't visible either, so I can't imagine any
-other annotation that would work), but I am willing to be convinced otherwise.
-
-An alternative approach would be to wrap up the entire set of items in
-Global in/out annotations for each access type (that would be disjoint with
-access-to-subprograms use for the same thing). That would include all of the
-Global annotations for the subprograms of the storage pool, an annotation for
-the storage pool object, and ??? for general access object ["others" is the only
-current thing, which would be nasty]. That would be easier for tools to use, I
-suspect, but harder to write and less specific. Which doesn't seem to be an
-improvement to me.
+Replace to G.1.1(3) with:
 
----
+   type Complex is
+       record
+           Re, Im : Real'Base;
+       end record with
+          Global in => (null), Global out => (null);
+
+[Editor's note: This is the only visible record type in the standard that I know
+of. We may want some annotation for many of the private types as well; that
+needs to be done on a case-by-case basis.]
+
+[Editor's note: Annotations on the containers were assigned to Bob Duff.
+I'm providing suggested annotations for part of Bounded_Vectors in order
+to test that the generic mechanisms work.
+
+Notes: We have to use the OTHERS IN Vectors on all of the cursor forms
+because of the dereference of an access-to-vector type defined in this
+package (cursors include a reference to their associated container).
+
+The annotations on the unbounded form of Vectors would be the same except
+that OTHERS IN Vectors would be added to any that could allocate/deallocate
+elements in order to reflect the allocated memory (from a presumably private
+but library-level access type).]
+
+
+A.18.17 Bounded Vectors
+
+generic
+   type Index_Type is range <>;
+   type Element_Type is private;
+   with function "=" (Left, Right : Element_Type)
+      return Boolean is <>;
+package Ada.Containers.Bounded_Vectors is
+   pragma Preelaborate(Bounded_Vectors);
+   pragma Remote_Types(Bounded_Vectors);
+
+   subtype Extended_Index is
+      Index_Type'Base range
+         Index_Type'First-1 ..
+         Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
+   No_Index : constant Extended_Index := Extended_Index'First;
+
+   type Vector (Capacity : Count_Type) is tagged private with
+      Global in out => (generic Element_Type);
+   pragma Preelaborable_Initialization(Vector);
+      -- We're assuming an implementation something like:
+      -- type Vector (Capacity : Count_Type) is tagged record
+      --    Length : Count_Type;
+      --    Data : array (1 .. Capacity) of Element_Type;
+      -- end record;
+
+   type Cursor is private with
+      Global in out => (generic Index_Type);
+   pragma Preelaborable_Initialization(Cursor);
+      -- We're assuming an implementation like:
+      -- type Cursor is
+      --    Vect  : access Vector;
+      --    Index : Extended_Index;
+      -- end record;
+
+   Empty_Vector : constant Vector;
+   No_Element : constant Cursor;
+   function "=" (Left, Right : Vector) return Boolean with
+      Global in out => (generic Element_Type, generic Ada.Containers.Bounded_Vectors."=");
+
+   function To_Vector (Length : Count_Type) return Vector with
+      Global in out => (generic Element_Type);
+      -- Every operation that needs to create a Vector object needs to
+      -- include the annotations of the Vector object.
+
+   function To_Vector
+     (New_Item : Element_Type;
+      Length   : Count_Type) return Vector with
+      Global in out => (generic Element_Type);
+
+   function "&" (Left, Right : Vector) return Vector with
+      Global in out => (generic Element_Type);
+
+   function "&" (Left  : Vector;
+                 Right : Element_Type) return Vector with
+      Global in out => (generic Element_Type);
+
+   function "&" (Left  : Element_Type;
+                 Right : Vector) return Vector with
+      Global in out => (generic Element_Type);
+
+   function "&" (Left, Right  : Element_Type) return Vector with
+      Global in out => (generic Element_Type);
+
+   function Capacity (Container : Vector) return Count_Type with
+      Global in out => (null);
+
+   procedure Reserve_Capacity (Container : in out Vector;
+                               Capacity  : in     Count_Type) with
+      Global in out => (null);
+      -- This would be very different for other forms, where this does
+      -- something.
+
+   function Length (Container : Vector) return Count_Type with
+      Global in out => (null);
+      
+   procedure Set_Length (Container : in out Vector;
+                         Length    : in     Count_Type) with
+      Global in out => (generic Element_Type);
+      -- We need to allow writing empty elements, if the implementation
+      -- does something explicit for them. We have to allow Adjust, so
+      -- we also need to include the reading portion.
+
+   function Is_Empty (Container : Vector) return Boolean with
+      Global in out => (null);
+
+   procedure Clear (Container : in out Vector) with
+      Global in out => (null);
+      -- This just changes the length.
+
+   function To_Cursor (Container : Vector;
+                       Index     : Extended_Index) return Cursor with
+      Global in out => (null);
+      -- No dereferences here.
+
+   function To_Index (Position  : Cursor) return Extended_Index;
+      Global in out => (null);
+      -- No dereferences here.
+
+   function Element (Container : Vector;
+                     Index     : Index_Type)
+      return Element_Type with
+      Global in out => (generic Element_Type);
+      -- Creates an element.
+
+   function Element (Position : Cursor) return Element_Type with
+      Global in => (others), Global out => (generic Element_Type);
+      -- The dereference of the container can touch anything.
+      -- Even if we had a more specific annotation (perhaps we need
+      -- to add one), this would still prevent many optimizations.
+      -- I knew I hated this implicit container semantics, I just
+      -- couldn't explain why. Note that the previous routine has
+      -- much stronger annotations. Apparently, tools will need to
+      -- be container-aware to have any chance. Yuck.
+
+
+   procedure Replace_Element (Container : in out Vector;
+                              Index     : in     Index_Type;
+                              New_Item  : in     Element_Type) with
+      Global in out => (generic Element_Type);
+      -- Assigns an element; the type's Global annotations are also
+      -- used for assignment.
+
+   procedure Replace_Element (Container : in out Vector;
+                              Position  : in     Cursor;
+                              New_item  : in     Element_Type) with
+      Global in => (others), Global out => (generic Element_Type);
 
-I hate the duplication of rules here. I tried and tried to find some way to
-eliminate the duplication for expressions and calls (for which most of the
-rules applied. But I continually got stuck by the fact that there are essentially
-4 parameters: the expression E; the accessibility/locality of objects to exclude
-(that is, the definition of what is local is different for subprograms [we need
-to include the parameters], packages [we need to exclude anything outside of the
-package, even though at the same accessibility level, as packages are invisible
-to accessibility], and types [locals only for tasks,and nothing special needed];
-the kind of annotation (either "in" or "out"); and which annotation it is (Global
-or Global_Init). It's just too much to do in any understandable way. And I couldn't
-find a way to factor out the accessibility without getting overlapping rules. Maybe
-someone else has a better idea.
+...
 
-** End Wording TBD.
 
 !discussion
 
@@ -452,16 +750,6 @@
 
 ---
 
-These annotations can be used by the compiler to guide code generation as well
-as for static analysis. In that case, rules similar to those for Pure
-subprograms should be applied -- it is OK to assume that the annotations are
-correct, but if the subprogram is called, then the compiler must use the actual
-side-effects, not any assumed because of annotations.
-
-[I didn't try to word this. - Randy]
-
----
-
 It might make the most sense to define these in Annex H (High-Integrity Systems),
 rather than in Section 13. The most important thing is to define the syntax
 so that implementations can implement it and the checking (even if they are not
@@ -470,13 +758,28 @@
 ensure that the information is accurate.
 
 ---
+
+Annotations are defined in terms of "reading" and "writing" of objects. We
+use these terms in the same way as the rest of the standard; in particular,
+in the definitions of the semantics for Atomic objects and pragma Reviewable.
+
+---
 
-We have two kinds of global annotations, one for callable entities (Global)
-and one for the initialization/elaboration of entities. We need both as
-there is a (small) overlap for access-to-subprogram types, which is both a
-type and an callable entity.
+We have three kinds of global annotations, one for almost everything (Global),
+and two for special cases: Global'Access for calls through access-to-subprogram
+types, and Global'Class for dispatching calls.
+
+Note that we need Global'Access to be a separate annotation as an
+access-to-subprogram type has both annotations (and we need to be able to
+talk about it for generics, as well as needed to support the unlikely
+possibility of it having a partial view).
+
+Annotations are defined as aspects, and thus we are using the rules for aspects
+to simplify this description: there is only one per type (they are not
+view-specific) [although they can be given on private types, they then cannot
+be given on the full type]; 
 
-Global_Init annotations can be given on private types; if so, they are
+Global annotations can be given on private types; if so, they are
 enforced on the full type as well.
 
 ---
@@ -485,21 +788,306 @@
 concept (elaboration). We tried to avoid that mistake with this set of rules.
 
 That requires making composition of annotations explicit. The definition of
-the Global_Init annotations for types requires this. Once we have this,
-applying the rules just requires talking about the type of stand-alone
-objects and of assignment_statements; they include the annotations of any
-components by definition.
+the Global annotations for types requires this; the annotations of all of
+the components and all of the default expressions have to be compatible with
+the type's annotation. Once we have this, applying the rules just requires
+talking about the type of stand-alone objects and of assignment_statements;
+they include the annotations of any components by definition.
 
 ---
 
 The rules are complicated by the need to include all implicit calls. That
-is done by folding Initialize/Finalize/Adjust into Global_Init (along
+is done by folding Initialize/Finalize/Adjust into Global (along
 with default initialization), and explicitly talking about the operations
 of storage pools.
 
+---
+
+These annotations can be used by the compiler to guide code generation as well
+as for static analysis. The Implementation Permission provides rules similar
+to those for Pure subprograms -- it is OK to assume that the annotations are
+correct, but if the subprogram is called, then the compiler must use the actual
+side-effects, not any assumed because of annotations.
+
+---
+
+Annotations can explicitly include names of generic formal parameters; the
+annotations appropriate for the actual parameters are substituted when the
+generic is instantiated.
+
+We originally tried to use an assume-the-worst rule for generic units, but
+that essentially requires any subprogram declaring in a generic that uses a
+formal parameter to be annotated with Global in => (others). That would
+totally prevent useful annotations on generic units, which is a
+complete nonstarter for obvious reasons.
+
+Another option considered was to include the annotations as part of the
+generic contract. That would require some new matching rules, but otherwise
+is fairly simple. But it should be obvious that that does not work well for
+general-purpose generic units. For instance, consider the bounded Vector
+container. In order to be able to have the desired (null), (null) annotations
+on most routines, we would have to annotate the Element_Type with (null),
+(null) annotations. But that would prevent instantiating the container with
+many real types (any that include parts with Initialize/Adjusts that allocate
+memory, for instance). Not only is that incompatible, it also reduces the
+utility of the containers.
+
+Luckily, annotations can be combined with the normal set operations. Thus, if
+we create a way to refer to the annotations of formal parameters without
+actually knowing what they are, we can then use the real annotations of the
+actual types when the generic is instantiated. This neatly solves the problem
+by making the annotations change as needed. For instance, when the bounded
+container is instantiated with Integer, all of the annotations will become
+(null), (null); but if the actual type has default annotations of (others),
+(others) all of the annotations will reflect that as well.
+
+[I'm so smart to have figured this out myself. ;-) Just wish I had done so
+the first time. Editor.]
+
+Note that we only provide generic annotations for formal entities that
+have interesting annotations. We don't provide annotations for *in* formal
+parameters, as they are copies of the actual made at the point of the
+instance. As such, they have no effect on the annotations of items declared
+in the generic (of course, the evaluation of the actuals could require them
+to be included in an annotation for a subprogram or package surrounding the
+instance).
+
+Similarly, we don't provide annotations for formal packages, as the actuals
+for those are already elaborated instances. As such, their annotations will
+never be needed in the generic unit (they're only used at the point of the
+instance).
+
+---
+
+The objects accessed by an access type are:
+
+For pool-specific types, only the storage pool can be accessed by a dereference.
+For general access types, any aliased or tagged object of the designated type
+(and the storage pool) can be accessed by a dereference. (Recall that any
+tagged parameter, and thus any tagged object can have 'Access taken.)
+
+We allow specifying the name of the access type as an Annotation_Item. This
+provides a convinient way to cover all possible target objects without discussing
+the pool or aliased objects. Tools would have to use rules similar to the above,
+but the the programmer does not need to worry about exactly what is being
+written.
+
+However, if name of the access type is hidden (or no name is available), then
+we have to fall back on OTHERS. But OTHERS is a blunt instrument. For a
+pool-specific type, we can allow just naming the package containing the pool.
+But for a general access type, we can only allow (OTHERS) -- which provides no
+information at all.
+
+An option that was considered was adding a general access Annotation_Item.
+
+     ACCESS subtype_mark
+
+This gives the designated type, and thus would limit references to aliased
+or tagged objects of the appropriate type.
+
+However, we would still need to cover the pool with an appropriate OTHERS.
+And that can't be done cleanly for default pools (especially for anonymous
+access types).
+
+At this point the author gave up and left the problem for all to see.
+
+
+An alternative approach would be to wrap up the entire set of items in
+Global in/out annotations for each access type (that would be disjoint with
+access-to-subprograms use for the same thing). That would include all of the
+Global annotations for the subprograms of the storage pool, an annotation for
+the storage pool object, and ACCESS designated_subtype_mark for general access
+objects. That probably would be easier for tools to use, but harder to write
+and less specific. And it doesn't help the anonymous default pool problem.
+So it doesn't seem to be an improvement, thus we did not use that alternative.
+
 !example
+
+Following is a non-generic example that illustrates how these annotations work on
+a controlled type. There are some embedded comments that explain some details of
+the annotations.
+
+with Ada.Finalization;
+package TestV02A is
+
+   type JSON_Data_Type is
+     (JSON_NULL,
+      JSON_BOOLEAN,
+      JSON_NUMBER,
+      JSON_STRING);
+      -- As this is an elementary type, we don't need any annotations;
+      -- they will default to Global in => null, Global out => null.
+
+   type Holder is tagged private with
+       Global in => (TC_Count),
+       Global out => (TC_Count, TC_Passed);
+      -- Globals used by the default initialization/adjustment/finalization of
+      -- the type.
+
+   Null_Holder : constant Holder;
+
+   Boolean_Holder : constant Holder;
+
+   String_Holder : constant Holder;
+
+   function Check_Holder (Container : in Holder; Kind : in JSON_Data_Type)
+       return Boolean with
+       Global in out => (null);
+
+   TC_Passed : Boolean := True;
+
+   TC_Final_Count : Natural := 0;
+
+private
+
+   type Holder is new Ada.Finalization.Controlled with record
+      Type_Kind : JSON_Data_Type := JSON_Null;
+   end record;
+   -- Since Global is an aspect and it was specified for the private type,
+   -- we don't repeat it here. Aspects are the same for all views.
+   subtype My_Holder is Holder;
+
+   procedure Initialize (Container : in out Holder) with
+       Global in  => (null),
+       Global out => (TC_Passed);
+
+   procedure Adjust (Container : in out Holder) with
+       Global in  => (null),
+       Global out => (TC_Passed);
+
+   procedure Finalize (Container : in out Holder) with
+       Global in  => (TC_Count),
+       Global out => (TC_Count);
+
+   -- Neither Adjust nor Initialize should be called on the following:
+   -- (Note: Program_Error probably will be raised here if the test fails.)
+
+   Null_Holder : constant Holder :=
+     (Ada.Finalization.Controlled with Type_Kind => JSON_NULL);
+
+   Boolean_Holder : constant Holder :=
+     Holder'(Ada.Finalization.Controlled with Type_Kind => JSON_BOOLEAN);
+
+   String_Holder : constant Holder :=
+     (My_Holder'(Ada.Finalization.Controlled with Type_Kind => JSON_STRING));
+
+end TestV02A;
+
+package body TestV02A is
+
+    function Check_Holder (Container : in Holder; Kind : in JSON_Data_Type)
+        return Boolean is
+        -- Only parameters are used, so the annotations are both (null).
+    begin
+        return Container.Type_Kind = Kind;
+    end Check_Holder;
+
+    procedure Initialize (Container : in out Holder) is
+    begin
+        TC_Passed := False;
+    end Initialize;
+
+    procedure Adjust (Container : in out Holder) is
+    begin
+        TC_Passed := False;
+    end Adjust;
+
+    procedure Finalize (Container : in out Holder) is
+    begin
+        TC_Count := TC_Count + 1;
+    end Finalize;
+
+end TestV02A;
+
+with TestV02A;
+package TestV02B is
+
+    function Generator return TestV02a.JSON_Data_Type with
+        Global in  => (others in TestV02B),
+        Global out => (others in TestV02B);
+        -- We have to use others as the global object is not visible
+        -- in the specification.
+    type Operand is record
+        Kind : TestV02a.JSON_Data_Type := Generator;
+        Obj  : TestV02a.Holder;
+    end record with
+        Global in => (others in TestV02B, TestV02A.TC_Count),
+        Global out => (others in TestV02B, TestV02A.TC_Passed, TestV02A.TC_Count);
+        -- This annotation at least has to cover the annotations of the component
+        -- types and anything used by the default expressions. But it can cover
+        -- more: (others) could have been used, or (others in TestV02B, others in TestV02a).
+
+    procedure Do_It_Once (O : in Operand) with
+        Global in => (others in TestV02B, TestV02A.TC_Count),
+        Global out => (others in TestV02B, TestV02A.TC_Passed, TestV02A.TC_Count);
+
+    function OK return Boolean with
+        Global in => (TestV02A.TC_Passed, TestV02A.TC_Count),
+        Global out => (null);
+
+end TestV02B;
+
+package body TestV02B is
+
+    Seed : TestV02a.JSON_Data_Type := TestV02a.JSON_NULL;
+
+    function Generator return TestV02a.JSON_Data_Type is
+       use type TestV02a.JSON_Data_Type;
+    begin
+       if Seed /= TestV02a.JSON_Data_Type'Last then
+          Seed := TestV02a.JSON_Data_Type'Succ(Seed);
+       else
+          Seed := TestV02a.JSON_Data_Type'First;
+       end if;
+       return Seed;
+    end Generator;
+
+    procedure Do_It_Once (O : in Operand) is
+        Copy_of_O : Operand := O;
+            -- The annotations of Operand are required to be covered
+            -- because of this declaration.
+    begin
+       TestV02A.Check_Holder (Copy_of_O, TestV02a.JSON_NULL);
+    end Do_It_Once;        
+
+    function OK return Boolean is
+    begin
+        return TestV02A.TC_Passed and (TestV02A.TC_Count = 3);
+    end OK;
+
+end TestV02B;
+
+---
+
+Annotations of instances are substituted. For instance, for the following
+instantiation of Ada.Containers.Bounded_Vectors:
+
+   subtype Short_Int is Natural range 0 .. 1000;
+   package Int_Vect is new Ada.Containers.Bounded_Vectors (Short_Int, Integer);
+
+In this case, the annotations for the actual corresponding to "Generic Element_Type"
+would be "Global in out => (null)", as would the annotations for "=". That means that
+almost all of the annotations of the types and routines in the instance would become
+"Global in out => (null)", meaning that the permission to remove extra calls would
+be active.
+
+On the other hand, if a type like Holder above was used as the element type:
+
+   package Holder_Vect is new Ada.Containers.Bounded_Vectors (Short_Int,
+                                                 TestV02a.Holder);
+
+In this case, the annotations for the actual corresponding to "Generic Element_Type"
+would be "Global in  => (TestV02A.TC_Count),
+          Global out => (TestV02A.TC_Passed, TestV02A.TC_Count)"
+and the annotations for "=" would be "Global in out => (others)" (since they were
+not specified).
+
+Thus the effective annotations for "=" in the Holder_Vect instance would be
+Global in out => (others), while those for Element (by index) would be
+Global in  => (TestV02A.TC_Count),
+Global out => (TestV02A.TC_Passed, TestV02A.TC_Count), and those for
+function Length would still be Global in out => (null).
 
-** TBD **
 
 !ACATS test
 

Questions? Ask the ACAA Technical Agent