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

Differences between 1.15 and version 1.16
Log of other versions for file ai12s/ai12-0112-1.txt

--- ai12s/ai12-0112-1.txt	2019/02/21 05:29:33	1.15
+++ ai12s/ai12-0112-1.txt	2019/04/06 05:08:49	1.16
@@ -3,6 +3,7 @@
 !standard 11.5(23)
 !standard 11.5(26)
 !standard A(4)
+!standard A.18(10)
 !class Amendment 14-05-15
 !status Amendment 1-2012 18-12-10
 !status ARG Approved 9-0-2  18-12-10
@@ -138,16 +139,14 @@
 
 97.2/3
 function Has_Element (Position : Cursor) return Boolean
-   with Nonblocking => True,
-        Global => access Vector;
+   with Nonblocking, Global => in access Vector;
 [We have to assume this looks at the container object.]
 97.3/3
 Returns True if Position designates an element, and returns False otherwise.
 
 New
 function Has_Element (Container : Vector; Position : Cursor) return Boolean
-   with Nonblocking => True,
-        Global => null;
+   with Nonblocking, Global => null;
 New
 Returns True if Position designates an element in Container, and returns False
 otherwise.
@@ -171,8 +170,7 @@
 New
 function Tampering_With_Cursors_Prohibited 
    (Container : Vector) return Boolean
-   with Nonblocking => True,
-        Global => null;
+   with Nonblocking, Global => null;
 New
 Returns True if tampering with cursors or tampering with elements is currently
 prohibited for Container, and returns False otherwise.
@@ -182,8 +180,7 @@
 New
 function Tampering_With_Elements_Prohibited 
    (Container : Vector) return Boolean
-   with Nonblocking => True,
-        Global => null;
+   with Nonblocking, Global => null;
 New
 Returns True if tampering with elements is currently prohibited for Container,
 and returns False otherwise.
@@ -281,14 +278,13 @@
 111/2
 Returns a vector comprising the element Left followed by the element Right.
 
-112/2
+112/2+
 function Capacity (Container : Vector) return Count_Type
-   with Nonblocking => True,
-        Global => null;
+   with Nonblocking, Global => null;
 113/2
 Returns the capacity of Container.
 
-114/2
+114/2+
 procedure Reserve_Capacity (Container : in out Vector;
                             Capacity  : in     Count_Type)
    with Post => Container.Capacity >= Capacity;
@@ -302,10 +298,9 @@
 deallocates any storage no longer needed. Any exception raised during allocation
 is propagated and Container is not modified.
 
-116/2
+116/2+
 function Length (Container : Vector) return Count_Type
-   with Nonblocking => True,
-        Global => null;
+   with Nonblocking, Global => null;
 117/2
 Returns the number of elements in Container.
 
@@ -323,12 +318,12 @@
 Length. If Length is greater than the original length of Container, empty
 elements are added to Container; otherwise, elements are removed from Container.
 
-120/2
+120/2+
 function Is_Empty (Container : Vector) return Boolean
-   with Nonblocking => True,
-        Global => null;
-121/2
-Equivalent to Length (Container) = 0.
+   with Nonblocking, Global => null,
+        Post => Is_Empty'Result = Length (Container) = 0;
+121/2+
+Returns True if Container is empty.
 
 122/2+
 procedure Clear (Container : in out Vector)
