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

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

--- ai05s/ai05-0186-1.txt	2010/02/02 04:49:02	1.5
+++ ai05s/ai05-0186-1.txt	2010/02/04 07:10:51	1.6
@@ -1,4 +1,4 @@
-!standard 13.3.4 (0)                                10-02-01  AI05-0186-1/04
+!standard 13.3.4 (0)                                10-02-03  AI05-0186-1/05
 !class amendment 09-11-02
 !status work item 09-11-02
 !status received 09-11-02
@@ -12,26 +12,26 @@
 
 !problem
 
-We're considering adding many kinds of annotations to Ada (see AI05-0145-1 and
+We're considering adding many aspects to Ada (see AI05-0145-1 and
 AI05-0146-1) 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 annotations,
-a tool has to assume the worst about any user-defined functions. That is, that
+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" annotations, to erroneous execution.
+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 annotations are available. This is
+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
 require creating pseudo body dependencies (if the body is changed, any analysis
-depending on that properties of that body would have to be performed again); but
+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).
 
@@ -46,9 +46,9 @@
 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 annotations for types cover default
+initialization/adjustment/finalization. The global annotations for packages
+cover operations that occur as part of the elaboration for packages.
 
 !wording
 
@@ -56,8 +56,9 @@
 
 13.3.4 Global usage annotation
 
-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.]
+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-0183-1:
 
@@ -94,18 +95,24 @@
 
 Static Semantics
 
-A read or write of an object O is *covered by an annotation* in an
+An *annotation* is defined by an Annotation_List.
+
+[Editor's note: This is probably overly broad, but it was the meaning that I used
+throughout the wording, and this is the best way to fix that without rewriting all
+of the wording.]
+
+A read or write of an object Obj is *covered by an annotation* in an
 Annotation_List if:
-    * O statically denotes a part of an object named in the Annotation_List;
+    * Obj statically denotes a part of an object named in the Annotation_List;
     * 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 pool-specific access type whose
+      Obj denotes part of an object declared in P, or Obj denotes a part of an object
+      produced by a dereference of an object of a pool-specific access type whose
       pool is declared in P;
-    * O denotes a part of an object produced by a dereference of an object with
+    * Obj denotes a part of an object produced by a dereference of an object with
       designated type T, and the type D given in an ACCESS D
       annotation item covers T; or
-    * O denotes a part of an object produced by a dereference of an object of
+    * Obj denotes a part of an object produced by a dereference of an object of
       a pool-specific access type named in the Annotation_List.
 
 AARM Ramification: OTHERS by itself allows anything to be read or written.
@@ -117,10 +124,11 @@
 "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:
+An annotation defined by an Annotation_List A1 is *compatible* with another such
+annotation A2 if:
     * A1 contains NULL; or
     * A2 contains the annotation item OTHERS without a package name; or
-    * All of the following must be true:
+    * All of the following are true:
       -- 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;
@@ -131,14 +139,14 @@
 
       -- 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, 
+         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)).
+AARM Ramification: This definition is not symmetrical; A2 may allow more object
+access than A1 allows (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
@@ -184,21 +192,21 @@
      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
+Analogous rules apply to a Global out annotation (replacing "Global in" by "Global out" and
 "read" by "written" everywhere).
 
-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.
+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.
+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.
+The aspect Global shall be given only on subprograms, generic subprograms, types,
+packages, and generic packages.
 
 The aspect Global'Access shall be given only on access-to-subprogram types.
 
@@ -217,9 +225,9 @@
 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:
+If a subprogram or generic 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
+    from the subprogram call, be a constant object of an elementary type, or be
     covered by the Global in annotation.
   * The subprogram corresponding to each dispatching call in the subprogram body
     which has a dynamically tagged controlling operand shall have a compatible
@@ -228,8 +236,8 @@
     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.
+  * The type of every stand-alone object declared by the subprogram shall have
+    a compatible Global in annotation.
   * Every nested package and package instantiation declared by the subprogram
     shall have a compatible Global in annotation.
   * The type of each assignment_statement in the subprogram body shall be compatible
@@ -243,7 +251,8 @@
 
   * The Allocate and Deallocate routines associated with the storage pool for the
     type of each allocator in the subprogram body shall have compatible Global in
-    annotations.
+    annotations, and the type of the allocated object shall have a compatible
+    Global in annotation.
 
     AARM Reason: Again, Deallocate can be called here if the implementation chooses;
     we have to assume the worst.
@@ -266,7 +275,7 @@
 Note that this is referring to constant objects, not just constant views of an
 object.
 
-A write of a dereference of an object P *reads* the object P (and writes the 
+A write of a dereference of an object P *reads* the object P (and writes the
 designated object).
 
 The prefix of a protected function call is considered to be
@@ -287,10 +296,10 @@
 
 [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'Access in
-annotation, subprogram P shall have a compatible Global in annotation. Similarly,
-for a type S that has a Global'Access out annotation, subprogram P shall have a
-compatible Global out annotation.
+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'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.]
@@ -335,7 +344,8 @@
        each allocator in E shall have a compatible Global in annotation.
      * The Allocate and Deallocate routines associated with the storage pool for the
        type of each allocator in E shall have compatible Global in
-       annotations.
+       annotations, and the type of the allocated object 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.
@@ -372,12 +382,14 @@
      * the Allocate routine associated with the storage pool for the type of
        each allocator in E shall have a compatible Global in annotation.
      * The Allocate and Deallocate routines associated with the storage pool for the
-       type of each allocator in E shall have compatible Global in annotations.
+       type of each allocator in E shall have compatible Global in annotations,
+       and the type of the allocated object 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 be compatible
-    with the annotation.
+  * The type of every stand-alone object declared by the package shall have
+    a compatible Global in annotation.
   * Every nested package and package instantiation declared by the package
     shall have a compatible Global in annotation.
   * The type of each assignment_statement in the sequence_of_statements of the
@@ -461,7 +473,7 @@
 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. 
+annotations are accurate, even though this cannot be 100% certain.
 
 ---
 
@@ -707,7 +719,7 @@
 
    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);
@@ -826,7 +838,7 @@
 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]; 
+be given on the full type];
 
 Global annotations can be given on private types; if so, they are
 enforced on the full type as well.
