Version 1.3 of ai12s/ai12-0112-1.txt

Unformatted version of ai12s/ai12-0112-1.txt version 1.3
Other versions for file ai12s/ai12-0112-1.txt

!standard A.18.2(99/3)          14-05-15 AI12-0112-1/01
!class Amendment 14-05-15
!status work item 14-05-15
!status received 15-02-11
!priority Medium
!difficulty Hard
!subject Preconditions for container operations
!summary
Most container checks are described with preconditions rather than English, so that the definitions are more formal (and can be processed by tools) and that the text is simpler.
!problem
Many of the subprograms defined by the containers start with a series of checks described in English. These would be better written as preconditions, which would make them available to compilers for optimization and to proof tools, as well as being less ambiguous for human readers.
** Must add some text about the missing reading operations -- see the January 2017 mail in this AI **
!proposal
(See summary.)
!wording
[See the !discussion for general notes before reading this.]
Prototype of revised package Ada.Containers.Vectors, paragraphs A.18.2(97.2/3) through A.18.2(237).
97.2/3 function Has_Element (Position : Cursor) return Boolean; 97.3/3 Returns True if Position designates an element, and returns False otherwise.
98/2 function "=" (Left, Right : Vector) return Boolean; 99/3 If Left and Right denote the same vector object, then the function returns True. If Left and Right have different lengths, then the function returns False. Otherwise, it compares each element in Left to the corresponding element in Right using the generic formal equality operator. If any such comparison returns False, the function returns False; otherwise, it returns True. Any exception raised during evaluation of element equality is propagated.
New function Cursor_Belongs_To_Container (Container : Vector; Position : Cursor)
return Boolean;
New Returns True if Position designates an element in Container, and returns False otherwise.
New AARM Ramification: If Position is No_Element, Cursor_Belongs_To_Container returns False.
New function Tampering_With_Cursors_Prohibited (Container : Vector) return Boolean; New Returns True if tampering with cursors or tampering with elements is currently prohibited for Container, and returns False otherwise. New AARM Note: Prohibiting tampering with elements also prohibits tampering with cursors, so we have this function reflect that.
New function Tampering_With_Elements_Prohibited (Container : Vector) return Boolean; New Returns True if tampering with elements is currently prohibited for Container, and returns False otherwise.
100/2+ function To_Vector (Length : Count_Type) return Vector
with Post'Class => Length (To_Vector'Result) = Length;
101/2 Returns a vector with a length of Length, filled with empty elements.
102/2+ function To_Vector
(New_Item : Element_Type;
Length : Count_Type) return Vector with Post'Class => Length (To_Vector'Result) = Length;
103/2 Returns a vector with a length of Length, filled with elements initialized to the value New_Item.
104/2+ function "&" (Left, Right : Vector) return Vector
with Post'Class => Length ("&"'Result) = Length (Left) + Length (Right);
105/2 Returns a vector comprising the elements of Left followed by the elements of Right.
106/2+ function "&" (Left : Vector;
Right : Element_Type) return Vector
with Post'Class => Length ("&"'Result) = Length (Left) + 1;
107/2 Returns a vector comprising the elements of Left followed by the element Right.
108/2+ function "&" (Left : Element_Type;
Right : Vector) return Vector
with Post'Class => Length ("&"'Result) = Length (Right) + 1;
109/2 Returns a vector comprising the element Left followed by the elements of Right.
110/2+ function "&" (Left, Right : Element_Type) return Vector
with Post'Class => Length ("&"'Result) = 2;
111/2 Returns a vector comprising the element Left followed by the element Right.
112/2 function Capacity (Container : Vector) return Count_Type; 113/2 Returns the capacity of Container.
114/2 procedure Reserve_Capacity (Container : in out Vector;
Capacity : in Count_Type);
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 storage as necessary to ensure that the length of the resulting vector can become at least the value Capacity without requiring an additional call to Reserve_Capacity, and is large enough to hold the current length of Container. Reserve_Capacity then, as necessary, moves elements into the new storage and deallocates any storage no longer needed. Any exception raised during allocation is propagated and Container is not modified.
116/2 function Length (Container : Vector) return Count_Type; 117/2 Returns the number of elements in Container.
118/2+ procedure Set_Length (Container : in out Vector;
Length : in Count_Type)
with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error),
Post'Class => Length (To_Vector'Result) = Length;
119/3 If Length is larger than the capacity of Container, Set_Length calls Reserve_Capacity (Container, Length), then sets the length of the Container to 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 function Is_Empty (Container : Vector) return Boolean; 121/2 Equivalent to Length (Container) = 0.
122/2+ procedure Clear (Container : in out Vector)
with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error),
Post'Class => Length (Container) = 0;
123/2 Removes all the elements from Container. The capacity of Container does not change.
124/2+ function To_Cursor (Container : Vector;
Index : Extended_Index) return Cursor
with Post'Class => (if Index in First_Index (Container) .. Last_Index (Container)
then Cursor_Belongs_To_Container (Container, To_Cursor'Result) else To_Cursor'Result = No_Element);
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 position Index in Container is returned.
126/2 function To_Index (Position : Cursor) return Extended_Index; 127/2 If Position is No_Element, No_Index is returned. Otherwise, the index (within its containing vector) of the element designated by Position is returned.
128/2+ function Element (Container : Vector;
Index : Index_Type)
return Element_Type with Pre'Class => (if Index not in First_Index (Container) .. Last_Index (Container)
then raise Constraint_Error),
Post'Class => Length (Container)'Old = Length (Container);
129/2+ Element returns the element at position Index.
130/2+ function Element (Position : Cursor) return Element_Type
with Pre'Class => (if Position = No_Element then raise Constraint_Error),
Post'Class => Length (Container)'Old = Length (Container);
131/2+ Element returns the element designated by Position.
132/2+ procedure Replace_Element (Container : in out Vector;
Index : in Index_Type; New_Item : in Element_Type)
with Pre'Class => (if Tampering_With_Elements_Prohibited (Container)
then raise Program_Error) and then
(if Index not in First_Index (Container) .. Last_Index (Container)
then raise Constraint_Error),
Post'Class => Length (Container)'Old = Length (Container);
133/3+ Replace_Element assigns the value New_Item to the element at position Index. Any exception raised during the assignment is propagated. The element at position Index is not an empty element after successful call to Replace_Element.
134/2+ procedure Replace_Element (Container : in out Vector;
Position : in Cursor; New_Item : in Element_Type);
with Pre'Class => (if Tampering_With_Elements_Prohibited (Container)
then raise Program_Error) and then
(if Position = No_Element then raise Constraint_Error) and then (if not Cursor_Belongs_To_Container (Container, Position)
then raise Program_Error),
Post'Class => Length (Container)'Old = Length (Container);
135/3+ Replace_Element assigns New_Item to the element designated by Position. Any exception raised during the assignment is propagated. The element at Position is not an empty element after successful call to Replace_Element.
136/2+ procedure Query_Element
(Container : in Vector;
Index : in Index_Type; Process : not null access procedure (Element : in Element_Type)) with Pre'Class => (if Index not in First_Index (Container) .. Last_Index (Container) then raise Constraint_Error), Post'Class => Length (Container)'Old = Length (Container);
137/3+ Query_Element calls Process.all with the element at position Index as the argument. Tampering with the elements of Container is prohibited during the execution of the call on Process.all. Any exception raised by Process.all is propagated.
138/2+ procedure Query_Element
(Position : in Cursor;
Process : not null access procedure (Element : in Element_Type)) with Pre'Class => (if Position = No_Element then raise Constraint_Error), Post'Class => Length (Container)'Old = Length (Container);
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 designated by Position is prohibited during the execution of the call on Process.all. Any exception raised by Process.all is propagated.
140/2+ procedure Update_Element
(Container : in out Vector;
Index : in Index_Type; Process : not null access procedure (Element : in out Element_Type)) with Pre'Class => (if Index not in First_Index (Container) .. Last_Index (Container) then raise Constraint_Error), Post'Class => Length (Container)'Old = Length (Container);
[Editor's note: Yes, Update_Element does not tamper with elements, because it cannot replace the memory of the element. There is AARM note: A.18.2(97.a/2). When Process is called, it prohibits tampering with elements; I don't know of any way with the current aspects to show that.] 141/3+ Update_Element calls Process.all with the element at position Index as the argument. Tampering with the elements of Container is prohibited during the execution of the call on Process.all. Any exception raised by Process.all is propagated. 142/2 If Element_Type is unconstrained and definite, then the actual Element parameter of Process.all shall be unconstrained. 143/2 The element at position Index is not an empty element after successful completion of this operation.
144/2+ procedure Update_Element
(Container : in out Vector;
Position : in Cursor; Process : not null access procedure (Element : in out Element_Type)) with Pre'Class => (if Position = No_Element then raise Constraint_Error) and then (if not Cursor_Belongs_To_Container (Container, Position) then raise Program_Error), Post'Class => Length (Container)'Old = Length (Container);
145/3 Update_Element calls Process.all with the element designated by Position as the argument. Tampering with the elements of Container is prohibited during the execution of the call on Process.all. Any exception raised by Process.all is propagated. 146/2 If Element_Type is unconstrained and definite, then the actual Element parameter of Process.all shall be unconstrained. 147/2 The element designated by Position is not an empty element after successful completion of this operation.
147.1/3 type Constant_Reference_Type
(Element : not null access constant Element_Type) is private with Implicit_Dereference => Element;
147.2/3 type Reference_Type (Element : not null access Element_Type) is private
with Implicit_Dereference => Element;
147.3/3 The types Constant_Reference_Type and Reference_Type need finalization. 147.4/3 The default initialization of an object of type Constant_Reference_Type or Reference_Type propagates Program_Error.
147.5/3+ function Constant_Reference (Container : aliased in Vector;
Index : in Index_Type)
return Constant_Reference_Type with Pre'Class => (if Index not in First_Index (Container) .. Last_Index (Container)
then raise Constraint_Error),
Post'Class => Length (Container)'Old = Length (Container);
147.6/3 This function (combined with the Constant_Indexing and Implicit_Dereference aspects) provides a convenient way to gain read access to an individual element of a vector given an index value. 147.7/3+ Constant_Reference returns an object whose discriminant is an access value that designates the element at position Index. Tampering with the elements of Container is prohibited while the object returned by Constant_Reference exists and has not been finalized.
147.8/3+ function Reference (Container : aliased in out Vector;
Index : in Index_Type)
return Reference_Type with Pre'Class => (if Index not in First_Index (Container) .. Last_Index (Container)
then raise Constraint_Error),
Post'Class => Length (Container)'Old = Length (Container);
147.9/3 This function (combined with the Variable_Indexing and Implicit_Dereference aspects) provides a convenient way to gain read and write access to an individual element of a vector given an index value. 147.10/3+ Reference returns an object whose discriminant is an access value that designates the element at position Index. Tampering with the elements of Container is prohibited while the object returned by Reference exists and has not been finalized. 147.11/3 The element at position Index is not an empty element after successful completion of this operation.
147.12/3+ function Constant_Reference (Container : aliased in Vector;
Position : in Cursor)
return Constant_Reference_Type with Pre'Class => (if Position = No_Element then raise Constraint_Error) and then
(if not Cursor_Belongs_To_Container (Container, Position)
then raise Program_Error),
Post'Class => Length (Container)'Old = Length (Container);
147.13/3 This function (combined with the Constant_Indexing and Implicit_Dereference aspects) provides a convenient way to gain read access to an individual element of a vector given a cursor. 147.14/3+ Constant_Reference returns an object whose discriminant is an access value that designates the element designated by Position. Tampering with the elements of Container is prohibited while the object returned by Constant_Reference exists and has not been finalized.
147.15/3+ function Reference (Container : aliased in out Vector;
Position : in Cursor)
return Reference_Type is with Pre'Class => (if Position = No_Element then raise Constraint_Error) and then
(if not Cursor_Belongs_To_Container (Container, Position)
then raise Program_Error),
Post'Class => Length (Container)'Old = Length (Container);
147.16/3 This function (combined with the Variable_Indexing and Implicit_Dereference aspects) provides a convenient way to gain read and write access to an individual element of a vector given a cursor. 147.17/3+ Reference returns an object whose discriminant is an access value that designates the element designated by Position. Tampering with the elements of Container is prohibited while the object returned by Reference exists and has not been finalized. 147.18/3 The element designated by Position is not an empty element after successful completion of this operation.
147.19/3+ procedure Assign (Target : in out Vector; Source : in Vector)
with Pre'Class => (if Tampering_With_Cursors_Prohibited (Target)
then raise Program_Error),
Post'Class => Length (Source) = Length (Target);
147.20/3 If Target denotes the same object as Source, the operation has no effect. If the length of Source is greater than the capacity of Target, Reserve_Capacity (Target, Length (Source)) is called. The elements of Source are then copied to Target as for an assignment_statement assigning Source to Target (this includes setting the length of Target to be that of Source).
147.21/3+ function Copy (Source : Vector; Capacity : Count_Type := 0)
return Vector with Pre'Class => (if Capacity /= 0 and then Capacity < Length (Source)
then raise Capacity_Error),
Post'Class => Length (Copy'Result) = Length (Source);
147.22/3+ Returns a vector whose elements are initialized from the corresponding elements of Source. If Capacity is 0, then the vector capacity is the length of Source; if Capacity is equal to or greater than the length of Source, the vector capacity is at least the specified value.
148/2+ procedure Move (Target : in out Vector;
Source : in out Vector)
with Pre'Class => (if Tampering_With_Cursors_Prohibited (Target)
then raise Program_Error) and then
(if Tampering_With_Cursors_Prohibited (Source)
then raise Program_Error),
Post'Class => (if Target = Source then True
else
Length (Target) = Length (Source'Old) and then Length (Source) = 0);
149/3 If Target denotes the same object as Source, then the operation has no effect. Otherwise, Move first calls Reserve_Capacity (Target, Length (Source)) and then Clear (Target); then, each element from Source is removed from Source and inserted into Target in the original order. The length of Source is 0 after a successful call to Move.
150/2+ procedure Insert (Container : in out Vector;
Before : in Extended_Index; New_Item : in Vector)
with Pre'Class => (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),
Post'Class => Length (Container)'Old + Length (New_Item) = Length (Container);
151/3+ If Length (New_Item) is 0, then Insert does nothing. Otherwise, it computes the new length NL as the sum of the current length and Length (New_Item); if the value of Last appropriate for length NL would be greater than Index_Type'Last, then Constraint_Error is propagated. [Editor's note: This last check might overflow if written as a Precondition; I didn't try.] 152/2 If the current vector capacity is less than NL, Reserve_Capacity (Container, NL) is called to increase the vector capacity. Then Insert slides the elements in the range Before .. Last_Index (Container) up by Length (New_Item) positions, and then copies the elements of New_Item to the positions starting at Before. Any exception raised during the copying is propagated.
153/2+ procedure Insert (Container : in out Vector;
Before : in Cursor; New_Item : in Vector);
with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Length (New_Item) /= 0 and then
Before /= No_Element and then
(not Cursor_Belongs_To_Container (Container, Before)) then raise Program_Error), Post'Class => Length (Container)'Old + Length (New_Item) = Length (Container);
154/3+ If Length (New_Item) is 0, then Insert does nothing. If Before is No_Element, then the call is equivalent to Insert (Container, Last_Index (Container) + 1, New_Item); otherwise, the call is equivalent to Insert (Container, To_Index (Before), New_Item);
155/2+ procedure Insert (Container : in out Vector;
Before : in Cursor; New_Item : in Vector; Position : out Cursor);
with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Before /= No_Element and then
(not Cursor_Belongs_To_Container (Container, Before))
then raise Program_Error), Post'Class => Length (Container)'Old + Length (New_Item) = Length (Container) and then
Cursor_Belongs_To_Container (Container, Position);
156/2+ If Before equals No_Element, then let T be Last_Index (Container) + 1; otherwise, let T be To_Index (Before). Insert (Container, T, New_Item) is called, and then Position is set to To_Cursor (Container, T).
157/2+ procedure Insert (Container : in out Vector;
Before : in Extended_Index; New_Item : in Element_Type; Count : in Count_Type := 1)
with Pre'Class => (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),
Post'Class => Length (Container)'Old + Count = Length (Container);
158/2 Equivalent to Insert (Container, Before, To_Vector (New_Item, Count));
159/2+ procedure Insert (Container : in out Vector;
Before : in Cursor; New_Item : in Element_Type; Count : in Count_Type := 1)
with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Count /= 0 and then
Before /= No_Element and then
(not Cursor_Belongs_To_Container (Container, Before)) then raise Program_Error), Post'Class => Length (Container)'Old + Count = Length (Container);
160/2 Equivalent to Insert (Container, Before, To_Vector (New_Item, Count));
161/2+ procedure Insert (Container : in out Vector;
Before : in Cursor; New_Item : in Element_Type; Position : out Cursor; Count : in Count_Type := 1)
with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Before /= No_Element and then
(not Cursor_Belongs_To_Container (Container, Before))
then raise Program_Error), Post'Class => Length (Container)'Old + Count = Length (Container) and then
Cursor_Belongs_To_Container (Container, Position);
162/2 Equivalent to Insert (Container, Before, To_Vector (New_Item, Count), Position);
163/2+ procedure Insert (Container : in out Vector;
Before : in Extended_Index; Count : in Count_Type := 1)
with Pre'Class => (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),
Post'Class => Length (Container)'Old + Count = Length (Container);
164/3+ If Count is 0, then Insert does nothing. Otherwise, it computes the new length NL as the sum of the current length and Count; if the value of Last appropriate for length NL would be greater than Index_Type'Last, then Constraint_Error is propagated. 165/2 If the current vector capacity is less than NL, Reserve_Capacity (Container, NL) is called to increase the vector capacity. Then Insert slides the elements in the range Before .. Last_Index (Container) up by Count positions, and then inserts elements that are initialized by default (see 3.3.1) in the positions starting at Before.
166/2+ procedure Insert (Container : in out Vector;
Before : in Cursor; Position : out Cursor; Count : in Count_Type := 1)
with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Before /= No_Element and then
(not Cursor_Belongs_To_Container (Container, Before))
then raise Program_Error), Post'Class => Length (Container)'Old + Count = Length (Container) and then
Cursor_Belongs_To_Container (Container, Position);
167/2 If Before equals No_Element, then let T be Last_Index (Container) + 1; otherwise, let T be To_Index (Before). Insert (Container, T, Count) is called, and then Position is set to To_Cursor (Container, T).
168/2+ procedure Prepend (Container : in out Vector;
New_Item : in Vector)
with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error),
Post'Class => Length (Container)'Old + Length (New_Item) = Length (Container);
169/2 Equivalent to Insert (Container, First_Index (Container), New_Item).
170/2+ procedure Prepend (Container : in out Vector;
New_Item : in Element_Type; Count : in Count_Type := 1)
with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error),
Post'Class => Length (Container)'Old + Count = Length (Container);
171/2 Equivalent to Insert (Container, First_Index (Container), New_Item, Count).
172/2+ procedure Append (Container : in out Vector;
New_Item : in Vector)
with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error),
Post'Class => Length (Container)'Old + Length (New_Item) = Length (Container);
173/2 Equivalent to Insert (Container, Last_Index (Container) + 1, New_Item).
174/2+ procedure Append (Container : in out Vector;
New_Item : in Element_Type; Count : in Count_Type := 1)
with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error),
Post'Class => Length (Container)'Old + Count = Length (Container);
175/2 Equivalent to Insert (Container, Last_Index (Container) + 1, New_Item, Count).
176/2+ procedure Insert_Space (Container : in out Vector;
Before : in Extended_Index; Count : in Count_Type := 1);
with Pre'Class => (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),
Post'Class => Length (Container)'Old + Count = Length (Container);
177/3 If Count is 0, then Insert_Space does nothing. Otherwise, it computes the new length NL as the sum of the current length and Count; if the value of Last appropriate for length NL would be greater than Index_Type'Last, then Constraint_Error is propagated. 178/2 If the current vector capacity is less than NL, Reserve_Capacity (Container, NL) is called to increase the vector capacity. Then Insert_Space slides the elements in the range Before .. Last_Index (Container) up by Count positions, and then inserts empty elements in the positions starting at Before.
179/2+ procedure Insert_Space (Container : in out Vector;
Before : in Cursor; Position : out Cursor; Count : in Count_Type := 1)
with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Before /= No_Element and then
(not Cursor_Belongs_To_Container (Container, Before))
then raise Program_Error), Post'Class => Length (Container)'Old + Count = Length (Container) and then
Cursor_Belongs_To_Container (Container, Position);
180/2 If Before equals No_Element, then let T be Last_Index (Container) + 1; otherwise, let T be To_Index (Before). Insert_Space (Container, T, Count) is called, and then Position is set to To_Cursor (Container, T).
181/2+ procedure Delete (Container : in out Vector;
Index : in Extended_Index; Count : in Count_Type := 1)
with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Index not in First_Index (Container) .. Last_Index (Container) + 1
then raise Constraint_Error),
Post'Class => Length (Container)'Old - Count <= Length (Container);
182/3+ If Count is 0, Delete has no effect. Otherwise, Delete slides the elements (if any) starting at position Index + Count down to Index. Any exception raised during element assignment is propagated.
183/2+ procedure Delete (Container : in out Vector;
Position : in out Cursor; Count : in Count_Type := 1)
with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Position = No_Element then raise Constraint_Error) and then (if not Cursor_Belongs_To_Container (Container, Position)
then raise Program_Error),
Post'Class => Length (Container)'Old - Count <= Length (Container);
184/2 Delete (Container, To_Index (Position), Count) is called, and then Position is set to No_Element.
185/2+ procedure Delete_First (Container : in out Vector;
Count : in Count_Type := 1)
with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error),
Post'Class => Length (Container)'Old - Count <= Length (Container);
186/2 Equivalent to Delete (Container, First_Index (Container), Count).
187/2+ procedure Delete_Last (Container : in out Vector;
Count : in Count_Type := 1);
with Pre'Class => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error),
Post'Class => Length (Container)'Old - Count <= Length (Container);
188/3 If Length (Container) <= Count, then Delete_Last is equivalent to Clear (Container). Otherwise, it is equivalent to Delete (Container, Index_Type'Val(Index_Type'Pos(Last_Index (Container)) Count + 1), Count).
189/2+ procedure Reverse_Elements (Container : in out Vector)
with Pre'Class => (if Tampering_With_Elements_Prohibited (Container)
then raise Program_Error),
Post'Class => Length (Container)'Old = Length (Container);
190/2 Reorders the elements of Container in reverse order.
191/2+ procedure Swap (Container : in out Vector;
I, J : in Index_Type) with Pre'Class => (if Tampering_With_Elements_Prohibited (Container)
then raise Program_Error) and then
(if I not in First_Index (Container) .. Last_Index (Container)
then raise Constraint_Error) and then
(if J not in First_Index (Container) .. Last_Index (Container)
then raise Constraint_Error),
Post'Class => Length (Container)'Old = Length (Container);
192/2+ Swap exchanges the values of the elements at positions I and J.
193/2+ procedure Swap (Container : in out Vector;
I, J : in Cursor); with Pre'Class => (if Tampering_With_Elements_Prohibited (Container)
then raise Program_Error) and then
(if I = No_Element or else J = No_Element
then raise Constraint_Error) and then
(if not Cursor_Belongs_To_Container (Container, I)
then raise Program_Error) and then
(if not Cursor_Belongs_To_Container (Container, J)
then raise Program_Error),
Post'Class => Length (Container)'Old - Count <= Length (Container);
194/2+ Swap exchanges the values of the elements designated by I and J.
195/2 function First_Index (Container : Vector) return Index_Type; 196/2 Returns the value Index_Type'First.
197/2+ function First (Container : Vector) return Cursor
with Post'Class => (if not Is_Empty (Container)
then Cursor_Belongs_To_Container (Container, First'Result) else First'Result = No_Element);
198/2 If Container is empty, First returns No_Element. Otherwise, it returns a cursor that designates the first element in Container.
199/2 function First_Element (Container : Vector) return Element_Type; 200/2 Equivalent to Element (Container, First_Index (Container)).
201/2 function Last_Index (Container : Vector) return Extended_Index; 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'Class => (if not Is_Empty (Container)
then Cursor_Belongs_To_Container (Container, Last'Result) 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.
205/2 function Last_Element (Container : Vector) return Element_Type; 206/2 Equivalent to Element (Container, Last_Index (Container)).
207/2 function Next (Position : Cursor) return Cursor; 208/2 If Position equals No_Element or designates the last element of the container, then Next returns the value No_Element. Otherwise, it returns a cursor that designates the element with index To_Index (Position) + 1 in the same vector as Position.
209/2 procedure Next (Position : in out Cursor); 210/2 Equivalent to Position := Next (Position).
211/2 function Previous (Position : Cursor) return Cursor; 212/2 If Position equals No_Element or designates the first element of the container, then Previous returns the value No_Element. Otherwise, it returns a cursor that designates the element with index To_Index (Position) 1 in the same vector as Position.
213/2 procedure Previous (Position : in out Cursor); 214/2 Equivalent to Position := Previous (Position).
215/2 function Find_Index (Container : Vector;
Item : Element_Type; Index : Index_Type := Index_Type'First)
return Extended_Index;
216/2 Searches the elements of Container for an element equal to Item (using the generic formal equality operator). The search starts at position Index and proceeds towards Last_Index (Container). If no equal element is found, then Find_Index returns No_Index. Otherwise, it returns the index of the first equal element encountered.
217/2+ function Find (Container : Vector;
Item : Element_Type; Position : Cursor := No_Element)
return Cursor
with Pre'Class => (if Position /= No_Element and then
(not Cursor_Belongs_To_Container (Container, Position))
then raise Program_Error),
with Post'Class => (if Find'Result then True
else Cursor_Belongs_To_Container (Container, Find'Result));
218/3+ Find searches the elements of Container for an element equal to Item (using the generic formal equality operator). The search starts at the first element if Position equals No_Element, and at the element designated by Position otherwise. It proceeds towards the last element of Container. If no equal element is found, then Find returns No_Element. Otherwise, it returns a cursor designating the first equal element encountered.
219/2 function Reverse_Find_Index (Container : Vector;
Item : Element_Type; Index : Index_Type := Index_Type'Last)
return Extended_Index;
220/2 Searches the elements of Container for an element equal to Item (using the generic formal equality operator). The search starts at position Index or, if Index is greater than Last_Index (Container), at position Last_Index (Container). It proceeds towards First_Index (Container). If no equal element is found, then Reverse_Find_Index returns No_Index. Otherwise, it returns the index of the first equal element encountered.
221/2+ function Reverse_Find (Container : Vector;
Item : Element_Type; Position : Cursor := No_Element)
return Cursor
with Pre'Class => (if Position /= No_Element and then
(not Cursor_Belongs_To_Container (Container, Position))
then raise Program_Error),
with Post'Class => (if Reverse_Find'Result then True
else Cursor_Belongs_To_Container (Container, Reverse_Find'Result));
222/3+ Reverse_Find searches the elements of Container for an element equal to Item (using the generic formal equality operator). The search starts at the last element if Position equals No_Element, and at the element designated by Position otherwise. It proceeds towards the first element of Container. If no equal element is found, then Reverse_Find returns No_Element. Otherwise, it returns a cursor designating the first equal element encountered.
223/2 function Contains (Container : Vector;
Item : Element_Type) return Boolean;
224/2 Equivalent to Has_Element (Find (Container, Item)).
227/2+ procedure Iterate
(Container : in Vector;
Process : not null access procedure (Position : in Cursor)) with Post'Class => Length (Container)'Old = Length (Container);
228/3 Invokes Process.all with a cursor that designates each element in Container, in index order. Tampering with the cursors of Container is prohibited during the execution of a call on Process.all. Any exception raised by Process.all is propagated.
229/2 procedure Reverse_Iterate
(Container : in Vector;
Process : not null access procedure (Position : in Cursor)) with Post'Class => Length (Container)'Old = Length (Container);
230/3 Iterates over the elements in Container as per procedure Iterate, except that elements are traversed in reverse index order.
230.1/3 function Iterate (Container : in Vector)
return Vector_Iterator_Interfaces.Reversible_Iterator'Class;
230.2/3 Iterate returns a reversible iterator object (see 5.5.1) that will generate a value for a loop parameter (see 5.5.2) designating each node in Container, starting with the first node and moving the cursor as per the Next function when used as a forward iterator, and starting with the last node and moving the cursor as per the Previous function when used as a reverse iterator. Tampering with the cursors of Container is prohibited while the iterator object exists (in particular, in the sequence_of_statements of the loop_statement whose iterator_specification denotes this object). The iterator object needs finalization.
230.3/3 function Iterate (Container : in Vector; Start : in Cursor)
return Vector_Iterator_Interfaces.Reversible_Iterator'Class;
230.4/3 If Start is not No_Element and does not designate an item in Container, then Program_Error is propagated. If Start is No_Element, then Constraint_Error is propagated. Otherwise, Iterate returns a reversible iterator object (see 5.5.1) that will generate a value for a loop parameter (see 5.5.2) designating each node in Container, starting with the node designated by Start and moving the cursor as per the Next function when used as a forward iterator, or moving the cursor as per the Previous function when used as a reverse iterator. Tampering with the cursors of Container is prohibited while the iterator object exists (in particular, in the sequence_of_statements of the loop_statement whose iterator_specification denotes this object). The iterator object needs finalization. 231/3 The actual function for the generic formal function "<" of Generic_Sorting is expected to return the same value each time it is called with a particular pair of element values. It should define a strict weak ordering relationship (see A.18); it should not modify Container. If the actual for "<" behaves in some other manner, the behavior of the subprograms of Generic_Sorting are unspecified. The number of times the subprograms of Generic_Sorting call "<" is unspecified.
232/2 function Is_Sorted (Container : Vector) return Boolean; 233/2 Returns True if the elements are sorted smallest first as determined by the generic formal "<" operator; otherwise, Is_Sorted returns False. Any exception raised during evaluation of "<" is propagated.
234/2+ procedure Sort (Container : in out Vector)
with Pre'Class => (if Tampering_With_Elements_Prohibited (Container)
then raise Program_Error),
Post'Class => Length (Container)'Old = Length (Container);
[We could check in the postcondition that these are sorted, but that's rather expensive, and these assertions won't usually be ignored.] 235/2 Reorders the elements of Container such that the elements are sorted smallest first as determined by the generic formal "<" operator provided. Any exception raised during evaluation of "<" is propagated.
236/2+ procedure Merge (Target : in out Vector;
Source : in out Vector)
with Pre'Class => (if Tampering_With_Elements_Prohibited (Target)
then raise Program_Error) and then
(if Tampering_With_Elements_Prohibited (Source)
then raise Program_Error),
Post'Class => Length (Source) = 0 and then
Length (Target) = Length (Source)'Old + Length (Target)'Old;
[Checking whether these are sorted is too expensive, so we won't try; especially as wee don't specify what happens if they're not. We don't have a foolproof way to check if these are the same object, so we don't try that, either.] 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 removes elements from Source and inserts them into Target; afterwards, Target contains the union of the elements that were initially in Source and Target; Source is left empty. If Target and Source are initially sorted smallest first, then Target is ordered smallest first as determined by the generic formal "<" operator; otherwise, the order of elements in Target is unspecified. Any exception raised during evaluation of "<" is propagated.
!discussion
For this initial version, we've prototyped the changes needed for a single package (Ada.Containers.Vectors). The other 6 basic containers would need similar wording changes. We also might want some additional preconditions related to capacity for the bounded versions (although that would be painful to do, as the bounded versions are described by difference).
Since the other containers would be very similar, we did just this one container in order to determine whether it is worth following through with the effort to do the remainder of the containers.
The prototype only shows the wording for the main body of the definition of Ada.Containers.Vectors. The package specification would also have to be modified, and there might be some wording simplifications possible in the other sections. These were not looked at for this prototype.
A handful of new predicate functions are needed for these preconditions. These are clearly marked as new. All other operations are pre-existing; the contracts are new and some of the English text has been simplified but no change in semantics is intended. The paragraph numbers of modified paragraphs are marked with a "+". The edits to text (including deletions) is not shown in order to illustrate the improvement (or lack thereof) in readability after converting English checks to Ada expressions. (A lot of connector words were dropped, especially "otherwise", which should improve readability.)
The prototype includes very simple postconditions on the operations. These are by no means complete; for instance, we could easily have postconditions on the capacity of the container. The question of how far we ought to go with postconditions is one that will need to be discussed.
One postcondition not included that should be is
Tampering_With_Cursors_Prohibited (Container)'Old = Tampering_With_Cursors_Prohibited (Container) and Tampering_With_Elements_Prohibited (Container)'Old = Tampering_With_Elements_Prohibited (Container)
This says that the tampering state is not changed by the subprogram. Knowing that will allow compilers to eliminate extra tampering checks - often multiple modifications will be grouped together such that only a single check is needed.
This should be included on every subprogram that has a Container parameter other that Reference and Constant_Reference. (Note that the routines with callbacks, like Iterate and Query_Element, change the tampering state internally, but the state is unchanged when they complete.) I would suggest doing that with a blanket rule rather than cluttering the definitions with these two extra lines.
There are two additional issues with this addition. First, most of the reading routines do not have a Container parameter. We would need a global out annotation (Global out => null) on most of those routines to state that the container tampering state (as well as any other global state) is unchanged. If we had such an annotation, we would probably want to specify it with a blanket rule as well. (But we could also forget the blanket rules and simply repeat these on every routine, after all, that's what an implementation would do. Or alternatively, write everything out in the package specification and use a simplified version in the body of the clause.)
Second, I don't see any way to show where the tampering is prohibited. That occurs in callbacks (Query_Element, Update_Element, Iterate, Reverse_Iterate), when an iterator object returned by Iterate is used, and during the lifetime of the object returned by Reference and Constant_Reference. Unfortunately, none of these places can be described by the constract aspects currently available with Ada. One could imagine having appropriate preconditions on the callback access values such that we could describe it there, but I don't have any idea of a way to describe its association with use of the objects.
!ASIS
No ASIS impact.
!ACATS test
These changes are not intended to change any of the semantics of the containers, so no new ACATS tests are needed. To the extent that the ACATS doesn't test the error cases, C-Tests are needed to do that (but those are needed whether or not this AI is approved).
!appendix

From: Randy Brukardt
Sent: Tuesday, February 11, 2014  12:18 PM

[A partial message in response to messages in the thread filed in AI12-0111-1.]

> One thing that would have helped is to design all the safety stuff so
> that it was in the form of preconditions and postconditions, which
> could be easily suppressed.

I've suggested that before (including on Friday). It's still possible, of
course, it would be compatible to do so (we couldn't use predicates, but
preconditions would work). (But it would be a lot of work for the Standard, and
some for implementers.) Of course, we couldn't have done this for Ada 2005, as
we  didn't have preconditions then.

In particular, if we added the routine Is_Tampering_with_Cursors (Container
: in Vector) return Boolean, then the bounded vector Insert could be:

procedure Insert (Container : in out Vector;
                  Before    : in     Extended_Index;
                  New_Item  : in     Vector)
    with Pre => (if Container.Is_Tampering_with_Cursors then raise Program_Error with "Tampering check") and then
                (if Before not in Container.First_Index .. Container.Last_Index + 1 then raise Constraint_Error) and then
                (if Container.Length = Container.Capacity then raise Capacity_Error),
         Post => (Container.Is_Tampering_with_Cursors'Old = Container.Is_Tampering_with_Cursors) and
                  Container.Length'Old + 1 = Container.Length);

The postcondition is intended to show provers that a call of Insert doesn't
change the tampering state.

Having these as preconditions and postconditions would allow easy suppression
of the checks (and also would allow the compiler to combine and/or eliminate
them, so it wouldn't be as necessary to suppress them).

This seems to me to be the best way to fix the performance problem caused by
the checking. But that presumes that we're sure that the performance problem
is caused solely by the checking.

****************************************************************

From: Randy Brukardt
Sent: Wednesday, January 11, 2017  7:33 PM

[The quote is from the e-mail discussion of AI12-0215-1 - Editor.]

>Yes, this exhibit N in the long list of reasons that we should have had all
>of the container operations having a container parameter.

It strikes me that it might make sense to put on the record all of these
reasons. We're talking about a routine like:

    function Next (Position : Cursor) return Cursor;

(1) This routine (and its relatives) is not primitive for the container type,
    so it doesn't get inherited by derivation. Thus derivation of the
    container type is incomplete and rather useless;

(2) One can't use the prefixed notation to call this routine (Cursor is not
    tagged, and you wouldn't want it to be the prefix anyway);

(3) The Global aspect for this routine is problematic, as we have to include
    any container object of the correct type. (The object being read not being
    part of the specification.) That means we either need some unusual Global
    specification for this case, or we have to fall back to "reads all", which
    is far from ideal. (Recall that Cursor is a private type, from outside of
    the package it doesn't appear to designate anything.)

(4) Reading and writing the container is not symmetric. One uses different
    parameter lists for each. (This is mitigated somewhat by the Ada 2012
    Reference routine and the indexed notation - probably most new code will
    use that, but of course the original routines still can be used.)

---

If, instead, the routine had been declared as (I'm showing the precondition,
which would have been written in English in Ada 2005/12):

    function Next (Container : Map; Position : Cursor) return Cursor
       with Pre => (if not Cursor_Belongs_To_Container (Container, Position)
                    then raise Program_Error);

The routine is primitive, so (1) and (2) are eliminated (in particular,
prefixed notation can be used). The precondition eliminates (3); we only need
to include global container state (the storage pool, at a minimum) in the
Global aspect [and nothing at all for the bounded containers). (4) is
eliminated as Element and Replace have the same type profile (different modes,
of course).

The only negative is expressed by the precondition: a check is needed that the
cursor belongs to the container. Of course as a precondition this can often be
eliminated. [It's likely that an earlier precondition or postcondition will
have previously checked/asserted this fact, and this could easily be a stable
property that doesn't change for most routines.]

---

A possibility here would be to add the necessary additional routines. For the
Maps, there are only 6 routines that could be added (2 Nexts, 2 Previouses,
Key, and Element) -- the others are operators which obviously can't have more
parameters. [The next three parameter "<" that I see will be the first. ;-)]
That would allow applications that care about Global or want to uniformly use
prefixed notation or to do a derivation to work usefully, and won't (I think)
equire any other code to change. [It would be only incompatible with anyone
hat decided to add these themselves somewhere; that might make some calls
ambiguous. That's the normal problem from added new routines.]

I'm thinking that adding these routines might be a good idea, especially for
the purposes of AI12-0112-1 (which intends to add Pre/Post/Global/Nonblocking/
Stable_Properties to all of the containers, along with some additional
routines to support those, and remove English text where possible). The nasty
Global aspect for the existing routines seems to be justification enough (and
the other reasons add importance). Any objections to adding them to the next
draft of AI12-0112-1???

****************************************************************

From: Randy Brukardt
Sent: Thursday, January 12, 2017  3:46 PM

[From mail found about AI12-0215-1 - Editor.]

> > My initial thought was that this is fine, (with the obvious caveat 
> > that this is a tagged type, so there has to be a null extension on 
> > the
> > type) but then I remembered that you can't usefully derive
> a type in a containers package.
> 
> This seems more of a failing of the structure of the containers 
> packages, and doesn't argue against the value of the feature more 
> generally.  As you mention below, and we have discovered for other 
> reasons in the context of SPARK, having cursor operations that don't 
> take the associated container as a parameter create numerous problems 
> when it comes to doing anything "formal" with the containers.

I take it from this that you agree with my suggestion to add the missing
container reading operations so that derivation and formal analysis work
appropriately? (I made that a separate thread, that no one seems to have
commented on so far.) We can't get rid of the existing operations for obvious
reasons, but we could add ones that work "right" and formal uses could just
ignore the ones without a container parameter. (That seems like a more
practical solution than defining a completely separate set of containers that
have better behavior.)

****************************************************************

From: Tucker Taft
Sent: Thursday, January 12, 2017  4:31 PM

[Just the reply to the above message, see AI12-0215-1 for the whole
thread - Editor.]

> ... I take it from this that you agree with my suggestion to add the 
> missing container reading operations so that derivation and formal 
> analysis work appropriately? (I made that a separate thread, that no 
> one seems to have commented on so far.)

Yes, I agree with that proposal.

****************************************************************

From: Bob Duff
Sent: Sunday, January 15, 2017  6:01 PM

> If, instead, the routine had been declared as (I'm showing the 
> precondition, which would have been written in English in Ada 2005/12):
> 
>     function Next (Container : Map; Position : Cursor) return Cursor
>        with Pre => (if not Cursor_Belongs_To_Container (Container, Position)
>                     then raise Program_Error);

I have often thought that those ops should take a Container param.

The SPARK folks at AdaCore designed "formal containers" to be used with
proofs. Not proving the implementation of the container is correct, but
proving that clients obey the pre/post. They came to the same conclusion. They
tried to keep their interface similar to the language-defined ones, but they
found the need to add the Container params.

> I'm thinking that adding these routines might be a good idea, 
> especially for the purposes of AI12-0112-1 (which intends to add 
> Pre/Post/Global/Nonblocking/Stable_Properties to all of the 
> containers, along with some additional routines to support those, and 
> remove English text where possible). The nasty Global aspect for the 
> existing routines seems to be justification enough (and the other 
> reasons add importance). Any objections to adding them to the next draft of
> AI12-0112-1???

I don't object to adding those routines, but I think I object to AI12-0112-1.
Sounds like a lot of useless work for little gain.

And if we do that, it should be done by hacking on an existing container
implementation, with regression testing.  There's no way ARG can get it right
in a vacuum.

****************************************************************

From: Randy Brukardt
Sent: Monday, January 16, 2017  7:59 PM

> I don't object to adding those routines, but I think I object to 
> AI12-0112-1.  Sounds like a lot of useless work for little gain.
> 
> And if we do that, it should be done by hacking on an existing 
> container implementation, with regression testing.
> There's no way ARG can get it right in a vacuum.

Why? It certainly doesn't hurt to try the changes in an implementation, but I 
don't think there is much chance that much beyond a handful of typos would be
found.

For Pre and Nonblocking, this is just replacing English rules with
specifications. It's rather rote; all of the preconditions are of the form
"(if Some_Predicate (Container) then raise Some_Exception)", combined with
"and then". Any cut-and-errors would be clearly obvious (failing the Dewar
rules). Besides, we're planning to use Nonblocking in the entire Ada library
(it doesn't work if that's not done), so whether or not a containers overhaul
is done isn't relevant to it.

For Post/Stable_Properties, we're also encoding the English rules; there's a
bit more risk of omission but again errors would be clearly obvious
(requiring an obvious nonsense property).

Global could be more of a problem, but there I think we have to be very
conservative; no existing implementation is going to help much there, as the
rules have to allow far more than any single implementation needs --
regardless of design.

If there is any risk, it is in the English wording changes (deleting too much
certainly would be possible). But if you look at the prototype AI12-0112-1,
you'll see that the descriptions of the container operations are *much* more
understandable. Getting the English for what really was code was very
difficult and probably isn't exactly right. Most likely, we'll fix some errors
by this exercise (and probably fix some errors in existing implementations,
too, if our experience with containers ACATS tests is any guide). [Indeed, by
making these checks first-class preconditions, we will eliminate most of the
need for ACATS tests on those checks, which are annoying to write, and only
important if someone has screwed up. That would allow redirecting that effort
elsewhere.]

****************************************************************

topic Pragma Suppress (Container_Checks)
!reference Ada 202x 2012 RM11.5, A.18.4
!from Gautier de Montmollin 17-12-05
!keywords Suppress Container_Checks
!discussion

Hello,

Like it or not, GNAT has a pragma Suppress (Container_Checks) which is
activated with the -gnatp option. It changes changes the behaviour
of Maps (and perhaps other containers) when an element hasn't been
found: the behaviour of function Element @ A.18.4 34/2 fails, and
Constraint_Error is NOT propagated as expected.
Especially, function Element (Container : Map; Key : Key_Type) return Element_Type; (68/2)
cannot be used at all.

Actually my proposal is either:

  - For the Ada standard, to add this pragma. It would join the other documented
    pragmata in 11.5 (Suppressing Checks) that have to be used with caution.
  - Or for the GNAT compiler, to warn better of the risks of this undocumented
    (in the Ada standard sense) pragma

****************************************************************

From: Randy Brukardt
Sent: Tuesday, December 5, 2017  3:57 PM

(1) pragma Suppress always causes the risk of making a program's erroneous.
If this is a real concern (and it should be), don't use pragma Suppress.
(It's almost never necessary with modern compilers which can eliminate the
vast majority of checks by optimizations.) [I'm not going to say more here,
as it would get off-topic; I had much more to say about this in a recent
comp.lang.ada thread.]

(2) We already have this issue on our radar. In particular, AI12-0112-1
intends to make almost all of the container checks into explicit preconditions
and provide a way to suppress language-defined preconditions. This will make
the description of the checks clearer and still provide the functionality if
it is needed.

(3) 11.5(27/2) allows an implementation to define additional check names for
Suppress. There's no requirement that the check names be language-defined.
So GNAT is perfectly OK defining Container_Check, Box_Check, Gautier_Check,
or any other name that they like. :-) As to the quality of their
documentation, that's hardly a language Standard concern.

****************************************************************


Questions? Ask the ACAA Technical Agent