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

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

--- ai12s/ai12-0112-1.txt	2019/04/12 06:09:23	1.18
+++ ai12s/ai12-0112-1.txt	2019/05/08 02:02:02	1.19
@@ -1,4 +1,4 @@
-!standard A.18.2(99/3)                                19-01-21    AI12-0112-1/07
+!standard A.18.2(99/3)                                19-04-15    AI12-0112-1/08
 !standard 11.4.2(23.1/3)
 !standard 11.5(23)
 !standard 11.5(26)
@@ -84,10 +84,10 @@
       return Boolean is <>;
 package Ada.Containers.Vectors
    with Preelaborate, Remote_Types,
-        Nonblocking => Equal_Element'Nonblocking,
-        Global => Equal_Element'Global &
-                  Element_Type'Global &
-                  in out synchronized Ada.Containers.Vectors is
+        Nonblocking => Element_Type'Nonblocking and
+                       Equal_Element'Nonblocking,
+        Global => synchronized in out Ada.Containers.Vectors &
+                  Element_Type'Global & Equal_Element'Global is
 
 [These are the default Nonblocking and Global settings; they're used unless
 otherwise specified. Note that these depend on the formal parameters of the
@@ -137,7 +137,7 @@
 Revised package Ada.Containers.Vectors, paragraphs A.18.2(97.2/3)
 through A.18.2(237):
 
-97.2/3
+97.2/3+
 function Has_Element (Position : Cursor) return Boolean
    with Nonblocking, Global => in access Vector;
 [We have to assume this looks at the container object.]
@@ -287,7 +287,9 @@
 114/2+
 procedure Reserve_Capacity (Container : in out Vector;
                             Capacity  : in     Count_Type)
-   with Post => Container.Capacity >= Capacity;
+   with Pre  => (if Tampering_With_Elements_Prohibited (Container)
+                 then raise Program_Error),
+        Post => Container.Capacity >= Capacity;
 115/3
 If the capacity of Container is already greater than or equal to Capacity, then
 Reserve_Capacity has no effect. Otherwise, Reserve_Capacity allocates additional
@@ -321,7 +323,7 @@
 120/2+
 function Is_Empty (Container : Vector) return Boolean
    with Nonblocking, Global => null,
-        Post => Is_Empty'Result = Length (Container) = 0;
+        Post => Is_Empty'Result = (Length (Container) = 0);
 121/2+
 Returns True if Container is empty.
 
@@ -389,7 +391,7 @@
 function Element (Position  : Cursor) return Element_Type
    with Pre  => (if Position = No_Element then raise Constraint_Error),
         Nonblocking => True,
-        Global => Element_Type'Global & in access Vector;
+        Global => in access Vector & Element_Type'Global;
 131/2+
 Element returns the element designated by Position.
 
@@ -444,7 +446,7 @@
    Index     : in Index_Type;
    Process   : not null access procedure (Element : in Element_Type))
    with Pre  => (if Index not in First_Index (Container) .. Last_Index (Container)
-                 then raise Constraint_Error).
+                 then raise Constraint_Error),
         Global => Element_Type'Global;
 
 [Tampering ought to be indicated for the access procedure here, but we don't
@@ -459,8 +461,8 @@
 procedure Query_Element
   (Position : in Cursor;
    Process  : not null access procedure (Element : in Element_Type))
-   with Pre  => (if Position = No_Element then raise Constraint_Error);
-        Global => Element_Type'Global & in access Vector; 
+   with Pre  => (if Position = No_Element then raise Constraint_Error),
+        Global => in access Vector & Element_Type'Global; 
 139/3+
 Query_Element calls Process.all with the element designated by Position as the
 argument. Tampering with the elements of the vector that contains the element
@@ -472,8 +474,9 @@
   (Container : in Vector;
    Position  : in Cursor;
    Process   : not null access procedure (Element : in Element_Type))
-   with Pre  => (if Position = No_Element then raise Constraint_Error) or else
-                (not Has_Element (Container, Position) then raise Program_Error)
+   with Pre  => (if Position = No_Element then raise Constraint_Error
+                 elsif not Has_Element (Container, Position) 
+                 then raise Program_Error),
         Global => Element_Type'Global;
 
 New
@@ -631,7 +634,7 @@
 procedure Assign (Target : in out Vector; Source : in Vector)
    with Pre  => (if Tampering_With_Cursors_Prohibited (Target)
                  then raise Program_Error),
-        Post => Length (Source) = Length (Target),
+        Post => Length (Source) = Length (Target) and then
                 Capacity (Target) >= Length (Target);
 147.20/3
 If Target denotes the same object as Source, the operation has no effect. If the
@@ -708,7 +711,7 @@
                  then raise Program_Error) and then
                 (if Length (Container) > Maximum_Length - Length (New_Item)
                  then raise Constraint_Error),
