CVS difference for 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