@@ -345,7 +340,7 @@
    with Post => (if Index in First_Index (Container) .. Last_Index (Container)
                  then Has_Element (Container, To_Cursor'Result)
                  else To_Cursor'Result = No_Element),
-        Nonblocking => True;
+        Nonblocking, Global => null;
 125/2
 If Index is not in the range First_Index (Container) .. Last_Index (Container),
 then No_Element is returned. Otherwise, a cursor designating the element at
@@ -355,8 +350,7 @@
 
 126/2
 function To_Index (Position  : Cursor) return Extended_Index
-   with Global => Vectors'Global & in access Vector,
-        Nonblocking => True;
+   with Nonblocking, Global => in access Vector;
 
 [Note: No postcondition here, since we can't name the container. See below.]
 127/2
@@ -371,7 +365,7 @@
         Post => (if Position = No_Element then To_Index'Result = No_Index
                  else To_Index'Result in First_Index (Container) ..
                         Last_Index (Container)),
-        Nonblocking => True;
+        Nonblocking, Global => null;
 New
 If Position is No_Element, No_Index is returned. Otherwise, the index (within
 its containing vector) of the element designated by Position is returned.
@@ -382,8 +376,7 @@
    return Element_Type
    with Pre  => (if Index not in First_Index (Container) .. Last_Index (Container)
                        then raise Constraint_Error),
-        Nonblocking => True,
-        Global => Element_Type'Global;
+        Nonblocking, Global => Element_Type'Global;
 
 129/2+
 Element returns the element at position Index.
@@ -401,8 +394,7 @@
    with Pre => (if Position = No_Element then raise Constraint_Error) and then
                (if not Has_Element (Container, Position)
                 then raise Program_Error),
-        Nonblocking => True,
-        Global => Element_Type'Global;
+        Nonblocking, Global => Element_Type'Global;
 New
 Element returns the element designated by Position.
 
@@ -531,12 +523,14 @@
 type Constant_Reference_Type
       (Element : not null access constant Element_Type) is private
    with Implicit_Dereference => Element,
-        Global => in out access Vector,
+        Global => (in access Vector, synchronized out access Vector),
+        Nonblocking => True,
         Default_Initial_Condition => (raise Program_Error);
 147.2/3
 type Reference_Type (Element : not null access Element_Type) is private
    with Implicit_Dereference => Element,
-        Global => in out access Vector,
+        Global => synchronized in out access Vector,
+        Nonblocking => True,
         Default_Initial_Condition => (raise Program_Error);
 147.3/3
 The types Constant_Reference_Type and Reference_Type need finalization.
@@ -1347,15 +1341,24 @@
 A.18.11 The Generic Package Containers.Indefinite_Vectors
 
 Add after A.18.11(9/4):
+
+The description of Tampering_With_Elements_Prohibited is replaced by:
 
-Tampering_With_Cursors_Prohibited is replaced by
-Tampering_With_Elements_Prohibited in the postcondition for the operations
+   Returns True if tampering with elements is prohibited for Container, and 
+   False otherwise.
+
+Tampering_With_Cursors_Prohibited is replaced by 
+Tampering_With_Elements_Prohibited in the postcondition for the operations 
 Reference and Constant_Reference.
 
 -----------------------------------------
 
 A.18.19 The Generic Package Containers.Bounded_Vectors
 
+Modify A.18.19(2/3):
+
+* The {aspect}[pragma] Preelaborate is replaced with {aspect}[pragma] Pure.
+
 Add after A.18.19(3/3):
 
 * The Global aspect of the package is replaced by 
@@ -1683,10 +1686,19 @@
 
 Add after A.18(11/5):
 
-If an instance of an Ada.Containers generic package is nonblocking, then the 
-specific type of the object returned from a function that returns an object 
-of an iterator interface, as well as the primitive operations of that specific 
-type, shall be nonblocking.
+For an instance I of a container package with a container type C, the
+specific type T of the object returned from a function that returns an object 
+of an iterator interface, as well as the primitive operations of T, shall 
+be nonblocking. The Global aspect specified for T and the primitive operations 
+of T shall be (in access C, synchronized out access C) or a specification
+that allows accesses fewer global objects.
+
+AARM Implementation Note: This requires that the traversal and iteration 
+operations of a container do not create, destroy, or assign any objects of 
+a formal type of I, nor call any formal subprograms of I. Those objects and
+subprograms might be blocking or write globals (depending on the actual 
+parameters). We put similar requirements on the individual traversal 
+operations in the container package definitions.
 
 
 !discussion
@@ -1897,7 +1909,7 @@
 specification of @b<null>.
 
 
-!corrigendum A.18(11/5)
+!corrigendum A.18(10)
 
 @dinsa
 For an indefinite container (one whose type is defined in an instance of a
@@ -1913,10 +1925,12 @@
 finalized. For other kinds of containers, when elements are created
 and finalized is unspecified.
 @dinst
-If an instance of an Ada.Containers generic package is nonblocking, then the 
-specific type of the object returned from a function that returns an object 
-of an iterator interface, as well as the primitive operations of that specific 
-type, shall be nonblocking.
+For an instance @i<I> of a container package with a container type @i<C>, the
+specific type @i<T> of the object returned from a function that returns an 
+object of an iterator interface, as well as the primitive operations of @i<T>, 
+shall be nonblocking. The Global aspect specified for @i<T> and the primitive 
+operations of @i<T> shall be @fc<(@b<in access> @i<C>, @b<synchronized out 
+access> @i<C>)> or a specification that allows access to fewer global objects.
 
 !comment For the actual container's definitions (A.18.2-A.18.36), we only 
 !comment provide Corrigendum sections for those that conflict with other

Questions? Ask the ACAA Technical Agent