@@ -1088,7 +1100,7 @@
             -- because of this declaration.
     begin
        TestV02A.Check_Holder (Copy_of_O, TestV02a.JSON_NULL);
-    end Do_It_Once;        
+    end Do_It_Once;
 
     function OK return Boolean is
     begin
@@ -1637,6 +1649,7 @@
 Following is an example of a type that would be problematic without the
 requirement to annotate hidden access types.
 
+private with Ada.Finalization;
 package Clones is
 
     type Clonee is tagged private
@@ -1647,7 +1660,7 @@
 
     function Cnt (Obj : in Clonee) return Natural with
        Global in => (others in Clones), Global out => (null);
- 
+
     function Ave (Obj : in Clonee) return Natural with
        Global in => (others in Clones), Global out => (null);
 
@@ -1663,13 +1676,15 @@
     end record;
     type Data_Access is access Data;
 
-    type Clonee is tagged record
+    type Clonee is new Ada.Finalization.Controlled with record
         Data : Data_Access;
     end record;
 
+    overriding
     procedure Adjust (Obj : in out Clonee) with
        Global in out => (others in Clones);
 
+    overriding
     procedure Finalize (Obj : in out Clonee)
        Global in out => (others in Clones);
 
@@ -1687,7 +1702,7 @@
     begin
         return Obj.Data.Cnt;
     end Cnt;
- 
+
     function Ave (Obj : in Clonee) return Natural is
     begin
         return Obj.Data.Ave;
@@ -1739,5 +1754,1354 @@
 Note that if the Reset operation would have been some call unrelated
 to package Clones, the optimization would have been allowed, as the
 value of B could not have changed (even though it contains "global" data).