-        Post => Length (Container)'Old + Length (New_Item) = Length (Container),
+        Post => Length (Container)'Old + Length (New_Item) = Length (Container) and then
                 Capacity (Container) >= Length (Container);
 154/3+
 If Length (New_Item) is 0, then Insert does nothing. If Before is No_Element,
@@ -820,7 +823,7 @@
                  then raise Program_Error) and then
                 (if Before /= No_Element and then 
                     (not Has_Element (Container, Before))
-                 then raise Program_Error) and
+                 then raise Program_Error) and then
                 (if Length (Container) > Maximum_Length - Count
                  then raise Constraint_Error),
         Post => Length (Container)'Old + Count = Length (Container) and then
@@ -899,11 +902,11 @@
                         Before    : in     Extended_Index;
                         Count     : in     Count_Type := 1);
    with Pre  => (if Tampering_With_Cursors_Prohibited (Container)
-                 then raise Program_Error) and then
-                (if Before not in First_Index (Container) .. Last_Index (Container) + 1
-                 then raise Constraint_Error),
-                (if Length (Container) > Maximum_Length - Count
-                 then raise Constraint_Error),
+                    then raise Program_Error
+                 elsif Before not in First_Index (Container) .. Last_Index (Container) + 1
+                    then raise Constraint_Error
+                 elsif Length (Container) > Maximum_Length - Count
+                    then raise Constraint_Error),
         Post => Length (Container)'Old + Count = Length (Container) and then
                 Capacity (Container) >= Length (Container);
 177/3+
@@ -921,12 +924,12 @@
                         Position  :    out Cursor;
                         Count     : in     Count_Type := 1)
    with Pre  => (if Tampering_With_Cursors_Prohibited (Container)
-                 then raise Program_Error) and then
-                (if Before /= No_Element and then 
+                    then raise Program_Error) and then
+                 elsif Before /= No_Element and then 
                     (not Has_Element (Container, Before))
-                 then raise Program_Error) and then
-                (if Length (Container) > Maximum_Length - Count
-                 then raise Constraint_Error),
+                    then raise Program_Error) and then
+                 elsif Length (Container) > Maximum_Length - Count
+                    then raise Constraint_Error),
         Post => Length (Container)'Old + Count = Length (Container) and then
                 Has_Element (Container, Position) and then
                 Capacity (Container) >= Length (Container);
@@ -940,9 +943,9 @@
                   Index     : in     Extended_Index;
                   Count     : in     Count_Type := 1)
    with Pre  => (if Tampering_With_Cursors_Prohibited (Container)
-                 then raise Program_Error) and then
+                 then raise Program_Error and then
                 (if Index not in First_Index (Container) .. Last_Index (Container) + 1
-                 then raise Constraint_Error) and then
+                 then raise Constraint_Error and then
                 (if Length (Container) + Count > Maximum_Length
                  then raise Constraint_Error),
         Post => Length (Container)'Old - Count <= Length (Container);
