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

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

--- ai05s/ai05-0186-1.txt	2009/11/03 03:36:22	1.1
+++ ai05s/ai05-0186-1.txt	2009/11/03 06:46:27	1.2
@@ -1,4 +1,4 @@
-!standard 13.15 (0)                                09-11-02  AI05-0186-1/01
+!standard 13.3.4 (0)                                09-11-02  AI05-0186-1/01
 !class amendment 09-11-02
 !status work item 09-11-02
 !status received 09-11-02
@@ -46,34 +46,30 @@
 
 !wording
 
-Semi-formal description:
+Semi-formal description (presumably in Section 13.3.4):
 
 Add to the aspect syntax given in AI05-0184-1:
 
-    Aspect_Mark => BODY Annotation_List
+    Aspect_Mark [in|out] => Annotation_List
 
-[Note: I'm using "Body" here to differentiate this list from
-the normal expression used for other aspects. That's necessary so
-that special resolution
+    Annotation_List ::= ( Annotation_Item {, Annotation_Item} )
 
-    Annotation_List ::= Annotation_Item {, Annotation_Item}
-
     Annotation_Item ::= *object_*name | *access_subtype_*name |
-                         NULL | PRIVATE [IN *package*name]
+                         NULL | OTHERS [IN *package*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.
 
-Aspects Global_In and Global_Out are defined.
+Aspect Global is defined.
 
 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 PRIVATE without a package name occurs in the list;
-    * The annotation PRIVATE with a package name P occurs in the list, and
+    * The annotation OTHERS without a package name occurs in the list;
+    * The annotation OTHERS with a package name P occurs in the list, and
       O denotes 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
     * O denotes a part of an object produced by a dereference of an object of
@@ -83,12 +79,12 @@
 
 An annotation A1 is *compatible* with another annotation A2 if:
     * A1 contains NULL; or
-    * A2 contains the annotation PRIVATE without a package name; or
+    * A2 contains the annotation 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 PRIVATE annotation with a package name P, there is
-      -- a PRIVATE annotation in A2 that statically denotes P.
+      -- For each OTHERS annotation with a package name P, there is
+         a OTHERS annotation in A2 that statically denotes P.
 
 AARM Ramification: This is not symeterical.
 
@@ -100,21 +96,21 @@
 An *object*_name given in an Annotation_List shall statically denote some
 object.
 
-If a subprogram contains a Global_In annotation, then:
+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, or be covered by the Global_In annotation.
-  * every call in the subprogram body shall have a compatible Global_In annotation.
+    from the function call, or be covered by the Global in annotation.
+  * every call in the subprogram body shall have a compatible Global in annotation.
 
 [The first part means that the object has the accessibility of the function
 call.]
 
 AARM Ramification: Local objects and the parameters of the call do not need to
-appear in a Global_In annotation.
+appear in a Global in annotation.
 
-If a subprogram contains a Global_Out annotation, then:
+If a subprogram contains a Global out annotation, then:
   * every object that is written by the subprogram body shall either be accessible
-    from the function call, or be covered by the Global_Out annotation.
-  * every call in the subprogram body shall have a compatible Global_Out annotation.
+    from the function call, or be covered by the Global out annotation.
+  * every call in the subprogram body shall have a compatible Global out annotation.
 
 
 ---
@@ -122,18 +118,18 @@
 Add to 4.5:
 
 Unless otherwise specified, the predefined operators of the language all have
-implied annotations of Global_In => null, Global_Out => null.
+implied annotations of Global in => (null), Global out => (null).
 
 [Do we want to give annotations to other operations, such as some of those
 in the containers?]
 
 [We could define that language-defined Pure subprograms that do not have access
-parameters have implied annotations of Global_In => null, Global_Out => null.]
+parameters have implied annotations of Global in => (null), Global out => (null).]
 
 
 !discussion
 
-The global_in and global_out annotations are intended to be descriptive.
+The global in and global out annotations are intended to be descriptive.
 That is, the annotations describe the behavior of the subprogram body.
 As such, these annotations are checked. There is no benefit to be gained
 from lying about side-effects; such incorrect information could easily lead
@@ -141,7 +137,7 @@
 Moreover, if it is impractical to specify the correct annotations, it makes
 sense to specify none at all.
 
-All of the global_in and global_out annotations proposed can be statically
+All of the global in and global out annotations proposed can be statically
 checked. It is possible to imagine annotations that cannot be statically
 checked, but these are assumptions as opposed to descriptive. Assumptions are
 a different set of annotations.
@@ -153,6 +149,15 @@
 
 ---
 
+The keywords in the syntax are necessary in order that the special syntax
+of this list can be recognized immediately. Otherwise, a massive amount of
+lookahead is needed to parse this (as the list would start the same way as
+the expression used for more typical aspects). We take advantage of the
+fact that Ada already has "in" and "out" keywords to make this syntax
+distinctive but still sensible.
+
+---
+
 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
@@ -163,7 +168,10 @@
 
 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.
+so that implementations can implement it and the checking (even if they are not
+doing semantic analysis now). The information is valuable to have in programs
+for future analysis when improved tools are available. The legality rules
+ensure that the information is accurate.
 
 
 !example

Questions? Ask the ACAA Technical Agent