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

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

!standard A.18.2(99/3)          18-03-01 AI12-0112-1/02
!class Amendment 14-05-15
!status work item 14-05-15
!status received 15-02-11
!priority Medium
!difficulty Medium
!subject Contracts for container operations
!summary
We add contracts to all of the container operations. These include aspect Nonblocking and aspect Global (needed for the parallel operations).
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.
We add some additional operations to the containers to use in the preconditions and to simplify the needed Global aspects.
Finally, we added a mechanism to suppress precondition checks for the containers; this puts the containers on the same footing as arrays in regards to the trade-offs of checking and performance.
!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.
Additionally, check suppression is a missing feature in Ada. While a user of an array can suppress checks if they are sufficiently convinced of correctness (and thus get better performance), there is no way to do this for the containers.
We also need to add the Nonblocking (AI12-0064-2) and Global (AI12-0079-1) aspects to the containers, so that they can usefully be used with the new parallel features (including AI12-0119-1 and AI12-0242-1), as well as in statically checked protected operations (using aspect Nonblocking).
Finally, some of the container reading operations are defined so that the container object is not passed explicitly. This has a number of bad effects:
(1) The reading operations are not primitive, so a derivation of a container type is missing reading operations and thus is rather useless; (2) Prefix notation cannot be used on such reading operations, as one wants the prefix to be the container object (it can be used on writing operations, which is asymetric); (3) Since the container is not named explicitly, it is used implicitly. That requires a Global aspect including all containers of the correct type -- which could prevent parallel operation in some cases.
Therefore, we add new analogs of these operations that include a container parameter.
!proposal
(See summary.)
[Questions:
(1) I used the name "Container_Check" for the check name (for use in pragma Suppress). This sort of stomps on GNAT's existing implementation, although they should be pretty close in functionality (exceptions not raised through preconditions are not included in this Ada definition). Is this a problem? Is there an alternative name? (See !discussion.)
(2) Should the preconditions be repeated in the semantics section or just shown in the package specification? I have them repeated for now, but that's relatively easy to change.
(3) I used Pre and Post rather than Pre'Class and Post'Class, since these mostly belong to the specific routine rather than any routine matching the profile. This way, they can be eliminated for a derived type if desired. (The usual rules mean that any delegation to the original routine will check the original Pre/Post.) This does mean that they won't necessarily follow LSP for a dispatching call, but that seems unnecessary for the containers (extensions seem unusual, and using multiple versions of a single container simultaenously more so). By using Pre, an implementation can generate the precondition as part of the subprogram body if it wishes (or it can generate it at the call site to support optimization and suppressibility). Objections?
(4) I've overridden the usual Nonblocking and Global status for the various predicate routines, to essentially mark these as Pure. If Nonblocking => True is used, this would prevent calling the formal subprograms in the associated routines. Can anyone think of a reason NOT to require these routines to be pure (in general or specifically)?
(5) The global setting "Access subtype_mark" says that it applies to all of the "(aliased)" objects of subtype_mark. For a tagged type (like Vector), it needs to apply to all objects of the type, since 'Access can be used inside of the package, and has to for the containers packages in order to create the needed cursor semantics. I'm assuming that is the case.
(6) I had to use prefixed notation in some preconditions, as the function I wanted to call has the same name as a parameter of the routine (see To_Vector and Reserve_Capacity for examples). The direct name is hidden in that case, so prefixed notation seems like the best way to call the function. Should all of these be written in prefixed notation for consistency? (We decided the reverse the previous time, I think.) I suppose I could have used an expanded name instead (Vectors.Length (Container)) - but that's just longer for no obvious reason.
(7) I intend to check that this specification is compilable, and would prefer to check it against GNAT's existing implementation (meaning compiling the spec with the existing GNAT body enhanced with the additional routines). For that, I'll need some help from someone at AdaCore, as I don't have access to the AdaCore test suite and would need help finding the source code and recompiling part of the runtime with GNAT (never having done that). Is there a volunteer??
(8) It would be best if we had a way to specify a precondition for anonymous access-to-subprogram types in order to properly handle Tampering_With_Cursors_Prohibited for Query_Element/Update_Element/subprogram iterators. None has been proposed to date. (The only sane way seems to be via a named anonymous access subtype, which clearly would need a better name. ;-)
We also would need a way to indicate that Tampering_With_Cursors_Prohibited is true during the lifetime of an iterator or reference object. It's not clear to me how best to indicate this in the specification of the containers. Perhaps SPARK users would have a suggestion.
Neither of these are critical, in the sense that the specification will work without them. It just means that tools and compilers cannot detect failing tampering checks (and optimize away unnecessary checks) based on these properties alone.
]
!wording
[See the !discussion for general notes before reading this.] [Notes: This version only shows the final result; it does not show any deleted text. See the very end of this section for the text to be added to 11.5; it was put last as it isn't particularly important, but it should be at the start in the final AI as we usually show changes in order. Various notes are given in square brackets; these are for the benefit of ARG readers and will be removed in the Standard.]
with Ada.Iterator_Interfaces; generic type Index_Type is range <>; type Element_Type is private; with function "=" (Left, Right : Element_Type) return Boolean is <>; package Ada.Containers.Vectors with Preelaborate, Remote_Types, Nonblocking => Equal_Element'Nonblocking, Global => Equal_Element'Global & in out Ada.Containers.Vectors & <<some impl-defed helper packages>> 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 package. <<some impl-defed helper packages>> is a placeholder for however we decide to deal with helper packages. Note that in the Bounded version, Global is just Equal_Element'Global.]
subtype Extended_Index is Index_Type'Base range Index_Type'First-1 .. Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1; No_Index : constant Extended_Index := Extended_Index'First;
type Vector is tagged private with Constant_Indexing => Constant_Reference, Variable_Indexing => Reference, Default_Iterator => Iterate, Iterator_Element => Element_Type, Stable_Properties => Length, Capacity, Tampering_With_Cursors_Prohibited, Tampering_With_Elements_Prohibited; pragma Preelaborable_Initialization(Vector);
type Cursor is private; pragma Preelaborable_Initialization(Cursor);
Empty_Vector : constant Vector;
No_Element : constant Cursor;
function Equal_Element (Left, Right : Element_Type) return Boolean renames "=";
[Note: We need this renames of the formal parameter in order to be able to write the Nonblocking and Global aspects.]
[The rest of the package is as described in the detailed wording below. The specs would match.]
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
with Nonblocking => True,
Global => access Vector;
[We have to assume this looks at the container object.] 97.3/3 Returns True if Position designates an element, and returns False otherwise.
New function Has_Element (Container : Vector; Position : Cursor) return Boolean
with Nonblocking => True,
Global => in out null;
New Returns True if Position designates an element in Container, and returns False otherwise.
New AARM Ramification: If Position is No_Element, Has_Element returns False.
98/2 function "=" (Left, Right : Vector) return Boolean;
[Note: This depends on the formal parameter "=", so we use the default values for Global and Nonblocking.] 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 Tampering_With_Cursors_Prohibited (Container : Vector) return Boolean
with Nonblocking => True,
Global => in out null;
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
with Nonblocking => True,
Global => in out null;
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 => To_Vector'Result.Length = Length and then
not Tampering_With_Elements_Prohibited (To_Vector'Result) and then not Tampering_With_Cursors (To_Vector'Result) and then To_Vector'Result.Capacity >= 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 => Length (To_Vector'Result) = Length and then not Tampering_With_Elements_Prohibited (To_Vector'Result) and then not Tampering_With_Cursors (To_Vector'Result) and then To_Vector'Result.Capacity >= 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 => Length (Vectors."&"'Result) = Length (Left) + Length (Right),
not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then not Tampering_With_Cursors (Vectors."&"'Result) and then Vectors."&"'Result.Capacity >= 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 => Vectors."&"'Result.Length = Length (Left) + 1 and then
not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then not Tampering_With_Cursors (Vectors."&"'Result) and then Vectors."&"'Result.Capacity >= 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 => Length (Vectors."&"'Result) = Length (Right) + 1 and then
not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then not Tampering_With_Cursors (Vectors."&"'Result), Vectors."&"'Result.Capacity >= 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 => Length ("&"'Result) = 2 and then
not Tampering_With_Elements_Prohibited (Vectors."&"'Result) and then not Tampering_With_Cursors (Vectors."&"'Result) and Vectors."&"'Result.Capacity >= 2;
111/2 Returns a vector comprising the element Left followed by the element Right.
112/2 function Capacity (Container : Vector) return Count_Type
with Nonblocking => True,
Global => in out null;
113/2 Returns the capacity of Container.
114/2 procedure Reserve_Capacity (Container : in out Vector;
Capacity : in Count_Type)
with 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 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
with Nonblocking => True,
Global => in out null;
117/2 Returns the number of elements in Container.
118/2+ procedure Set_Length (Container : in out Vector;
Length : in Count_Type)
with Pre => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error),
Post => Container.Length = Length and then
Capacity (Container) >= 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
with Nonblocking => True,
Global => in out null;
121/2 Equivalent to Length (Container) = 0.
122/2+ procedure Clear (Container : in out Vector)
with Pre => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error),
Post => 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 => (if Index in First_Index (Container) .. Last_Index (Container)
then Has_Element (Container, To_Cursor'Result) else To_Cursor'Result = No_Element),
Nonblocking => True;
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. For the purposes of determining whether the parameters overlap in a call to To_Cursor, the Container parameter is not considered to overlap with any object [(including itself)].
126/2 function To_Index (Position : Cursor) return Extended_Index
with Global => Vectors'Global & in access Vector,
Nonblocking => True;
[Note: No postcondition here, since we can't name the container. See below.] 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.
New function To_Index (Container : Vector; Position : Cursor) return Extended_Index
when Pre => (if Position /= No_Element and then
not Has_Element (Container, Position) then raise Program_Error),
Post => (if Position = No_Element then To_Index'Result = No_Index
else To_Index'Result in First_Index (Container) ..
Last_Index (Container)),
Nonblocking => True;
New If Position is No_Element, No_Index is returned. Otherwise, the index (within its containing vector) of the element designated by Position is returned.
128/2+ function Element (Container : Vector;
Index : Index_Type)
return Element_Type with Pre => (if Index not in First_Index (Container) .. Last_Index (Container)
then raise Constraint_Error),
Nonblocking => True;
129/2+ Element returns the element at position Index.
130/2+ function Element (Position : Cursor) return Element_Type
with Pre => (if Position = No_Element then raise Constraint_Error),
Nonblocking => True, Global => Vectors'Global & in access Vector;
131/2+ Element returns the element designated by Position.
New function Element (Container : Vector; Position : Cursor) return Element_Type
with Pre => (if Position = No_Element then raise Constraint_Error) and then
(if not Has_Element (Container, Position)
then raise Program_Error),
Nonblocking => True;
New 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 => (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);
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. 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)], and the Index parameter is considered to overlap with the element at position Index.
134/2+ procedure Replace_Element (Container : in out Vector;
Position : in Cursor; New_Item : in Element_Type);
with Pre => (if Tampering_With_Elements_Prohibited (Container)
then raise Program_Error) and then
(if Position = No_Element then raise Constraint_Error) and then (if not Has_Element (Container, Position)
then raise Program_Error);
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. 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)].
136/2+ procedure Query_Element
(Container : in Vector;
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);
[Tampering ought to be indicated for the access procedure here, but we don't have a mechanism to do that. See the questions above.] 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 => (if Position = No_Element then raise Constraint_Error);
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 => (if Index not in First_Index (Container) .. Last_Index (Container) then raise Constraint_Error);
[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 => (if Position = No_Element then raise Constraint_Error) and then (if not Has_Element (Container, Position) then raise Program_Error);
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 => (if Index not in First_Index (Container) .. Last_Index (Container)
then raise Constraint_Error);
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 => (if Index not in First_Index (Container) .. Last_Index (Container)
then raise Constraint_Error);
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 => (if Position = No_Element then raise Constraint_Error) and then
(if not Has_Element (Container, Position)
then raise Program_Error);
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 => (if Position = No_Element then raise Constraint_Error) and then
(if not Has_Element (Container, Position)
then raise Program_Error);
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 => (if Tampering_With_Cursors_Prohibited (Target)
then raise Program_Error),
Post => Length (Source) = Length (Target),
Capacity (Target) >= 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 => (if Capacity /= 0 and then Capacity < Length (Source)
then raise Capacity_Error),
Post => Length (Copy'Result) = Length (Source) and then
Copy'Result.Capacity >= (if Capacity = 0 then
Length (Source) else Capacity);
147.22/3+ Returns a vector whose elements are initialized from the corresponding elements of Source.
148/2+ procedure Move (Target : in out Vector;
Source : in out Vector)
with Pre => (if Tampering_With_Cursors_Prohibited (Target)
then raise Program_Error) and then
(if Tampering_With_Cursors_Prohibited (Source)
then raise Program_Error),
Post => (if Target = Source then True
else
Length (Target) = Length (Source'Old) and then Length (Source) = 0 and then Capacity (Target) >= Length (Source'Old));
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.
150/2+ procedure Insert (Container : in out Vector;
Before : in Extended_Index; New_Item : in Vector)
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) and then
(if Length (Container) + Length (New_Item) > Index_Type'Last
then raise Constraint_Error),
[Note: This length calculation might overflow, but if it does, that's OK, as the rules require Constraint_Error to be raised in this case.]
Post => Length (Container)'Old + Length (New_Item) = Length (Container) and then
Capacity (Container) >= 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). 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 => (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 Has_Element (Container, Before))
then raise Program_Error) and then (if Length (Container) + Length (New_Item) > Index_Type'Last
then raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) = Length (Container),
Capacity (Container) >= 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 => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Before /= No_Element and then
(not Has_Element (Container, Before)) then raise Program_Error),
Post => Length (Container)'Old + Length (New_Item) = Length (Container) and then
Has_Element (Container, Position) and then Capacity (Container) >= Length (Container);
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 => (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) and then
(if Length (Container) + Count > Index_Type'Last
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= 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 => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Count /= 0 and then
Before /= No_Element and then (not Has_Element (Container, Before)) then raise Program_Error) and then
(if Length (Container) + Count > Index_Type'Last
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= 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 => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Before /= No_Element and then
(not Has_Element (Container, Before))
then raise Program_Error), Post => Length (Container)'Old + Count = Length (Container) and then
Has_Element (Container, Position) and then Capacity (Container) >= Length (Container);
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 => (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) and then
(if Length (Container) + Count > Index_Type'Last
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= 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. 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 => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Before /= No_Element and then
(not Has_Element (Container, Before))
then raise Program_Error) and (if Length (Container) + Count > Index_Type'Last
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Has_Element (Container, Position) and then Capacity (Container) >= Length (Container);
67/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 => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Length (Container) + Length (New_Item) > Index_Type'Last
then raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) = Length (Container) and then
Capacity (Container) >= 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 => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Length (Container) + Count > Index_Type'Last
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= 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 => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Length (Container) + Length (New_Item) > Index_Type'Last
then raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) = Length (Container) and then
Capacity (Container) >= 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 => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Length (Container) + Count > Index_Type'Last
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= 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 => (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) + Count > Index_Type'Last
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= 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. 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 => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Before /= No_Element and then
(not Has_Element (Container, Before))
then raise Program_Error), (if Length (Container) + Count > Index_Type'Last
then raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Has_Element (Container, Position) and then Capacity (Container) >= Length (Container);
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 => (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 => 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 => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error) and then
(if Position = No_Element then raise Constraint_Error) and then (if not Has_Element (Container, Position)
then raise Program_Error),
Post => 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 => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error),
Post => 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 => (if Tampering_With_Cursors_Prohibited (Container)
then raise Program_Error),
Post => 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 => (if Tampering_With_Elements_Prohibited (Container)
then raise Program_Error);
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 => (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);
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 => (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 Has_Element (Container, I)
then raise Program_Error) and then
(if not Has_Element (Container, J)
then raise Program_Error);
194/2+ 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 => in out 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)
then Has_Element (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 is
with Pre => (if Is_Empty (Container) then raise Constraint_Error);
200/2 Equivalent to Element (Container, First_Index (Container)).
201/2 function Last_Index (Container : Vector) return Extended_Index
with Nonblocking => True,
Global => in out null, Post => (if Length (Container) = 0 then Last_Index'Result = No_Index
else Last_Index'Result = Length (Container) - 1 + Index_Type'First);
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)
then Has_Element (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
with Pre => (if Is_Empty (Container) then raise Constraint_Error);
206/2 Equivalent to Element (Container, Last_Index (Container)).
207/2+ function Next (Position : Cursor) return Cursor
with Global => Vectors'Global & in access Vector,
Nonblocking => True, Post => (if Position = No_Element then Next'Result = No_Element
else True);
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.
New function Next (Container : Vector; Position : Cursor) return Cursor
with 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 else Next'Result = No_Element and then
Position'Old = Last (Container)),
Global => in out null, Nonblocking => True;
New If Position equals No_Element or designates the last element of 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)
with Global => Vectors'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
(not Has_Element (Container, Position))
then raise Program_Error), Post => (if Position /= No_Element
then Has_Element (Container, Position)),
Global => in out null, Nonblocking => True;
New Equivalent to Position := Next (Position).
211/2+ function Previous (Position : Cursor) return Cursor
with Global => Vectors'Global & in access Vector,
Nonblocking => True, Post => (if Position = No_Element then Previous'Result = No_Element
else True);
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.
New function Previous (Container : Vector; Position : Cursor) return Cursor
with 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 else Previous'Result = No_Element and then
Position'Old = First (Container)),
Global => in out null, Nonblocking => True;
New 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)
with Global => Vectors'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
(not Has_Element (Container, Position))
then raise Program_Error), Post => (if Position /= No_Element
then Has_Element (Container, Position)),
Global => in out null, Nonblocking => True;
New 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 => (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));
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 => (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));
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));
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))
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; with Pre => (if Start = No_Element then raise Constraint_Error) and then
(if not Has_Element (Start, Position) then raise Program_Error);
230.4/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 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);
[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 => (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;
[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.] 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.
-----------------------------------------
A.18.11 The Generic Package Containers.Indefinite_Vectors
[So far as I can tell, the contracts of Vectors are also correct for Indefinite_Vectors. The capacity rules and heap usage are essentially similar.]
-----------------------------------------
A.18.19 The Generic Package Containers.Bounded_Vectors
Add after A.18.19(3/3):
* The Global aspect of the package is replaced by
Global => in out null,
AARM Reason: This package is pure, and thus it cannot have or depend upon any other packages that have state. Thus we require no global uses whatsoever.
Add after A.18.19(6/3):
* Capacity is omitted from the Stable_Properties of type Vector.
AARM Reason: The capacity is a discriminant here, so it can't be changed by most routines; thus including it in the stable properties adds no information.
Modify A.18.19(7/3):
In function Copy, [if the Capacity parameter is equal to or greater than the length of Source, the vector capacity exactly equals the value of the Capacity parameter]{the postcondition is altered to:}
Post => Length (Copy'Result) = Length (Source) and then
(if Capacity > Length (Source) then
Copy'Result.Capacity = Capacity
else Copy'Result.Capacity >= Length (Source));
[Note: Reading the discriminant here, not a prefix call.]
Replace A.18.19(9.3) by:
procedure Reserve_Capacity (Container : in out Vector; Capacity : in Count_Type) with Pre => (if Capacity > Container.Capacity then raise Capacity_Error);
This operation has no effect[Redundant: other than checking the precondition].
Add after A.18.19(9/3):
* The portion of the postcondition checking the capacity is omitted from
subprograms Set_Length, Assign, Insert, Insert_Space, Prepend, Append, Delete,
* For procedures Insert, Insert_Space, Prepend, and Append, the part of the
precondition reading:
(if <some length expression> > Index_Type'Last
then raise Constraint_Error)
is replaced by:
(if <some length expression> > Index_Type'Last then raise Constraint_Error) and then (if <some length expression> > Container.Capacity then raise Capacity_Error)
-----------------------------------------
Add after 11.5(23):
Redundant[The following check corresponds to situations in which the exception Assertion_Error is raised upon failure.]
Container_Check
Check the precondition of a routine declared in a child unit of Ada.Containers or in an instance of a generic unit declared in a child unit of Ada.Containers.
AARM Reason: One could use the Assertion_Policy to eliminate such checks, but that would require recompiling the Ada.Containers packages (the assertion policy that determines whether the checks are made is that used to compile the unit). In addition, we do not want to specify the behavior of the Ada.Containers operations if the precondition fails; that is different than the usual behavior of Assertion_Policy. By using Suppress for this purpose, we make it clear that a failed check that is suppressed means erroneous execution.
Modify 11.5(26):
If a given check has been suppressed, and the corresponding error situation occurs, the execution of the program is erroneous. {Similarly, if a precondition check has been suppressed and the evaluation of the precondition would have raised an exception, execution is erroneous.}
AARM Reason: It's unclear that a precondition expression that includes /raise/ Program_Error is an "error situation"; the precondition never actually evaluates to False in that case. Thus, we spell out that case. We only allow suppressing preconditions associated with language-defined units; other preconditions follow the rules of the appropriate Assertion_Policy.
!discussion
For this version, we've prototyped the changes needed for a single package (Ada.Containers.Vectors) and the bounded and indefinite versions thereof. Additional changes will be needed if AI12-0111-1 is approved. [Editor's note: I would want to apply both of these AIs together, since the changes needed are interrelated.]
This version only shows the wording for the main body of the definition of Ada.Containers.Vectors and the start of the package specification. The rest of 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. Also new are versions of a few reading routines that did not take a container parameter. (One routine, Has_Element with a container parameter, is both.) 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.)
There are a few cases where I was able to drop wording when it was specified by the postcondition (mostly where the length or capacity was specified). This follows the policy we adopted earlier when working on the random number package.
We are only including 4 stable properties in the postconditions. These are the Length, Capacity, and tampering state. These should be able to be reasoned about by humans and tools, so there is value in specifying that they are not changed.
We only give explicit postconditions when one of the stable properties is changed by a routine, or when the routine creates a cursor (in those cases, the postcondition asserts that the cursor belongs to the appropriate container).
---
We define a new check name Container_Check for pragma Suppress. As noted in the AARM note, Assertion_Policy is the wrong way to turn off these preconditions. We definitely do not want to require implementations to make duplicate checks in case the precondition isn't evaluated; therefore we need to say that execution is erroneous in case the precondition would have evaluated to False or raised an exception. (It would be nice to say this is just unspecified, with the intent of allowing anything Ada-related to happen, but not allow overwriting memory or the like, but that's a hard concept to define.)
I would have preferred to have this as a global setting for the entire Ada library, but Precondition_Check seems to imply this covers any precondition (which it doesn't). The "correct" name is Language_Defined_Unit_Precondition_Check, which I think the Ada community would clobber us for using.
Therefore, I hit on the idea of naming the check for the first level "grouping" package. Thus, the check names would be Container_Check (as used here), Numerics_Check (for Ada.Numerics), Strings_Check (for Ada.Strings), IO_Check (for the missing Ada.IO package; the packages would have to be listed), and so on. This provides a bit more granularity (although that only matters if we define many more routines with preconditions).
!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