CVS difference for ai12s/ai12-0079-1.txt

Differences between 1.21 and version 1.22
Log of other versions for file ai12s/ai12-0079-1.txt

--- ai12s/ai12-0079-1.txt	2018/11/13 05:47:38	1.21
+++ ai12s/ai12-0079-1.txt	2018/11/15 21:26:26	1.22
@@ -1,4 +1,4 @@
-!standard 6.1.2(0)                                  18-10-19    AI12-0079-1/08
+!standard 6.1.2(0)                                  18-10-21    AI12-0079-1/09
 !class Amendment 13-06-28
 !status work item 13-06-28
 !status received 13-06-14
@@ -85,17 +85,6 @@
     [for all X convertible to A => X.all]
-Also allow within a Global or Global'Class aspect
-a reference to the set of pointed-to objects reachable from
-a given object (of an access type or a composite type) using the attribute
-P'Reachable.  This attribute can also be used as a predicate to check
-for overlap between the reachable object set and specific objects or
-with another reachable object set, such as "P'Reachable(Obj1, Obj2)" or
-"not P'Reachable(Q'Reachable)."  Also can use this in a postcondition
-to specify when new objects are added or removed from the Reachable set
-(to add: "P'Reachable(Q'Reachable'Old)"; to remove: "not P'Reachable(Obj2)";
-to remove all: "P'Reachable = (<>)").
 2.	Allow the name of a package P to stand-in for the set of objects
 described roughly by:
@@ -134,43 +123,6 @@
-Add after 6.1.1(30.3/5) -- at the end of static semantics:
-  Given an access-to-object type T that has Ownership aspect False (see
-  H.7), an aliased object is /reachable/ from an access object X of type
-  T if the aliased object satisfies the constraints of the designated
-  subtype of T and any constraints that apply to X, and, when T is a
-  pool-specific access type, the aliased object might be part of the
-  collection (see 7.6.1) associated with T. In addition, an aliased
-  object is reachable from X if it is reachable from a part of an object
-  that is itself reachable from X. Reachability from access objects of a
-  type with Ownership aspect True is defined in H.7. An aliased object is
-  /reachable/ from a composite object if the aliased object is reachable
-  from some subcomponent of the composite object.
-    AARM Reason: Reachability is defined in terms of types rather than
-    individual objects, in the absence of "ownership."  See H.7 (AI-0240)
-    for the rules that apply when ownership is True.
-    AARM Ramification: This notion of reachability is very imprecise,
-    and so it is not particularly useful for identifying true data
-    races.  It avoids having to expose particular access types used to
-    represent parts of private types, as X'Reachable essentially
-    represents the set of access types used in the representation of X,
-    without having to name them.  Some notion of ownership, as proposed
-    in AI12-0240, seems essential to identify true data races in the
-    presence of access types.
-  Within the aspect specification for a Post or Post'Class aspect, the
-  following attribute function is defined for an object X of an access
-  or composite type, where global_set is as defined in 6.1.2:
-  X'Reachable (global_set)
-   X'Reachable (global_set) returns True if at least one object in the set
-   identified by the global_set is reachable from X.
-     AARM Rationale: This allows a postcondition to indicate what additional
-     objects might become reachable from X as a result of invoking the
-     subprogram.
 Add the following section:
 6.1.2 The Global and Global'Class Aspects
@@ -216,7 +168,6 @@
       | /package_/name [ PRIVATE ]
       | /access_/subtype_mark
       | ACCESS subtype_mark
-      | /object_/name'Reachable
    A /global_/attribute_reference is an attribute_reference with attribute
    designator "Global."
@@ -323,10 +274,7 @@
        can be designated by values of the given access-to-variable type;
      * ACCESS subtype_mark identifies the set of (aliased) variables that
        can be designated by values of an access-to-variable type with a
-       designated subtype statically matching the given subtype_mark;
-     * /object_/name'Reachable identifies the set of (aliased) variables
-       that are reachable (see 6.1.1) from the object denoted by
-       /object_/name.
+       designated subtype statically matching the given subtype_mark.
     Legality Rules
@@ -399,8 +347,7 @@
 static analysis.
 The intent is that all of the global in, in-out, and out annotations
-proposed can be statically checked. Those involving 'Reachable need further
-explanation -- see below for our discussion of 'Reachable.
+proposed can be statically checked.
 We have allowed for an implementation-defined global_mode_qualifier, which
 would allow "proof in" for SPARK, as well as something like "synthesized
@@ -415,20 +362,6 @@
 check, but thankfully is covered by B.1(38.1/2). Incorrect annotations
 on imported subprograms could cause a program's execution to be erroneous.
-We have defined a 'Reachable attribute which can be used in the presence
-of access types, either visibly or hidden within a private type, to
-indicate side-effects on directly or indirectly designated (aliased) objects.
-A corresponding attribute function 'Reachable(obj1, obj2, ...) can be used
-in postconditions to specify how the set of reachable objects is affected
-by a subprogram.
-To check the uses of X'Reachable within global aspect specifications, the
-compiler needs to verify that, for dereferences that are *not* covered by
-global_name's of the form "access T" or the name of an access type, they
-fall within some X'Reachable set.  In the absence of pointer "ownership"
-(see AI12-0240), X'Reachable is defined in terms of what access *types*
-are "reachable" from X, so it should be checkable at compile time.
 SPARK does not currently support identifying particular components of a
 global variable in the Global aspect, but for Ada we plan to allow that.
 This is somewhat inconsistent with what can be specified for parameters,
@@ -478,8 +411,7 @@
         with Global => T'Global;
       procedure Insert(S : in out Set; X : T)
-        with Global => in out S'Reachable & Hash'Global & T'Global,
-             Post   => S'Reachable(X'Copy'Reachable);
+        with Global => in out Hash'Global & T'Global;
    end Sets;
@@ -489,12 +421,6 @@
 Hash, and as a result of dereferencing access objects within the
 representation of a Set. The default initialization, adjustment, and
 finalization of a Set indirectly uses the corresponding operations of T.
-Insert updates the objects reachable from S, as well as those updated
-by Hash and T's assignment operation, and has a post-condition that
-indicates it makes the objects reachable from X'Copy reachable from S
-(in addition to those originally reachable from S).  X'Copy is used here
-to indicate that we are not using X directly, but rather copying X
-into the data structure that represents S.

Questions? Ask the ACAA Technical Agent