@@ -1007,7 +1010,7 @@
 
 193/2+
 procedure Swap (Container : in out Vector;
-                I, J      : in     Cursor);
+                I, J      : in     Cursor)
    with Pre  => (if Tampering_With_Elements_Prohibited (Container)
                  then raise Program_Error) and then
                 (if I = No_Element or else J = No_Element
@@ -1020,48 +1023,45 @@
 Swap exchanges the values of the elements designated by I and J.
 
 195/2
-function First_Index (Container : Vector) return Index_Type is
-   with Nonblocking => True,
-        Global => null,
+function First_Index (Container : Vector) return Index_Type
+   with Nonblocking, Global => null,
         Post => First_Index'Result = Index_Type'First;
 196/2
 Returns the value Index_Type'First.
 
 197/2+
 function First (Container : Vector) return Cursor
-    with Post => (if not Is_Empty (Container)
+    with Nonblocking, Global => null,
+         Post => (if not Is_Empty (Container)
                   then Has_Element (Container, First'Result)
                   else First'Result = No_Element),
-         Global => null,
-         Nonblocking => True;
 
 198/2
 If Container is empty, First returns No_Element. Otherwise, it returns a cursor
 that designates the first element in Container.
 
-199/2
+199/2+
 function First_Element (Container : Vector) return Element_Type is
     with Pre => (if Is_Empty (Container) then raise Constraint_Error);
 200/2
 Equivalent to Element (Container, First_Index (Container)).
 
-201/2
+201/2+
 function Last_Index (Container : Vector) return Extended_Index
-   with Nonblocking => True,
-        Global => null,
+   with Nonblocking, Global => null,
         Post => (if Length (Container) = 0 then Last_Index'Result = No_Index
-                 else Last_Index'Result = Length (Container) - 1 + Index_Type'First);
+                 else Count_Type(Last_Index'Result - Index_Type'First) = 
+                      Length (Container) - 1);
 202/2
 If Container is empty, Last_Index returns No_Index. Otherwise, it returns the
 position of the last element in Container.
 
 203/2+
 function Last (Container : Vector) return Cursor;
-    with Post => (if not Is_Empty (Container)
+    with Nonblocking, Global => null,
+         Post => (if not Is_Empty (Container)
                   then Has_Element (Container, Last'Result)
-                  else Last'Result = No_Element),
-         Global => null,
-         Nonblocking => True;
+                  else Last'Result = No_Element);
 204/2
 If Container is empty, Last returns No_Element. Otherwise, it returns a cursor
 that designates the last element in Container.
@@ -1074,7 +1074,7 @@
 
 207/2+
 function Next (Position : Cursor) return Cursor
-   with Global => Vectors'Global & in access Vector,
+   with Global => in access Vector,
         Nonblocking => True,
         Post => (if Position = No_Element then Next'Result = No_Element
                  else True);
@@ -1086,42 +1086,42 @@
 
 New
 function Next (Container : Vector; Position : Cursor) return Cursor
-   with Pre  => (if Position /= No_Element and then 
+   with Nonblocking, Global => null,
+        Pre  => (if Position /= No_Element and then 
                     (not Has_Element (Container, Position))
                  then raise Program_Error),
         Post => (if Position = No_Element then Next'Result = No_Element
-                 elsif Has_Element (Container, Next'Result) then True
+                 elsif Has_Element (Container, Next'Result) then
+                    To_Index (Container, Next'Result) = 
+                    To_Index (Container, Position) + 1
                  elsif Next'Result = No_Element then
-                      Position = Last (Container)
-                 else To_Index (Container, Next'Result) = 
-                      To_Index (Container, Position) + 1),
-        Global => null,
-        Nonblocking => True;
+                    Position = Last (Container)
+                 else False);
 New
-Returns a cursor designating the next element in the Container, if any.
+Returns a cursor designating the next element in Container, if any.
 
 209/2+
 procedure Next (Position : in out Cursor)
-   with Global => Vectors'Global & in access Vector,
+   with Global => in access Vector,
         Nonblocking => True;
 210/2
 Equivalent to Position := Next (Position).
 
 New
-procedure Next (Container : Vector; Position : in out Cursor)
-   with Pre  => (if Position /= No_Element and then 
+procedure Next (Container : in     Vector;
+                Position  : in out Cursor)
+   with Nonblocking, Global => null,
+        Pre  => (if Position /= No_Element and then 
                     (not Has_Element (Container, Position))
                  then raise Program_Error),
         Post => (if Position /= No_Element
-                 then Has_Element (Container, Position)),
-        Global => null,
-        Nonblocking => True;
+                 then Has_Element (Container, Position));
 New
-Equivalent to Position := Next (Position).
+Equivalent to Position := Next (Container, Position).
 
 211/2+
 function Previous (Position : Cursor) return Cursor
-   with Global => Vectors'Global & in access Vector,
+   with Global => in access Vector,
         Nonblocking => True,
         Post => (if Position = No_Element then Previous'Result = No_Element
                  else True);
@@ -1132,39 +1132,40 @@
 Position.
 
 New
-function Previous (Container : Vector; Position : Cursor) return Cursor
-   with Pre  => (if Position /= No_Element and then 
+function Previous (Container : Vector; 
+                   Position  : Cursor) return Cursor
+   with Nonblocking, Global => null,
+        Pre  => (if Position /= No_Element and then 
                     (not Has_Element (Container, Position))
                  then raise Program_Error),
         Post => (if Position = No_Element then Previous'Result = No_Element
-                 elsif Has_Element (Container, Previous'Result) then True
-                 elsif Next'Result = No_Element then
-                      Position = First (Container)
-                 else To_Index (Container, Next'Result) = 
-                      To_Index (Container, Position) - 1),
-        Global => null,
-        Nonblocking => True;
+                 elsif Has_Element (Container, Previous'Result) then 
+                    To_Index (Container, Next'Result) = 
+                    To_Index (Container, Position) - 1  
+                 elsif Previous'Result = No_Element then
+                     Position = First (Container)
+                 else False);
 New
-Returns a cursor designating the previous element in the Container, if any.
+Returns a cursor designating the previous element in Container, if any.
 
 213/2+
 procedure Previous (Position : in out Cursor)
-   with Global => Vectors'Global & in access Vector,
+   with Global => in access Vector,
         Nonblocking => True;
 214/2
 Equivalent to Position := Previous (Position).
 
 New
-procedure Previous (Container : Vector; Position : in out Cursor)
-   with Pre  => (if Position /= No_Element and then 
+procedure Previous (Container : in     Vector; 
+                    Position  : in out Cursor)
+   with Nonblocking, Global => null,
+        Pre  => (if Position /= No_Element and then 
                     (not Has_Element (Container, Position))
                  then raise Program_Error),
         Post => (if Position /= No_Element
-                 then Has_Element (Container, Position)),
-        Global => null,
-        Nonblocking => True;
+                 then Has_Element (Container, Position));
 New
-Equivalent to Position := Previous (Position).
+Equivalent to Position := Previous (Container, Position).
 
 215/2
 function Find_Index (Container : Vector;
@@ -1183,11 +1184,11 @@
                Item      : Element_Type;
                Position  : Cursor := No_Element)
    return Cursor
-    with Pre  => (if Position /= No_Element and then 
-                    (not Has_Element (Container, Position))
-                  then raise Program_Error),
-    with Post => (if Find'Result = No_Element then True
-                  else Has_Element (Container, Find'Result));
+   with Pre  => (if Position /= No_Element and then 
+                   (not Has_Element (Container, Position))
+                 then raise Program_Error),
+        Post => (if Find'Result = No_Element then True
+                 else Has_Element (Container, Find'Result));
 218/3+
 Find searches the elements of
 Container for an element equal to Item (using the generic formal equality
@@ -1215,11 +1216,11 @@
                        Item      : Element_Type;
                        Position  : Cursor := No_Element)
    return Cursor
-    with Pre  => (if Position /= No_Element and then 
-                    (not Has_Element (Container, Position))
-                  then raise Program_Error),
-    with Post => (if Reverse_Find'Result = No_Element then True
-                  else Has_Element (Container, Reverse_Find'Result));
+   with Pre  => (if Position /= No_Element and then 
+                   (not Has_Element (Container, Position))
+                 then raise Program_Error),
+        Post => (if Reverse_Find'Result = No_Element then True
+                 else Has_Element (Container, Reverse_Find'Result));
 222/3+
 Reverse_Find searches the elements
 of Container for an element equal to Item (using the generic formal equality
@@ -1247,7 +1248,7 @@
 execution of a call on Process.all. Any exception raised by Process.all is
 propagated.
 
-229/2
+229/2+
 procedure Reverse_Iterate
   (Container : in Vector;
    Process   : not null access procedure (Position : in Cursor))
@@ -1257,7 +1258,7 @@
 Iterates over the elements in Container as per procedure Iterate, except that
 elements are traversed in reverse index order.
 
-230.1/3
+230.1/3+
 function Iterate (Container : in Vector)
    return Vector_Iterator_Interfaces.Reversible_Iterator'Class
    with Post   => Tampering_With_Cursors_Prohibited (Container);
@@ -1275,9 +1276,9 @@
 
 230.3/3+
 function Iterate (Container : in Vector; Start : in Cursor)
-   return Vector_Iterator_Interfaces.Reversible_Iterator'Class;
+   return Vector_Iterator_Interfaces.Reversible_Iterator'Class
    with Pre    => (if Start = No_Element then raise Constraint_Error) and then
-                  (if not Has_Element (Start, Position) then raise Program_Error),
+                  (if not Has_Element (Container, Start) then raise Program_Error),
         Post   => Tampering_With_Cursors_Prohibited (Container);
 230.4/3+
 Iterate returns a reversible iterator object (see 5.5.1)
@@ -1318,20 +1319,23 @@
 236/2+
 procedure Merge (Target  : in out Vector;
                  Source  : in out Vector)
-   with Pre  => (if Tampering_With_Elements_Prohibited (Target)
+   with Pre  => (if Tampering_With_Cursors_Prohibited (Target)
                  then raise Program_Error) and then
-                (if Tampering_With_Elements_Prohibited (Source)
+                (if Tampering_With_Cursors_Prohibited (Source)
                  then raise Program_Error) and then
                 (if Length (Target) > Maximum_Length - Length (Source)
                  then raise Constraint_Error),
-        Post => (if Target = Source then True
-                 else Length (Source) = 0 and then
-                 Length (Target) =
-                 Length (Source)'Old + Length (Target)'Old and then
-                 Capacity (Target) >=
-                     Length (Source)'Old + Length (Target)'Old;
+        Post => (declare
+                   Result_Length : constant Count_Type :=
+                      Length (Source)'Old + Length (Target)'Old;
+                 begin
+                    (if Target = Source then True
+                     else Length (Source) = 0 and then
+                        Length (Target) = Result_Length and then
+                        Capacity (Target) >= Result_Length));
+
 [Checking whether these are sorted is too expensive, so we won't try;
-especially as we don't specify what happens if they're not.]
+especially as we don't specify what happens if they're not sorted on input.]
 237/3
 If Source is empty, then Merge does nothing. If Source and Target are the same
 nonempty container object, then Program_Error is propagated. Otherwise, Merge
@@ -1432,9 +1436,8 @@
 package Ada.Containers.Indefinite_Holders
    with Preelaborate, Remote_Types,
         Nonblocking => Equal_Element'Nonblocking,
-        Global => Equal_Element'Global &
-                  Element_Type'Global &
-                  in out synchronized Ada.Containers.Indefinite_Holders is
+        Global => synchronized in out Ada.Containers.Indefinite_Holders &
+                  Equal_Element'Global & Element_Type'Global is
 
 6/3+
    type Holder is tagged private
@@ -1970,6 +1973,16 @@
            Post =@> Length (Container)'Old + 1 = Length (Container) @b<and then>
                    Capacity (Container) @>= Length (Container);>
 
+!corrigendum A.18.2(74.1/3)
+
+@drepl
+@xcode<   @b<function> Iterate (Container : @b<in> Vector)
+      @b<return> Vector_Iterator_Interfaces.Reversible_Iterator'Class;>
+@dby
+@xcode<   @b<function> Iterate (Container : @b<in> Vector)
+      @b<return> Vector_Iterator_Interfaces.Parallel_Reversible_Iterator'Class
+      @b<with> Post   =@> Tampering_With_Cursors_Prohibited (Container);>
+
 !corrigendum A.18.2(125/2)
 
 @drepl
@@ -2036,7 +2049,16 @@
 
 @xindent<Equivalent to Insert (Container, Last_Index (Container) + 1, New_Item, 1).>
 
+!corrigendum A.18.2(230.1/3)
 
+@drepl
+@xcode<@b<function> Iterate (Container : @b<in> Vector)
+   @b<return> Vector_Iterator_Interfaces.Reversible_Iterator'Class;>
+@dby
+@xcode<@b<function> Iterate (Container : @b<in> Vector)
+   @b<return> Vector_Iterator_Interfaces.Parallel_Reversible_Iterator'Class
+   @b<with> Post   =@> Tampering_With_Cursors_Prohibited (Container);>
+
 
 !corrigendum A.18.3(6/3)
 
@@ -2049,6 +2071,54 @@
    @b<pragma> Preelaborable_Initialization(List);>
 @dby
 See the conflict file!!
+
+!corrigendum A.18.3(46.1/3)
+
+@drepl
+@xcode<   @b<function> Iterate (Container : @b<in> List)
+      @b<return> List_Iterator_Interfaces.Reversible_Iterator'Class;>
+@dby
+@xcode<   @b<function> Iterate (Container : @b<in> List)
+      @b<return> List_Iterator_Interfaces.Parallel_Reversible_Iterator'Class
+      @b<with> Post   =@> Tampering_With_Cursors_Prohibited (Container);>
+
+
+!corrigendum A.18.3(81/3)
+
+@drepl
+@xindent<If Position equals No_Element, then Constraint_Error is propagated;
+if Position does not designate an element in Container, then Program_Error is
+propagated. Otherwise, Replace_Element assigns the value New_Item to the
+element designated by Position.>
+@dby
+@xindent<Replace_Element assigns the value New_Item to the
+element designated by Position. For the purposes of determining whether the
+parameters overlap in a call to Replace_Element, the Container parameter is
+not considered to overlap with any object (including itself).>
+
+!corrigendum A.18.3(144.1/3)
+
+@drepl
+@xcode<@b<function> Iterate (Container : @b<in> List)
+   @b<return> List_Iterator_Interfaces.Reversible_Iterator'Class;>
+@dby
+@xcode<@b<function> Iterate (Container : @b<in> List)
+   @b<return> List_Iterator_Interfaces.Parallel_Reversible_Iterator'Class
+   @b<with> Post   =@> Tampering_With_Cursors_Prohibited (Container);>
+
+
+!corrigendum A.18.4(36/3)
+
+@drepl
+@xindent<If Position equals No_Element, then Constraint_Error is propagated;
+if Position does not designate an element in Container, then Program_Error
+is propagated. Otherwise, Replace_Element assigns New_Item to the element of
+the node designated by Position.>
+@dby
+@xindent<Replace_Element assigns New_Item to the element of
+the node designated by Position. For the purposes of determining whether the
+parameters overlap in a call to Replace_Element, the Container parameter is
+not considered to overlap with any object (including itself).>
 
 
 !corrigendum A.18.5(3/2)

Questions? Ask the ACAA Technical Agent