+
+****************************************************************
+
+From: Bob Duff
+Sent (privately): Tuesday, February 2, 2010  3:51 PM
+
+> 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,
+
+Hmm.  I thought our philosophy was that assertions are either checked, or not,
+depending on the mode, but do not otherwise affect the semantics.  An
+implementation can have a mode where it optimizes based on the assumption that
+assertions are true (and perhaps the assumption that they don't have
+"interesting" side effects), but we don't define such modes in the language.
+
+Seems to me globals annotations are similar, and we should take a similar
+attitude.  That is, globals annotations are there to support assertions, not to
+help the optimizer.  (But of course, an implementation can have a mode where
+they help the optimizer.)
+
+****************************************************************
+
+From: Randy Brukardt
+Sent (privately): Wednesday, February 3, 2010  6:24 PM
+
+Steve Baird wrote:
+
+> Your goal of explicitly defining the static semantics (as opposed to a
+> 10.2.1(5)-style cheat) is laudable, but it seems like there are bound
+> to be holes even though (or perhaps
+> because) the proposed change seems enormous.
+>
+> Do we deal with the initialization side-effects of an uninitialized
+> allocator? Streaming attributes? Finalization of aggregate temps?
+
+Yes (in version /05). The model is that the type of any object that is
+declared/created by the syntax of a subprogram body requires that it's
+annotation is covered. If the wording is missing for some case, it needs to be
+added.
+
+Yes. Streaming attributes are subprograms, and as such have annotations of
+Global in out => (others) [because we didn't define them to be something else].
+And the normal call rules apply. One could imagine trying to do better, but as
+you imply, that would be hard.
+
+I don't know, because I don't know what you mean by an "aggregate temp". Last
+night, I thought you meant the logical copy required by the canonical semantics,
+and the answer to that is yes (since the annotation of the type of any
+assignment has to be compatible, which covers the finalization of that type as
+well as the Adjustment; similarly, the finalization of any component types of T
+is covered by the annotation for the T, so any component aggregate temporaries
+are necessarily covered), but that seems so obvious that perhaps you had
+something else in mind (I know how deviously your mind works. :-)
+
+> And an implementation permission such as
+>
+>     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.
+>
+> really raises the stakes here. This means that we can't, for example,
+> punt on defining the rules for some constructs. We don't want to allow
+> omitting a call to
+>
+>     procedure P with global out null is
+>     begin
+>        abort The_Runaway_Task;
+>     end P;
+> or
+>     procedure Q with global out null is
+>     begin
+>         raise We_Are_Approaching_An_Iceberg;
+>     end Q;
+
+Why not? We allow exactly that for pragma Pure, and global out (null) is
+*stronger* than pragma Pure. I believe that both of these are legal for a
+subprogram in a pragma Pure package, and the rule for Pure packages allows both
+of these calls (indeed, *any* procedure call that doesn't have a modifiable
+parameter).
+
+[Aside: The second case illustrates the need for exception contracts better than
+anything I could ever say, but we've all agreed that those are too complex for
+this go-around. They ought to exist and have similar rules to these global
+annotations: a possible raise of an exception not handled and not covered by the
+contract is illegal.]
+
+> I understand that these annotations are different than Assert pragmas
+> because they are statically checked. Nonetheless, I would feel more
+> comfortable if these annotations had no language-defined effects on
+> dynamic semantics.
+>
+> If a compiler wants to make use of annotations in performing
+> optimizations and is able to perform whatever analysis is needed in
+> order to conclude that some transformation is safe, then fine.
+> If we do a good job of defining these annotations, the existing
+> permissions should suffice and no new permissions should be needed.
+
+I don't buy any of this; I think your world view of these annotations is wrong.
+
+These are *facts* about a subprogram; they're part of the *contract* of the
+subprogram. A subprogram which violates its global annotations is wrong, whether
+or not the compiler detects it. The compiler detection is just an aid to help
+ensure that the program meant what they said. In that sense, it is no different
+than "aliased"; the compiler is allowed to assume that an untagged object
+without that notation is not going to be designated by an access type, even
+though there exist a number of ways to have that effect.
+
+One possible approach to that would be to say that outright:
+
+Erroneous Execution
+
+If a subprogram evaluates, elaborates, or executes an operation or statement
+that accesses an entity that is not covered by its Global in annotation, or
+modifies an entity that is not covered by its Global out annotation, execution
+is erroneous. In particular, execution of a subprogram with a Global out =>
+(null) annotation that modifies any non-local entity other than its parameters
+is erroneous.
+
+Since an erroneous subprogram can do anything at all, doing nothing at all would
+be a valid implementation.
+
+I don't particularly want to go this way, because we already have a more
+restricted permission than that in the Ada language, and it makes sense to copy
+it. And wording this normatively is likely to engender more controversy than is
+worthwhile. But the above is  how I think about Globals annotations (and pragma
+Pure, for that matter).
+
+---
+
+It is my opinion that this feature (and by corollary, all of the contract
+proposals) is not worthwhile unless the compiler is allowed to rely on the
+contracts. The basic problem is, if a tool cannot rely on the contracts unless
+it can verify their correctness, you are essentially requiring full-source
+analysis only. If you are willing to require that, you don't need *any* language
+feature; the entire point is to strengthen the contracts for analysis even
+before the body exists. (And that surely includes analysis by the compiler - I
+don't see why we should have a double standard for compilers and for other
+tools.)
+
+The problem here is that if the compiler isn't allowed to use the contracts,
+there is no justification for including the feature in the language. To
+oversimplify a bit, there are only 4 reasons to add a feature to Ada:
+
+(1) To improve the readability/expressiveness of the language;
+(2) To improve static error detection (legality rules);
+(3) To provide additional runtime correctness checking;
+(4) To improve the capabilities of the compiler to provide better code.
+
+Analyzing this proposal against these 4 criteria:
+(1) Readability is worse, in general, because there is more noise in the
+    specifications. Expressiveness is improved, but it mainly matters in corner
+    cases. This is a net loss. (This is true for all of the contract schemes,
+    IMHO.)
+(2) The only static error detection added here is internal to the new feature.
+    There is nothing added to the existing language. (This is also true for all
+    of the contract schemes.)
+(3) There is no runtime checks proposed here. (The other contracts differ on
+    this one.)
+(4) Yes, the compiler can use the additional information. But that requires
+    being able to assume it is accurate, or requires looking in the body. As
+    noted above, the reason for this feature is to avoid looking in the body, so
+    that is not worth considering. (The other contracts can only be used by the
+    compiler if it can prove that there are no side-effects, so this one is a
+    "no" unless the Global annotations are available.
+
+The net effect of this analysis is that the only language value to this feature
+is from the ability of compilers to use the contracts. If you take that away,
+you are taking it away from other contracts as well (that is, the ability to
+optimize preconditions is eliminated for all but ones consisting solely of
+predefined elementary operators, which will be approximately 0% of real
+preconditions on private types). At that point, the only remaining value is the
+ability of the compiler to produce warnings - but we don't have language
+features about warnings. And the value of the other contracts is also greatly
+compromised; they now have no more benefit than just writing some code at the
+top of the subprogram (which I've been doing for 30 years of Ada programming),
+with the possible exception of full-program analysis tools [and those don't need
+the help, they can figure out what they need to know from the source itself].
+
+So my question is, are we doing *contracts* or *assertions*? If we're doing
+*assertions*, we don't need this AI and I'm not at all interested in any of the
+related AIs [other than the syntax for aspects; it's what Ada should have had in
+the first place]. (The benefit isn't much over assertion pragmas to start with;
+the problems Pascal ranted about cancel out any benefits). In that case, I
+should not waste any of my time on any of those AIs (beyond the basic editorial
+issues. If we're doing *contracts*, we need to get this right, and compilers
+have to be able to take advantage of the information.
+
+To be continued tomorrow. :-)
+
+****************************************************************
+
+From: Bob Duff
+Sent (privately): Tuesday, February 2, 2010  3:51 PM
+
+I'm having trouble understanding this AI, and some others, because AI05-0183-1
+is still up in the air. Tuck, would you mind putting that one at the head of
+your priority queue?
+
+General comments.
+
+I find it difficult to understand this AI (even ignoring the AI05-0183-1 issue).
+I'm not blaming you, Randy -- I think it's just hard.
+
+I think perhaps globals annotations should not apply to nested subprograms.  A
+tool (or a human reader) can reasonably be expected to just figure it out.  All
+the relevant code is just there.  Yes, in case of subunits, the tool needs to do
+an inter-compilation-unit analysis, but I think that's reasonable.
+
+I think it would be useful to have a way to say "The default annotation in this
+scope is 'null' instead of the usual 'others'." Or maybe a general way to set
+the default (e.g. to 'all variables in this package').
+
+I don't buy the idea that tools that make potentially-false assumptions are
+useless.  Suppose a tool assumes X, and proves all kinds of assertions true
+based on that.  And suppose X might be false.  Well, we've still got useful info
+-- we know that "X implies so-and-so" (or, for the imply-o-phobes, "if X then
+so-and-so").  If X is usually true, and can be checked separately (perhaps by
+hand), then it's OK.
+
+One X I'm thinking of here is [De]allocate.  I hate to see all kinds of
+pessimistic assumptions, that basically ruin any attempt to prove anything about
+any subprogram that does 'new' or U_D.  Yeah, the storage pool can have side
+effects, but they're usually at a totally different level from the code that
+invokes them.
+
+Note that pure-functional languages do not consider "new" to be a side effect.
+
+I'm not sure how we intend to deal with low-level chap-13-ish stuff.
+There's a mention of Unchecked_Conversion here, but that's in the same category
+as machine-code inserts, address clauses, etc. Seems to me all these things need
+to be treated the same, namely it's the programmer's responsibility to ....
+
+> Annotations are provided to describe the use of global objects by
+> subprograms.
+>
+> !problem
+>
+> We're considering adding many kinds of annotations to Ada (see
+> AI05-0145-1 and AI05-0146-1) 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
+
+"functions" --> "subprograms".
+
+> annotations, a tool has to assume the worst about any user-defined
+> functions.
+
+When I said this at the last phone meeting, Ed pointed out that there's an
+alternative: whole-program analysis.  So I suggest adding "(or perform
+whole-program analysis)" at the end of the above sentence.  No need to point out
+the drawbacks of that.
+
+>...That is, that the result of a function can change even when
+
+"That is" --> "For example".
+
+> 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" annotations, to erroneous execution.  Both of these
+
+"erroneous" --> "incorrect".
+
+> 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
+> annotations  are available.
+
+OK, I see...
+
+>... 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 require creating
+>pseudo  body dependencies  (if the  body is changed,  any analysis
+>depending on  that properties of that body would  have to be performed
+>again); but the
+
+"that properties" --> "the properties"
+
+> 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.
+>
+> !proposal
+>
+> 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.
+
+Hmm...  Are we really sure it's OK to lump all that together.
+I can imagine being frustrated when I want to give different 'globals' for init
+versus final, e.g.
+
+> !wording
+>
+> Add a new section:
+>
+> 13.3.4 Global usage annotation
+>
+> 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-0183-1:
+>
+>     Aspect_Mark [in|out|in out] => Annotation_List
+>
+>     Annotation_List ::= ( Annotation_Item {, Annotation_Item} )
+>
+>     Annotation_Item ::= *object_*name | *access_*subtype_mark |
+>                          NULL | ACCESS subtype_mark |
+>                          OTHERS [IN *package*name] |
+>                          GENERIC *formal_parameter_*name
+
+A "generic formal parameter" is not a "formal parameter".
+
+> 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 pool-specific 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 (once for "in" and
+> once for "out") to "Aspect_Mark in out".
+>
+> Aspects Global, Global'Class, and Global'Access 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
+
+Please, PLEASE don't use "O" as an object name!
+"X" or "Obj" or ...
+
+> Annotation_List if:
+>     * O statically denotes a part of an object named in the
+> Annotation_List;
+
+I'm not sure "statically denotes" is right, here.
+Don't you want to include a record component X.Y, for example?
+
+>     * 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 pool-specific
+> access type whose
+
+"an" --> "a"
+
+>       pool is declared in P;
+
+Including children and nested packages?
+
+>     * O denotes a part of an object produced by a dereference of an object with
+>       designated type T, and the type D given in an ACCESS D
+>       annotation item covers T; or
+>     * O denotes a part of an object produced by a dereference of an object of
+>       a pool-specific access type named in the Annotation_List.
+>
+> AARM Ramification: OTHERS by itself allows anything to be read or written.
+>
+> AARM Discussion: ACCESS D represents reading/writing of any aliased or
+> tagged object (including those allocated from pools) with a type
+> covered by the type D.
+>
+> "Statically denotes" does not include dereferences, so the first rule
+> only applies to statically declared objects.
+
+I don't think "statically declared" means anything.
+
+> An annotation A1 is *compatible* with another annotation A2 if:
+
+"An annotation"?  We're only talking about globals annotations...
+
+>     * A1 contains NULL; or
+>     * A2 contains the annotation item OTHERS without a package name; or
+>     * All of the following must be true:
+
+"must be" --> "are"
+
+>       -- 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)).
+
+Heh?  I don't get the juxtaposition of "allow" and "requires".
+
+> 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.
+
+This seems to be talking about annotations/aspects in general, not just globals.
+Is that intended?
+
+> 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),
+
+What does "(either..." mean?
+
+> 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.]
+
+Need to merge multiple parents?  Or is that handled below?
+
+> 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 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.
+
+Not generic subprograms?  Entries?  Task bodies?
+
+> The aspect Global'Access shall be given only on access-to-subprogram types.
+>
+> The aspect Global'Class shall be given only on primitive subprograms
+> of a tagged type.
+>
+> The Annotation_Item NULL shall appear alone in an Annotation_List.
+
+Same for "others" (without pkg name)?
+
+> An *object*_name given in an Annotation_List shall statically denote
+> some object.
+>
+> An *access*_subtype_mark given in an Annotation_List shall denote a
+> pool-specific access type.
+
+???Hmm...
+
+> 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
+>     covered by the Global in annotation.
+
+Or be nested inside the subprogram, right?
+
+What does "accessible from the function call" mean?
+(And shouldn't it be "subp call"?)
+
+It seems like a pain to mention constants.  Can we limit this to "nonlimited",
+rather than "elementary"?
+
+>   * 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'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.
+
+I don't get it.
+
+>   * Every nested package and package instantiation declared by the subprogram
+>     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.
+
+Heh?
+
+>   * The Allocate and Deallocate routines associated with the storage pool for the
+>     type of each allocator in the subprogram body shall have compatible Global in
+>     annotations.
+>
+>     AARM Reason: Again, Deallocate can be called here if the implementation chooses;
+>     we have to assume the worst.
+>
+>   * For each attribute A'Storage_Size in the subprogram body 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 subprogram contains a call on an instance of Unchecked_Conversion with
+>     a pool-specific access type A as the target type, the subprogram is
+>     illegal if the type A is named as an *access*_subtype_mark annotation item.
+
+This one seems like overkill.
+
+>     AARM Reason: We assume that objects of type A can only designate objects in
+>     the pool of A. The only way to violate this is to use Unchecked_Conversion
+>     from a general access type value; if such a conversion exists, we require
+>     the subprogram to be annotated as if A is a general access type.
+>
+> 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.
+
+Shouldn't be allowed.
+
+> Note that this is referring to constant objects, not just constant
+> views of an object.
+>
+> A write of a dereference of an object P *reads* the object P (and
+> writes the designated object).
+>
+> The prefix of a protected function call is considered to be read; the
+> prefix of a protected procedure or entry call is considered to be both
+> read and written. The prefix of a task entry is considered to be read.
+> These rules follow from the requirements in 9.5 on whether or not the
+> prefix of a protected subprogram call or an entry call can be a
+> constant; we don't want to be logically writing constants.
+> 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.
+
+So anything that calls U_D has to have "others"?
+
+> End AARM Discussion.
+>
+> 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.]
+
+Agreed!
+
+> 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'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.]
+
+I agree to keeping all these rules together.
+
+================================================================
+
+> (Partial) Minutes of the Amendment subcommittee of the ARG conference
+> call of December 10, 2009
+>
+> Attendees: Bob Duff, Tucker Taft, Randy Brukardt, Steve Baird, Gary
+> Dismukes, Ed Schonberg
+>
+> AI05-0186-1/01
+>
+> Bob says that this is essential if you ever want to do any analysis of
+> programs without all of the source code available.
+>
+> Bob comments that the write up talks about function too much, it
+> should say subprogram more. Tucker notes that this is mainly an issue
+> in !problem. Randy notes that the motivating case has to do with
+> functions, so it just talks about that there.
+
+I don't get that.  I see no difference between a function and a procedure,
+except for syntax.
+
+> Bob wonders if we should talk about variables rather than constants.
+> He doesn't want to annotate reads of global constants. Not all
+> constants are really constants, however. Calling an entry of tasks if
+> side-effect, even if the task is a constant. He is not sure what the
+> right answer is (we could except elementary constants from the rules without problems).
+>
+> Elementary Operators would have null annotations. Randy notes that
+> composition of equality means that we have to exclude composite
+> operators, as they might contain user-defined parts (even array "=" has that problem).
+
+But "and" on boolean arrays, for ex., doesn't mess with globals.
+
+> Steve would like this to preserve the separation of static and dynamic
+> semantics. That is the intent - he notes that Pure does not do that.
+> That means the wording shouldn't talk about what happens at elaboration.
+
+I don't understand Steve's point.
+
+> ****************************************************************
+>
+> Example of access annotations, February 1, 2010, Randy Brukardt
+
+>     type Clonee is tagged record
+>         Data : Data_Access;
+>     end record;
+
+I think you wanted Clonee to be controlled, and say "overriding" on the
+following.
+
+>     procedure Adjust (Obj : in out Clonee) with
+>        Global in out => (others in Clones);
+>
+>     procedure Finalize (Obj : in out Clonee)
+>        Global in out => (others in Clones);
+
+****************************************************************
+
+From: Randy Brukardt
+Sent (privately): Tuesday, February 2, 2010  7:03 PM & Thursday, February 4, 2010
+
+> I'm having trouble understanding this AI, and some others, because
+> AI05-0183-1 is still up in the air.
+> Tuck, would you mind putting that one at the head of your priority
+> queue?
+
+I agree. I left out all of the resolution issues from this AI, as they ought to
+be covered in AI05-0183-1. But they're not there yet.
+
+> General comments.
+>
+> I find it difficult to understand this AI (even ignoring the
+> AI05-0183-1 issue).  I'm not blaming you, Randy -- I think it's just
+> hard.
+
+Well, I do have a tendency to ramble; I often find others (especiall Tucker)
+explaining something I was struggling to put into words much more clearly. So
+I'm certain there is room for improvement.
+
+One thing that is missing is an overview of the meaning of things. It just jumps
+into wording, so you are missing a roadmap. Perhaps that would be a good
+assignment for you to undertake (it would bring a fresh perspective as well).
+
+> I think perhaps globals annotations should not apply to nested
+> subprograms.  A tool (or a human reader) can reasonably be expected to
+> just figure it out.  All the relevant code is just there.  Yes, in
+> case of subunits, the tool needs to do an inter-compilation-unit
+> analysis, but I think that's reasonable.
+
+I am 100% against any sort of inter-compilation unit analysis. Janus/Ada has no
+such capability and will get one over my dead body. (I believe body dependencies
+are the root of all evil; we don't have any.)
+
+Anything separately compiled needs proper contracts. Period.
+
+As a lesser issue, doing that would greatly complicate the wording, because now
+you'd have to include everything present (logically) in the body, not just
+syntactically in the body. I designed the rules here to only require talking
+about things in the syntax.
+
+> I think it would be useful to have a way to say "The default
+> annotation in this scope is 'null' instead of the usual 'others'."
+> Or maybe a general way to set the default (e.g. to 'all variables in
+> this package').
+
+Maybe, but this is so complex already that I am dubious that making it more
+complex is very helpful. And the experience with the containers shows that the
+annotations vary from routine to routine (depending on proc vs. func, and reader
+versus modifier).
+
+> I don't buy the idea that tools that make potentially-false
+> assumptions are useless.  Suppose a tool assumes X, and proves all
+> kinds of assertions true based on that.  And suppose X might be false.
+> Well, we've still got useful info
+> -- we know that "X implies so-and-so" (or, for the imply-o-phobes, "if
+> X then so-and-so").  If X is usually true, and can be checked
+> separately (perhaps by hand), then it's OK.
+
+Well, it is useless for a compiler to optimize based on such assumptions
+(optimize here includes reducing/removing assertions/preconditions/etc.) That's
+because doing so can introduce erroneousness into programs that don't have any.
+That's beyond bad.
+
+I make no claims about what stand-alone tools can or can't do. I don't believe
+in them much; I believe more in the omnipitant compiler.
+
+> One X I'm thinking of here is [De]allocate.  I hate to see all kinds
+> of pessimistic assumptions, that basically ruin any attempt to prove
+> anything about any subprogram that does 'new' or U_D.  Yeah, the
+> storage pool can have side effects, but they're usually at a totally
+> different level from the code that invokes them.
+
+I'll address this particular issue later; it doesn't need to be assume-the-worst
+in general. I just didn't address it to keep the size of the proposal from
+getting out of hand.
+
+> Note that pure-functional languages do not consider "new" to be a side
+> effect.
+
+They don't have pools and cross-links, though, and those are the problem case.
+If we don't handle those properly, these annotations will be worse than useless,
+they'll be actively misleading.
+
+> I'm not sure how we intend to deal with low-level chap-13-ish stuff.
+> There's a mention of Unchecked_Conversion here, but that's in the same
+> category as machine-code inserts, address clauses, etc.
+> Seems to me all these things need to be treated the same, namely it's
+> the programmer's responsibility to ....
+
+The Unchecked_Conversion rules is specifically to plug a hole related
+conversions into pool-specific access types. That's a common thing to do in Ada
+83 code, and I didn't think it was a good idea to ignore it for that reason.
+
+In all other cases, we are talking about erroneous code (or code that ought to
+be declared that way, I think the rule for machine code insertions is missing,
+there ought to be one like the one for interfaces); and there never is a
+requirement in Ada that erroneous code does anything sane. In addition, I don't
+expect lying about Global annotation for Imported/Exported subprogram, broken
+machine code insertions, or abuse of
+Unchecked_Conversion/Address_to_Access_Conversions (there is only a problem if
+the designated type is incorrect) to be common. (Unlike the Unchecked_Conversion
+to pool-specific access types.)
+
+> > Annotations are provided to describe the use of global objects by
+> > subprograms.
+> >
+> > !problem
+> >
+> > We're considering adding many kinds of annotations to Ada (see
+> > AI05-0145-1 and AI05-0146-1) 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
+>
+> "functions" --> "subprograms".
+>
+> > annotations, a tool has to assume the worst about any user-defined
+> > functions.
+
+You can't use any subprograms other than functions in
+assertions/preconditions/etc. "Annotations" really is the wrong term here;
+they're really "contract aspects".
+
+> When I said this at the last phone meeting, Ed pointed out that
+> there's an alternative: whole-program analysis.  So I suggest adding
+> "(or perform whole-program analysis)" at the end of the above
+> sentence.  No need to point out the drawbacks of that.
+
+As you later note, the next paragraph covers that. Do I need to say something
+here?
+
+> >...That is, that the result of a function can change even when
+>
+> "That is" --> "For example".
+>
+> > 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" annotations, to erroneous execution.  Both of these
+>
+> "erroneous" --> "incorrect".
+
+I really meant "erroneous". If checks that fail are suppressed, execution is
+erroneous. That's what's happening here (the compiler suppressing checks that
+need to be made).
+
+> > 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
+> > annotations  are available.
+>
+> OK, I see...
+>
+> >... 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 require creating
+> >pseudo  body dependencies  (if the  body is changed,  any analysis
+> >depending on  that properties of that body would  have to be
+> performed
+> >again); but the
+>
+> "that properties" --> "the properties"
+>
+> > 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.
+> >
+> > !proposal
+> >
+> > 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.
+>
+> Hmm...  Are we really sure it's OK to lump all that together.
+> I can imagine being frustrated when I want to give different 'globals'
+> for init versus final, e.g.
+
+I don't know. We decided that during a phone call (the one before the previous
+one). Not doing thing would make things three times more complex, and all of the
+examples I've looked at show that there isn't any difference in practice except
+for ACATS test counters and the like.
+
+> > !wording
+> >
+> > Add a new section:
+> >
+> > 13.3.4 Global usage annotation
+> >
+> > 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-0183-1:
+> >
+> >     Aspect_Mark [in|out|in out] => Annotation_List
+> >
+> >     Annotation_List ::= ( Annotation_Item {, Annotation_Item} )
+> >
+> >     Annotation_Item ::= *object_*name | *access_*subtype_mark |
+> >                          NULL | ACCESS subtype_mark |
+> >                          OTHERS [IN *package*name] |
+> >                          GENERIC *formal_parameter_*name
+>
+> A "generic formal parameter" is not a "formal parameter".
+
+So what is it?
+
+> > 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 pool-specific 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 (once
+> for "in" and
+> > once for "out") to "Aspect_Mark in out".
+> >
+> > Aspects Global, Global'Class, and Global'Access 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
+>
+> Please, PLEASE don't use "O" as an object name!
+> "X" or "Obj" or ...
+
+OK.
+
+> > Annotation_List if:
+> >     * O statically denotes a part of an object named in the
+> > Annotation_List;
+>
+> I'm not sure "statically denotes" is right, here.
+> Don't you want to include a record component X.Y, for example?
+
+We definitely have to use "statically denotes" (or something similar), because
+we don't want to include anything with dynamic parts:
+
+    Obj : T renames Ptr.all;
+
+Don't want Obj in an annotation, but it "denotes" an object - but it doesn't
+"statically denote" an object.
+
+I don't much care about record components; I was thinking mainly of top-level
+objects. But I thought that "statically denotes" did apply to record components
+so long as the prefix is something that can be "statically denoted". I'll have
+to go back and read the definition again.
+
+
+> >     * 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 pool-specific
+> > access type whose
+>
+> "an" --> "a"
+>
+> >       pool is declared in P;
+>
+> Including children and nested packages?
+
+Good question. I would say nested yes, children no, but I don't know how to
+enforce that. (Nested yes because they can be totally hidden in the private
+part, and we don't want to have no possible annotation for them.)
+
+> >     * O denotes a part of an object produced by a dereference of an object with
+> >       designated type T, and the type D given in an ACCESS D
+> >       annotation item covers T; or
+> >     * O denotes a part of an object produced by a dereference of an object of
+> >       a pool-specific access type named in the Annotation_List.
+> >
+> > AARM Ramification: OTHERS by itself allows anything to be
+> read or written.
+> >
+> > AARM Discussion: ACCESS D represents reading/writing of any
+> aliased or
+> > tagged object (including those allocated from pools) with a type
+> > covered by the type D.
+> >
+> > "Statically denotes" does not include dereferences, so the
+> first rule
+> > only applies to statically declared objects.
+>
+> I don't think "statically declared" means anything.
+
+Well, what you you say instead? I'm talking about objects that are declared
+(ultimately) by declarations that are known statically.
+
+> > An annotation A1 is *compatible* with another annotation A2 if:
+>
+> "An annotation"?  We're only talking about globals annotations...
+
+"annotation" throughout this wording is short for "Annotation_List", the syntax
+here. This syntax is only used (currently) for the family of globals
+annotations, but there are already three such aspects (and in and out versions
+of each). I probably ought to look at this more carefully.
+
+"An annotation defined by an Annotation_List is *compatible* with another such
+annotation A2 if:
+
+Or something like that.
+
+> >     * A1 contains NULL; or
+> >     * A2 contains the annotation item OTHERS without a
+> package name; or
+> >     * All of the following must be true:
+>
+> "must be" --> "are"
+
+OK.
+
+...
+> > AARM Ramification: This definition is not symmetrical; A2 may allow
+> > more than
+> > A1 requires (such as having an annotation of (others)).
+>
+> Heh?  I don't get the juxtaposition of "allow" and "requires".
+
+I probably meant "requires it to allow" or something like that, but I agree that doesn't make much sense.
+
+"...allow more object accesses than A2 allows..."
+
+> > 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.
+>
+> This seems to be talking about annotations/aspects in general, not
+> just globals.  Is that intended?
+
+Again, there are three aspects in question (Global, Global'Class,
+Global'Access), and I've thought in the past we needed more.
+
+> > 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),
+>
+> What does "(either..." mean?
+
+either specified explicitly by the programmer (in the source code), or specified
+by the Standard (as for scalar operators, etc.)
+
+> > 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.]
+>
+> Need to merge multiple parents?  Or is that handled below?
+
+I wasn't expecting abstract or null subprograms to have annotations, but perhaps
+they ought to. Otherwise, though, you'd only inherit from a concrete parent, and
+there can only be one of those. Probably needs more wording.
+
+...
+> > The aspect Global shall be given only on subprograms,
+> types, packages,
+> > and generic packages.
+>
+> Not generic subprograms?  Entries?  Task bodies?
+
+Blah. Forgot the first. The last isn't necessary; the annotation can (and
+should) be given on the type. But I suppose we need a whole set of rules for
+checking a task body. Barf. We need to find a way to share the rules: I couldn't
+do it.
+
+Entries is problematic because task entries don't have "bodies" per se, so I
+don't know how to define what to check.
+
+> > The aspect Global'Access shall be given only on
+> access-to-subprogram types.
+> >
+> > The aspect Global'Class shall be given only on primitive
+> subprograms
+> > of a tagged type.
+> >
+> > The Annotation_Item NULL shall appear alone in an Annotation_List.
+>
+> Same for "others" (without pkg name)?
+
+We could do that, I though it was better to be able to say:
+
+    Global in => (Global_Counter, Wishing_Well, others)
+
+which means that you access the two named items and unspecified other stuff.
+
+But it isn't a big deal (you can't prove much additional with the above).
+
+> > An *object*_name given in an Annotation_List shall statically denote
+> > some object.
+> >
+> > An *access*_subtype_mark given in an Annotation_List shall denote a
+> > pool-specific access type.
+>
+> ???Hmm...
+
+I thought it was very confusing to have both with very different semantics.
+Tucker is now suggesting turning this whole model upside down. If we do that,
+then this annotation has to go away anyway (it would conflict with other
+meanings).
+
+> > 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
+> >     covered by the Global in annotation.
+>
+> Or be nested inside the subprogram, right?
+>
+> What does "accessible from the function call" mean?
+> (And shouldn't it be "subp call"?)
+
+Perhaps if you put this this question together with the previous paragraphs
+question, you'd see that one is the answer to the other. "Accessible from the
+function call" (which is a dynamic concept checked statically) includes the
+locals and the parameters: it's the accessibility from AI-142-4.
+
+> It seems like a pain to mention constants.
+
+We don't *have* to mention them, but then you'd have to annotate them. You said
+you didn't want that.
+
+>  Can we limit this
+> to "nonlimited", rather than "elementary"?
+
+No. Go back and read AI05-0054-2 again. We could say "types that cannot have
+parts of immutably limited or controlled types", but that is pretty much the
+same as "elementary" statically. You can't include any parts of private types,
+any classwide types, etc. That leaves String and Complex and not much else. The
+rule would take a whole paragraph by itself to define, and that would make this
+thing much more complex.
+
+> >   * 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'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.
+>
+> I don't get it.
+
+Words missing. And the intended wording is too complex anyway. "shall have a
+compatible annotation" is better.
+
+> >   * Every nested package and package instantiation declared
+> by the subprogram
+> >     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.
+>
+> Heh?
+
+Go read AI05-0107-1 again.
+
+...
+> >   * If the subprogram contains a call on an instance of
+> Unchecked_Conversion with
+> >     a pool-specific access type A as the target type, the
+> subprogram is
+> >     illegal if the type A is named as an
+> *access*_subtype_mark annotation item.
+>
+> This one seems like overkill.
+
+As I mentioned yesterday, this is so common in Ada 83 code that I thought it
+ought to be included. It completely destroys the model of pool-specific access
+types, and most importantly, it is *not* erroneous for it to do that.
+
+> >     AARM Reason: We assume that objects of type A can only
+> designate objects in
+> >     the pool of A. The only way to violate this is to use
+> Unchecked_Conversion
+> >     from a general access type value; if such a conversion
+> exists, we require
+> >     the subprogram to be annotated as if A is a general access type.
+> >
+> > 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.
+>
+> Shouldn't be allowed.
+
+Locals or parameter can't be because of visiblity. I see no reason to disallow
+giving constants (especially for reading purposes), it just isn't going to have
+much effect.
+
+...
+> > 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.
+>
+> So anything that calls U_D has to have "others"?
+
+That's the current model, because at some point we have to stop. Each new thing
+we try to annotate is more work and possible errors.
+
+It wouldn't be that hard to annotate U_D, because it could use the annotation of
+the pool's Deallocate routine. I'm not certain that is enough, however.
+
+...
+> > Bob comments that the write up talks about function too much, it
+> > should say subprogram more. Tucker notes that this is
+> mainly an issue
+> > in !problem. Randy notes that the motivating case has to do with
+> > functions, so it just talks about that there.
+>
+> I don't get that.  I see no difference between a function and a
+> procedure, except for syntax.
+
+The motivating case is in precondition expressions. If you can explicitly call a
+procedure there, you aren't using Ada. Talking about something you can't do in
+the context of discussion isn't helpful.
+
+The actual rules are on subprograms, of course.
+
+You made the same mistake in the AI-147 problem; it's a problem statement, not a
+general statement of usefulness. It's not a laundry list!
+
+...
+> > Elementary Operators would have null annotations. Randy notes that
+> > composition of equality means that we have to exclude composite
+> > operators, as they might contain user-defined parts (even
+> array "=" has that problem).
+>
+> But "and" on boolean arrays, for ex., doesn't mess with globals.
+
+The actual rules go further; I'm not sure why you are reading these !appendix
+minutes rather than the actual proposal.
+
+> > Steve would like this to preserve the separation of static
+> and dynamic
+> > semantics. That is the intent - he notes that Pure does not
+> do that.
+> > That means the wording shouldn't talk about what happens at
+> elaboration.
+>
+> I don't understand Steve's point.
+
+Legality Rules should not depend on Dynamic Semantics rules. Elaboration is a
+dynamic semantics rule. Steve can expand if I oversimplified.
+
+****************************************************************
+
+From: Bob Duff
+Sent (privately): Tuesday, February 2, 2010  8:31 PM
+
+> > Note that pure-functional languages do not consider "new" to be a
+> > side effect.
+>
+> They don't have pools and cross-links, though, and those are the
+> problem case. If we don't handle those properly, these annotations
+> will be worse than useless, they'll be actively misleading.
+
+What do you mean by "cross links"?
+
+Yes, pure-functional languages typically don't have pools.
+But if they did, I don't think it would change things in this regard.  Of
+course, the real issue is that such languages don't have pointer equality (e.g.
+Lisp's 'eq').
+
+****************************************************************
+
+From: Randy Brukardt
+Sent (privately): Thursday, February 4, 2010  12:55 AM
+
+> What do you mean by "cross links"?
+
+I mean when objects share other objects, as in the example I put in the
+!appendix.
+
+> Yes, pure-functional languages typically don't have pools.
+> But if they did, I don't think it would change things in this regard.
+> Of course, the real issue is that such languages don't have pointer
+> equality (e.g. Lisp's 'eq').
+
+Pure functional languages never share objects, do they? Everything is by-copy,
+at least logically. So this is a very different problem.
 
 ****************************************************************

Questions? Ask the ACAA Technical Agent