A.18 Containers
This Reference Manual output has not been verified, and may contain omissions or errors. Report any problems on the tracking issue
This clause presents the specifications of the package Containers and several child packages, which provide facilities for storing collections of elements.
A variety of sequence and associative containers are provided. Each container package defines a cursor type as well as a container type. A cursor is a reference to an element within a container. Many operations on cursors are common to all of the containers. A cursor referencing an element in a container is considered to be overlapping only with the element itself.
Some operations of the language-defined child units of Ada.Containers have access-to-subprogram parameters. To ensure such operations are well-defined, they guard against certain actions by the designated subprogram. An action on a container that can add or remove an element is considered to tamper with cursors, and these are prohibited during all such operations. An action on a container that can replace an element with one of a different size is considered to tamper with elements, and these are prohibited during certain of such operations. The details of the specific actions that are considered to tamper with cursors or elements are defined for each child unit of Ada.Containers.
Several of the language-defined child units of Ada.Containers include a nested package named Stable, which provides a view of a container that prohibits any operations that would tamper with elements. By using a Stable view for manipulating a container, the number of tampering checks performed while performing the operations can be reduced. The details of the Stable subpackage are defined separately for each child unit of Ada.Containers that includes such a nested package.
Within this clause we provide O(X). Presuming f is some function of a length parameter N and t(N) is the time the operation takes (on average or worst case, as specified) for the length N, a complexity of O(f(N)) means that there exists a finite A such that for any N, t(N)/f(N) < A.
If the advice suggests that the complexity should be less than O(f(N)), then for any arbitrarily small positive real D, there should exist a positive integer M such that for all N > M, t(N)/f(N) < D.
When a formal function is used to provide an ordering for a container, it is generally required to define a strict weak ordering. A function "<" defines a strict weak ordering if it is irreflexive, asymmetric, transitive, and in addition, if x < y for any values x and y, then for all other values z, (x < z) or (z < y). Elements are in a smallest first order using such an operator if, for every element y with a predecessor x in the order, (y < x) is false.
Language Design Principles
- (Expandable) Vectors of any nonlimited type;
- Doubly-linked Lists of any nonlimited type;
- Hashed Maps keyed by any nonlimited hashable type, and containing any nonlimited type;
- Ordered Maps keyed by any nonlimited ordered type, and containing any nonlimited type;
- Hashed Sets of any nonlimited hashable type;
- Ordered Sets of any nonlimited ordered type;
- Multiway Trees of any nonlimited type;
- Holders of any (indefinite) nonlimited type;
- Synchronized queues of any definite nonlimited type; and
- Priority queues of any definite nonlimited type.
- Library packages must allow concurrent calls – multiple tasks can use the packages as long as they operate on separate containers. Thus, it is only necessary for a user to protect a container if a single container needs to be used by multiple tasks and concurrent calls to operations of the container have overlapping parameters.
- Language-defined types must stream "properly". That means that the stream attributes can be used to implement persistence of containers when necessary, and containers can be passed between partitions of a program.
- Equality of language-defined types must compose “properly”. This means that the version of "=" directly used by users is the same one that will be used in generics and in predefined equality operators of types with components of the containers and/or cursors. This prevents the abstraction from breaking unexpectedly.
- Redispatching is not allowed (unless it is required). That means that overriding a container operation will not change the behavior of any other predefined container operation. This provides a stable base for extensions.
Static Semantics
7/4Certain subprograms declared within instances of some of the generic packages presented in this clause are said to perform indefinite insertion. These subprograms are those corresponding (in the sense of the copying described in subclause 12.3) to subprograms that have formal parameters of a generic formal indefinite type and that are identified as performing indefinite insertion in the subclause defining the generic package.
If a subprogram performs indefinite insertion, then certain run-time checks are performed as part of a call to the subprogram; if any of these checks fail, then the resulting exception is propagated to the caller and the container is not modified by the call. These checks are performed for each parameter corresponding (in the sense of the copying described in 12.3) to a parameter in the corresponding generic whose type is a generic formal indefinite type. The checks performed for a given parameter are those checks explicitly specified in subclause 4.8 that would be performed as part of the evaluation of an initialized allocator whose access type is declared immediately within the instance, where:
- the value of the
qualified_expressionis that of the parameter; and 10/4 - the designated subtype of the access type is the subtype of the parameter; and
- finalization of the collection of the access type has started if and only if the finalization of the instance has started.
Implementation Requirements
12/5For an indefinite container (one whose type is defined in an instance of a child package of Containers whose defining_identifier contains "Indefinite"), each element of the container shall be created when it is inserted into the container and finalized when it is deleted from the container (or when the container object is finalized if the element has not been deleted). For a bounded container (one whose type is defined in an instance of a child package of Containers whose defining_identifier starts with "Bounded") that is not an indefinite container, all of the elements of the capacity of the container shall be created and default initialized when the container object is created; the elements shall be finalized when the container object is finalized. [For other kinds of containers, when elements are created and finalized is unspecified.]
For an instance I of a container package with a container type, the specific type T of the object returned from a function that returns an object of an iterator interface, as well as the primitive operations of T, shall be nonblocking. The Global aspect specified for T and the primitive operations of T shall be (in all, out synchronized) or a specification that allows access to fewer global objects.
Extensions to Ada 95
Wording Changes from Ada 2005
Extensions to Ada 2012
Wording Changes from Ada 2012
A.18.1 The Package Containers
1/2The package Containers is the root of the containers subsystem.
Static Semantics
2/2The library package Containers has the following declaration:
package Ada.Containers
with Pure is
4/2type Hash_Type is mod implementation-defined;
5/2type Count_Type is range 0 .. implementation-defined;
5.1/3Capacity_Error : exception;
6/2end Ada.Containers;
Hash_Type represents the range of the result of a hash function. Count_Type represents the (potential or actual) number of elements of a container.
Capacity_Error is raised when the capacity of a container is exceeded.
Implementation Advice
8/2Hash_Type'Modulus should be at least 2**32. Count_Type'Last should be at least 2**31–1.
Extensions to Ada 95
Incompatibilities With Ada 2005
use_clause, and an entity with the name Capacity_Error is defined in a package that is also referenced in a use_clause, the entity Capacity_Error may no longer be use-visible, resulting in errors. This should be rare and is easily fixed if it does occur. A.18.2 The Generic Package Containers.Vectors
1/2The language-defined generic package Containers.Vectors provides private types Vector and Cursor, and a set of operations for each type. A vector container allows insertion and deletion at any position, but it is specifically optimized for insertion and deletion at the high end (the end with the higher index) of the container. A vector container also provides random access to its elements.
A vector container behaves conceptually as an array that expands as necessary as items are inserted. The length of a vector is the number of elements that the vector contains. The capacity of a vector is the maximum number of elements that can be inserted into the vector prior to it being automatically expanded.
Elements in a vector container can be referred to by an index value of a generic formal type. The first element of a vector always has its index value equal to the lower bound of the formal type.
A vector container may contain empty elements. Empty elements do not have a specified value.
Static Semantics
5/2The generic library package Containers.Vectors has the following declaration:
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, Global => in out synchronized is
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,
Iterator_View => Stable.Vector,
Aggregate => (Empty => Empty,
Add_Unnamed => Append,
New_Indexed => New_Vector,
Assign_Indexed => Replace_Element),
Stable_Properties => (Length, Capacity,
Tampering_With_Cursors_Prohibited,
Tampering_With_Elements_Prohibited),
Default_Initial_Condition =>
Length (Vector) = 0 and then
(not Tampering_With_Cursors_Prohibited (Vector)) and then
(not Tampering_With_Elements_Prohibited (Vector)),
Preelaborable_Initialization ;
9/5type Cursor is private
with Preelaborable_Initialization ;
10/2Empty_Vector : constant Vector;
11/2No_Element : constant Cursor;
11.1/5function Has_Element (Position : Cursor) return Boolean
with Nonblocking, Global => in all, Use_Formal => null;
function Has_Element (Container : Vector; Position : Cursor)
return Boolean
with Nonblocking, Global => null, Use_Formal => null;
package Vector_Iterator_Interfaces is new
Ada.Iterator_Interfaces (Cursor, Has_Element);
12/2function "=" (Left, Right : Vector) return Boolean;
12.1/5function Tampering_With_Cursors_Prohibited
(Container : Vector) return Boolean
with Nonblocking, Global => null, Use_Formal => null;
12.2/5function Tampering_With_Elements_Prohibited
(Container : Vector) return Boolean
with Nonblocking, Global => null, Use_Formal => null;
12.3/5function Maximum_Length return Count_Type
with Nonblocking, Global => null, Use_Formal => null;
12.4/5function Empty (Capacity : Count_Type := implementation-defined)
return Vector
with Pre => Capacity <= Maximum_Length
or else raise Constraint_Error,
Post =>
Capacity (Empty'Result) >= Capacity and then
not Tampering_With_Elements_Prohibited (Empty'Result) and then
not Tampering_With_Cursors_Prohibited (Empty'Result) and then
Length (Empty'Result) = 0;
13/5function To_Vector (Length : Count_Type) return Vector
with Pre => Length <= Maximum_Length or else raise Constraint_Error,
Post =>
To_Vector'Result.Length = Length and then
not Tampering_With_Elements_Prohibited (To_Vector'Result)
and then
not Tampering_With_Cursors_Prohibited (To_Vector'Result)
and then
To_Vector'Result.Capacity >= Length;
14/5function To_Vector
(New_Item : Element_Type;
Length : Count_Type) return Vector
with Pre => Length <= Maximum_Length or else raise Constraint_Error,
Post =>
To_Vector'Result.Length = Length and then
not Tampering_With_Elements_Prohibited (To_Vector'Result)
and then
not Tampering_With_Cursors_Prohibited (To_Vector'Result)
and then
To_Vector'Result.Capacity >= Length;
14.1/5function New_Vector (First, Last : Index_Type) return Vector is
(To_Vector (Count_Type (Last - First + 1)))
with Pre => First = Index_Type'First;
15/5function "&" (Left, Right : Vector) return Vector
with Pre => Length (Left) <= Maximum_Length - Length (Right)
or else raise Constraint_Error,
Post => Length (Vectors."&"'Result) =
Length (Left) + Length (Right) and then
not Tampering_With_Elements_Prohibited
(Vectors."&"'Result) and then
not Tampering_With_Cursors_Prohibited
(Vectors."&"'Result) and then
Vectors."&"'Result.Capacity >=
Length (Left) + Length (Right);
16/5function "&" (Left : Vector;
Right : Element_Type) return Vector
with Pre => Length (Left) <= Maximum_Length - 1
or else raise Constraint_Error,
Post => Vectors."&"'Result.Length = Length (Left) + 1 and then
not Tampering_With_Elements_Prohibited
(Vectors."&"'Result) and then
not Tampering_With_Cursors_Prohibited
(Vectors."&"'Result) and then
Vectors."&"'Result.Capacity >= Length (Left) + 1;
17/5function "&" (Left : Element_Type;
Right : Vector) return Vector
with Pre => Length (Right) <= Maximum_Length - 1
or else raise Constraint_Error,
Post => Length (Vectors."&"'Result) = Length (Right) + 1 and then
not Tampering_With_Elements_Prohibited
(Vectors."&"'Result) and then
not Tampering_With_Cursors_Prohibited
(Vectors."&"'Result) and then
Vectors."&"'Result.Capacity >= Length (Right) + 1;
18/5function "&" (Left, Right : Element_Type) return Vector
with Pre => Maximum_Length >= 2 or else raise Constraint_Error,
Post => Length ("&"'Result) = 2 and then
not Tampering_With_Elements_Prohibited
(Vectors."&"'Result) and then
not Tampering_With_Cursors_Prohibited
(Vectors."&"'Result) and then
Vectors."&"'Result.Capacity >= 2;
19/5function Capacity (Container : Vector) return Count_Type
with Nonblocking, Global => null, Use_Formal => null;
20/5procedure Reserve_Capacity (Container : in out Vector;
Capacity : in Count_Type)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Container.Capacity >= Capacity;
21/5function Length (Container : Vector) return Count_Type
with Nonblocking, Global => null, Use_Formal => null;
22/5procedure Set_Length (Container : in out Vector;
Length : in Count_Type)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Length <= Maximum_Length
or else raise Constraint_Error),
Post => Container.Length = Length and then
Capacity (Container) >= Length;
23/5function Is_Empty (Container : Vector) return Boolean
with Nonblocking, Global => null, Use_Formal => null,
Post => Is_Empty'Result = (Length (Container) = 0);
24/5procedure Clear (Container : in out Vector)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Length (Container) = 0;
25/5function 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, Global => null, Use_Formal => null;
26/5function To_Index (Position : Cursor) return Extended_Index
with Nonblocking, Global => in all;
26.1/5function To_Index (Container : Vector;
Position : Cursor) return Extended_Index
with Pre => Position = No_Element or else
Has_Element (Container, Position) or else
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, Global => null, Use_Formal => null;
27/5function Element (Container : Vector;
Index : Index_Type)
return Element_Type
with Pre => Index in
First_Index (Container) .. Last_Index (Container)
or else raise Constraint_Error,
Nonblocking, Global => null, Use_Formal => Element_Type;
function Element (Position : Cursor) return Element_Type
with Pre => Position /= No_Element or else raise Constraint_Error,
Nonblocking, Global => in all, Use_Formal => Element_Type;
28.1/5function Element (Container : Vector;
Position : Cursor) return Element_Type
with Pre => (Position /= No_Element or else
raise Constraint_Error) and then
(Has_Element (Container, Position)
or else raise Program_Error),
Nonblocking, Global => null, Use_Formal => Element_Type;
29/5procedure Replace_Element (Container : in out Vector;
Index : in Index_Type;
New_Item : in Element_Type)
with Pre => (not Tampering_With_Elements_Prohibited (Container)
or else raise Program_Error) and then
(Index in
First_Index (Container) .. Last_Index (Container)
or else raise Constraint_Error);
30/5procedure Replace_Element (Container : in out Vector;
Position : in Cursor;
New_item : in Element_Type)
with Pre => (not Tampering_With_Elements_Prohibited (Container)
or else raise Program_Error) and then
(Position /= No_Element
or else raise Constraint_Error) and then
(Has_Element (Container, Position)
or else raise Program_Error);
31/5procedure Query_Element
(Container : in Vector;
Index : in Index_Type;
Process : not null access procedure (Element : in Element_Type))
with Pre => Index in
First_Index (Container) .. Last_Index (Container)
or else raise Constraint_Error;
32/5procedure Query_Element
(Position : in Cursor;
Process : not null access procedure (Element : in Element_Type))
with Pre => Position /= No_Element or else raise Constraint_Error,
Global => in all;
32.1/5procedure Query_Element
(Container : in Vector;
Position : in Cursor;
Process : not null access procedure (Element : in Element_Type))
with Pre => (Position /= No_Element
or else raise Constraint_Error) and then
(Has_Element (Container, Position)
or else raise Program_Error);
33/5procedure Update_Element
(Container : in out Vector;
Index : in Index_Type;
Process : not null access procedure
(Element : in out Element_Type))
with Pre => Index in
First_Index (Container) .. Last_Index (Container)
or else raise Constraint_Error;
34/5procedure Update_Element
(Container : in out Vector;
Position : in Cursor;
Process : not null access procedure
(Element : in out Element_Type))
with Pre => (Position /= No_Element
or else raise Constraint_Error) and then
(Has_Element (Container, Position)
or else raise Program_Error);
34.1/5type Constant_Reference_Type
(Element : not null access constant Element_Type) is private
with Implicit_Dereference => Element,
Nonblocking, Global => in out synchronized,
Default_Initial_Condition => (raise Program_Error);
type Reference_Type (Element : not null access Element_Type) is private
with Implicit_Dereference => Element,
Nonblocking, Global => in out synchronized,
Default_Initial_Condition => (raise Program_Error);
34.3/5function Constant_Reference (Container : aliased in Vector;
Index : in Index_Type)
return Constant_Reference_Type
with Pre => Index in
First_Index (Container) .. Last_Index (Container)
or else raise Constraint_Error,
Post => Tampering_With_Cursors_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
34.4/5function Reference (Container : aliased in out Vector;
Index : in Index_Type)
return Reference_Type
with Pre => Index in
First_Index (Container) .. Last_Index (Container)
or else raise Constraint_Error,
Post => Tampering_With_Cursors_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
34.5/5function Constant_Reference (Container : aliased in Vector;
Position : in Cursor)
return Constant_Reference_Type
with Pre => (Position /= No_Element
or else raise Constraint_Error) and then
(Has_Element (Container, Position)
or else raise Program_Error),
Post => Tampering_With_Cursors_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
34.6/5function Reference (Container : aliased in out Vector;
Position : in Cursor)
return Reference_Type
with Pre => (Position /= No_Element
or else raise Constraint_Error) and then
(Has_Element (Container, Position)
or else raise Program_Error),
Post => Tampering_With_Cursors_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
34.7/5procedure Assign (Target : in out Vector; Source : in Vector)
with Pre => not Tampering_With_Cursors_Prohibited (Target)
or else raise Program_Error,
Post => Length (Source) = Length (Target) and then
Capacity (Target) >= Length (Target);
34.8/5function Copy (Source : Vector; Capacity : Count_Type := 0)
return Vector
with Pre => Capacity = 0 or else Capacity >= Length (Source)
or else raise Capacity_Error,
Post => Length (Copy'Result) = Length (Source) and then
not Tampering_With_Elements_Prohibited (Copy'Result)
and then
not Tampering_With_Cursors_Prohibited (Copy'Result)
and then
Copy'Result.Capacity >= (if Capacity = 0 then
Length (Source) else Capacity);
35/5procedure Move (Target : in out Vector;
Source : in out Vector)
with Pre => (not Tampering_With_Cursors_Prohibited (Target)
or else raise Program_Error) and then
(not Tampering_With_Cursors_Prohibited (Source)
or else raise Program_Error),
Post => (if not Target'Has_Same_Storage (Source) then
Length (Target) = Length (Source)'Old and then
Length (Source) = 0 and then
Capacity (Target) >= Length (Source)'Old);
36/5procedure Insert_Vector (Container : in out Vector;
Before : in Extended_Index;
New_Item : in Vector)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before in
First_Index (Container) .. Last_Index (Container) + 1
or else raise Constraint_Error) and then
(Length (Container) <= Maximum_Length - Length (New_Item)
or else raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) and then
Capacity (Container) >= Length (Container);
37/5procedure Insert_Vector (Container : in out Vector;
Before : in Cursor;
New_Item : in Vector)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before = No_Element or else
Has_Element (Container, Before)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Length (New_Item)
or else raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) and then
Capacity (Container) >= Length (Container);
38/5procedure Insert_Vector (Container : in out Vector;
Before : in Cursor;
New_Item : in Vector;
Position : out Cursor)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before = No_Element or else
Has_Element (Container, Before)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Length (New_Item)
or else raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) and then
Has_Element (Container, Position) and then
Capacity (Container) >= Length (Container);
39/5procedure Insert (Container : in out Vector;
Before : in Extended_Index;
New_Item : in Element_Type;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before in
First_Index (Container) .. Last_Index (Container) + 1
or else raise Constraint_Error) and then
(Length (Container) <= Maximum_Length - Count
or else raise Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) and then
Capacity (Container) >= Length (Container);
40/5procedure Insert (Container : in out Vector;
Before : in Cursor;
New_Item : in Element_Type;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before = No_Element or else
Has_Element (Container, Before)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Count
or else raise Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) and then
Capacity (Container) >= Length (Container);
41/5procedure Insert (Container : in out Vector;
Before : in Cursor;
New_Item : in Element_Type;
Position : out Cursor;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before = No_Element or else
Has_Element (Container, Before)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Count
or else raise Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) and then
Has_Element (Container, Position) and then
Capacity (Container) >= Length (Container);
42/5procedure Insert (Container : in out Vector;
Before : in Extended_Index;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before in
First_Index (Container) .. Last_Index (Container) + 1
or else raise Constraint_Error) and then
(Length (Container) <= Maximum_Length - Count
or else raise Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) and then
Capacity (Container) >= Length (Container);
43/5procedure Insert (Container : in out Vector;
Before : in Cursor;
Position : out Cursor;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before = No_Element or else
Has_Element (Container, Before)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Count
or else raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container)
and then Has_Element (Container, Position) and then
Capacity (Container) >= Length (Container);
44/5procedure Prepend_Vector (Container : in out Vector;
New_Item : in Vector)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Length (New_Item)
or else raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) and then
Capacity (Container) >= Length (Container);
45/5procedure Prepend (Container : in out Vector;
New_Item : in Element_Type;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Count
or else raise Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) and then
Capacity (Container) >= Length (Container);
46/5procedure Append_Vector (Container : in out Vector;
New_Item : in Vector)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Length (New_Item)
or else raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) and then
Capacity (Container) >= Length (Container);
47/5procedure Append (Container : in out Vector;
New_Item : in Element_Type;
Count : in Count_Type )
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Count
or else raise Constraint_Error),
Post =>
Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
47.1/5procedure Append (Container : in out Vector;
New_Item : in Element_Type)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - 1
or else raise Constraint_Error),
Post => Length (Container)'Old + 1 = Length (Container) and then
Capacity (Container) >= Length (Container);
48/5procedure Insert_Space (Container : in out Vector;
Before : in Extended_Index;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before in
First_Index (Container) .. Last_Index (Container) + 1
or else raise Constraint_Error) and then
(Length (Container) <= Maximum_Length - Count
or else raise Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) and then
Capacity (Container) >= Length (Container);
49/5procedure Insert_Space (Container : in out Vector;
Before : in Cursor;
Position : out Cursor;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before = No_Element or else
Has_Element (Container, Before)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Count
or else raise Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) and then
Has_Element (Container, Position) and then
Capacity (Container) >= Length (Container);
50/5procedure Delete (Container : in out Vector;
Index : in Extended_Index;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Index in
First_Index (Container) .. Last_Index (Container) + 1
or else raise Constraint_Error),
Post => Length (Container)'Old - Count <=
Length (Container);
51/5procedure Delete (Container : in out Vector;
Position : in out Cursor;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Position /= No_Element
or else raise Constraint_Error) and then
(Has_Element (Container, Position)
or else raise Program_Error),
Post => Length (Container)'Old - Count <=
Length (Container) and then
Position = No_Element;
52/5procedure Delete_First (Container : in out Vector;
Count : in Count_Type := 1)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Length (Container)'Old - Count <= Length (Container);
53/5procedure Delete_Last (Container : in out Vector;
Count : in Count_Type := 1)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Length (Container)'Old - Count <= Length (Container);
54/5procedure Reverse_Elements (Container : in out Vector)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error;
55/5procedure Swap (Container : in out Vector;
I, J : in Index_Type)
with Pre => (not Tampering_With_Elements_Prohibited (Container)
or else raise Program_Error) and then
(I in First_Index (Container) .. Last_Index (Container)
or else raise Constraint_Error) and then
(J in First_Index (Container) .. Last_Index (Container)
or else raise Constraint_Error);
56/5procedure Swap (Container : in out Vector;
I, J : in Cursor)
with Pre => (not Tampering_With_Elements_Prohibited (Container)
or else raise Program_Error) and then
(I /= No_Element or else Constraint_Error) and then
(J /= No_Element or else Constraint_Error) and then
(Has_Element (Container, I)
or else raise Program_Error) and then
(Has_Element (Container, J)
or else raise Program_Error);
57/5function First_Index (Container : Vector) return Index_Type
with Nonblocking, Global => null, Use_Formal => null,
Post => First_Index'Result = Index_Type'First;
58/5function First (Container : Vector) return Cursor
with Nonblocking, Global => null, Use_Formal => null,
Post => (if not Is_Empty (Container)
then Has_Element (Container, First'Result)
else First'Result = No_Element);
59/5function First_Element (Container : Vector)
return Element_Type
with Pre => (not Is_Empty (Container)
or else raise Constraint_Error);
60/5function Last_Index (Container : Vector) return Extended_Index
with Nonblocking, Global => null, Use_Formal => null,
Post => (if Length (Container) = 0
then Last_Index'Result = No_Index
else Count_Type(Last_Index'Result - Index_Type'First) =
Length (Container) - 1);
61/5function Last (Container : Vector) return Cursor
with Nonblocking, Global => null, Use_Formal => null,
Post => (if not Is_Empty (Container)
then Has_Element (Container, Last'Result)
else Last'Result = No_Element);
62/5function Last_Element (Container : Vector)
return Element_Type
with Pre => (not Is_Empty (Container)
or else raise Constraint_Error);
63/5function Next (Position : Cursor) return Cursor
with Nonblocking, Global => in all, Use_Formal => null,
Post => (if Position = No_Element then Next'Result = No_Element);
63.1/5function Next (Container : Vector; Position : Cursor) return Cursor
with Nonblocking, Global => null, Use_Formal => null,
Pre => Position = No_Element or else
Has_Element (Container, Position)
or else raise Program_Error,
Post => (if Position = No_Element then Next'Result = No_Element
elsif Has_Element (Container, Next'Result) then
To_Index (Container, Next'Result) =
To_Index (Container, Position) + 1
elsif Next'Result = No_Element then
Position = Last (Container)
else False);
64/5procedure Next (Position : in out Cursor)
with Nonblocking, Global => in all, Use_Formal => null;
64.1/5procedure Next (Container : in Vector;
Position : in out Cursor)
with Nonblocking, Global => null, Use_Formal => null,
Pre => Position = No_Element or else
Has_Element (Container, Position)
or else raise Program_Error,
Post => (if Position /= No_Element
then Has_Element (Container, Position));
65/5function Previous (Position : Cursor) return Cursor
with Nonblocking, Global => in all, Use_Formal => null,
Post => (if Position = No_Element
then Previous'Result = No_Element);
65.1/5function Previous (Container : Vector;
Position : Cursor) return Cursor
with Nonblocking, Global => null, Use_Formal => null,
Pre => Position = No_Element or else
Has_Element (Container, Position)
or else raise Program_Error,
Post => (if Position = No_Element
then Previous'Result = No_Element
elsif Has_Element (Container, Previous'Result) then
To_Index (Container, Previous'Result) =
To_Index (Container, Position) - 1
elsif Previous'Result = No_Element then
Position = First (Container)
else False);
66/5procedure Previous (Position : in out Cursor)
with Nonblocking, Global => in all, Use_Formal => null;
66.1/5procedure Previous (Container : in Vector;
Position : in out Cursor)
with Nonblocking, Global => null, Use_Formal => null,
Pre => Position = No_Element or else
Has_Element (Container, Position)
or else raise Program_Error,
Post => (if Position /= No_Element
then Has_Element (Container, Position));
67/2function Find_Index (Container : Vector;
Item : Element_Type;
Index : Index_Type := Index_Type'First)
return Extended_Index;
68/5function Find (Container : Vector;
Item : Element_Type;
Position : Cursor := No_Element)
return Cursor
with Pre => Position = No_Element or else
Has_Element (Container, Position)
or else raise Program_Error,
Post => (if Find'Result /= No_Element
then Has_Element (Container, Find'Result));
69/2function Reverse_Find_Index (Container : Vector;
Item : Element_Type;
Index : Index_Type := Index_Type'Last)
return Extended_Index;
70/5function Reverse_Find (Container : Vector;
Item : Element_Type;
Position : Cursor := No_Element)
return Cursor
with Pre => Position = No_Element or else
Has_Element (Container, Position)
or else raise Program_Error,
Post => (if Reverse_Find'Result /= No_Element
then Has_Element (Container, Reverse_Find'Result));
71/2function Contains (Container : Vector;
Item : Element_Type) return Boolean;
72/3This paragraph was deleted.
73/5procedure Iterate
(Container : in Vector;
Process : not null access procedure (Position : in Cursor))
with Allows_Exit;
74/5procedure Reverse_Iterate
(Container : in Vector;
Process : not null access procedure (Position : in Cursor))
with Allows_Exit;
74.1/5function Iterate (Container : in Vector)
return Vector_Iterator_Interfaces.Parallel_Reversible_Iterator 'Class
with Post => Tampering_With_Cursors_Prohibited (Container);
74.2/5function Iterate (Container : in Vector; Start : in Cursor)
return Vector_Iterator_Interfaces.Reversible_Iterator'Class
with Pre => (Start /= No_Element
or else raise Constraint_Error) and then
(Has_Element (Container, Start)
or else raise Program_Error),
Post => Tampering_With_Cursors_Prohibited (Container);
75/5generic
with function "<" (Left, Right : Element_Type)
return Boolean is <>;
package Generic_Sorting
with Nonblocking, Global => null is
76/2function Is_Sorted (Container : Vector) return Boolean;
77/5procedure Sort (Container : in out Vector)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error;
78/5procedure Merge (Target : in out Vector;
Source : in out Vector)
with Pre => (not Tampering_With_Cursors_Prohibited (Target)
or else raise Program_Error) and then
(not Tampering_With_Cursors_Prohibited (Source)
or else raise Program_Error) and then
(Length (Target) <= Maximum_Length - Length (Source)
or else raise Constraint_Error) and then
((Length (Source) = 0 or else
not Target'Has_Same_Storage (Source))
or else raise Program_Error),
Post => (declare
Result_Length : constant Count_Type :=
Length (Source)'Old + Length (Target)'Old;
begin
(Length (Source) = 0 and then
Length (Target) = Result_Length and then
Capacity (Target) >= Result_Length));
79/2end Generic_Sorting;
79.1/5package Stable is
79.2/5type Vector (Base : not null access Vectors.Vector) is
tagged limited private
with Constant_Indexing => Constant_Reference,
Variable_Indexing => Reference,
Default_Iterator => Iterate,
Iterator_Element => Element_Type,
Stable_Properties => (Length, Capacity),
Global => null,
Default_Initial_Condition => Length (Vector) = 0,
Preelaborable_Initialization;
type Cursor is private
with Preelaborable_Initialization;
79.4/5Empty_Vector : constant Vector;
79.5/5No_Element : constant Cursor;
79.6/5function Has_Element (Position : Cursor) return Boolean
with Nonblocking, Global => in all, Use_Formal => null;
79.7/5package Vector_Iterator_Interfaces is new
Ada.Iterator_Interfaces (Cursor, Has_Element);
79.8/5procedure Assign (Target : in out Vectors.Vector;
Source : in Vector)
with Post => Length (Source) = Length (Target) and then
Capacity (Target) >= Length (Target);
79.9/5function Copy (Source : Vectors.Vector) return Vector
with Post => Length (Copy'Result) = Length (Source);
79.10/5type Constant_Reference_Type
(Element : not null access constant Element_Type) is private
with Implicit_Dereference => Element,
Nonblocking, Global => null, Use_Formal => null,
Default_Initial_Condition => (raise Program_Error);
79.11/5type Reference_Type
(Element : not null access Element_Type) is private
with Implicit_Dereference => Element,
Nonblocking, Global => null, Use_Formal => null,
Default_Initial_Condition => (raise Program_Error);
79.12/5-- Additional subprograms as described in the text
-- are declared here.
79.13/5private
79.14/5... -- not specified by the language
79.15/5end Stable;
80/2private
81/2... -- not specified by the language
82/2end Ada.Containers.Vectors;
The actual function for the generic formal function "=" on Element_Type values is expected to define a reflexive and symmetric relationship and return the same result value each time it is called with a particular pair of values. If it behaves in some other manner, the functions defined to use it return an unspecified value. The exact arguments and number of calls of this generic formal function by the functions defined to use it are unspecified.
The type Vector is used to represent vectors. The type Vector needs finalization (see 7.6).
Empty_Vector represents the empty vector object. It has a length of 0. If an object of type Vector is not otherwise initialized, it is initialized to the same value as Empty_Vector.
No_Element represents a cursor that designates no element. If an object of type Cursor is not otherwise initialized, it is initialized to the same value as No_Element.
The primitive "=" operator for type Cursor returns True if both cursors are No_Element, or designate the same element in the same container.
Execution of the default implementation of the Input, Output, Read, or Write attribute of type Cursor raises Program_Error.
Vector'Write for a Vector object V writes Length(V) elements of the vector to the stream. It may also write additional information about the vector.
Vector'Read reads the representation of a vector from the stream, and assigns to Item a vector with the same length and elements as was written by Vector'Write.
No_Index represents a position that does not correspond to any element. The subtype Extended_Index includes the indices covered by Index_Type plus the value No_Index and, if it exists, the successor to the Index_Type'Last.
[Some operations check for “tampering with cursors” of a container because they depend on the set of elements of the container remaining constant, and others check for “tampering with elements” of a container because they depend on elements of the container not being replaced.] When tampering with cursors is prohibited for a particular vector object V, Program_Error is propagated by the finalization of V[, as well as by a call that passes V to certain of the operations of this package, as indicated by the precondition of such an operation]. Similarly, when tampering with elements is prohibited for V, Program_Error is propagated by a call that passes V to certain of the other operations of this package, as indicated by the precondition of such an operation.
Paragraphs 91 through 97 are removed as preconditions now describe these rules.
assignment_statement, because that finalizes the target object as part of the operation, and finalization of an object is already defined as tampering with cursors.
function Has_Element (Position : Cursor) return Boolean
with Nonblocking, Global => in all, Use_Formal => null;
Returns True if Position designates an element, and returns False otherwise.
function Has_Element (Container : Vector; Position : Cursor)
return Boolean
with Nonblocking, Global => null, Use_Formal => null;
Returns True if Position designates an element in Container, and returns False otherwise.
function "=" (Left, Right : Vector) return Boolean;
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.
function Tampering_With_Cursors_Prohibited
(Container : Vector) return Boolean
with Nonblocking, Global => null, Use_Formal => null;
Returns True if tampering with cursors or tampering with elements is currently prohibited for Container, and returns False otherwise.
function Tampering_With_Elements_Prohibited
(Container : Vector) return Boolean
with Nonblocking, Global => null, Use_Formal => null;
Always returns False[, regardless of whether tampering with elements is prohibited].
function Maximum_Length return Count_Type
with Nonblocking, Global => null, Use_Formal => null;
Returns the maximum Length of a Vector, based on the index type.
Count_Type (Index_Type'Last - Index_Type'First + 1)
function Empty (Capacity : Count_Type := implementation-defined)
return Vector
with Pre => Capacity <= Maximum_Length
or else raise Constraint_Error,
Post =>
Capacity (Empty'Result) >= Capacity and then
not Tampering_With_Elements_Prohibited (Empty'Result) and then
not Tampering_With_Cursors_Prohibited (Empty'Result) and then
Length (Empty'Result) = 0;
Returns an empty vector.
function To_Vector (Length : Count_Type) return Vector
with Pre => Length <= Maximum_Length or else raise Constraint_Error,
Post =>
To_Vector'Result.Length = Length and then
not Tampering_With_Elements_Prohibited (To_Vector'Result)
and then
not Tampering_With_Cursors_Prohibited (To_Vector'Result)
and then
To_Vector'Result.Capacity >= Length;
Returns a vector with a length of Length, filled with empty elements.
function To_Vector
(New_Item : Element_Type;
Length : Count_Type) return Vector
with Pre => Length <= Maximum_Length or else raise Constraint_Error,
Post =>
To_Vector'Result.Length = Length and then
not Tampering_With_Elements_Prohibited (To_Vector'Result)
and then
not Tampering_With_Cursors_Prohibited (To_Vector'Result)
and then
To_Vector'Result.Capacity >= Length;
Returns a vector with a length of Length, filled with elements initialized to the value New_Item.
function "&" (Left, Right : Vector) return Vector
with Pre => Length (Left) <= Maximum_Length - Length (Right)
or else raise Constraint_Error,
Post => Length (Vectors."&"'Result) =
Length (Left) + Length (Right) and then
not Tampering_With_Elements_Prohibited (Vectors."&"'Result)
and then
not Tampering_With_Cursors_Prohibited (Vectors."&"'Result)
and then
Vectors."&"'Result.Capacity >=
Length (Left) + Length (Right);
Returns a vector comprising the elements of Left followed by the elements of Right.
function "&" (Left : Vector;
Right : Element_Type) return Vector
with Pre => Length (Left) <= Maximum_Length - 1
or else raise Constraint_Error,
Post => Vectors."&"'Result.Length = Length (Left) + 1 and then
not Tampering_With_Elements_Prohibited (Vectors."&"'Result)
and then
not Tampering_With_Cursors_Prohibited (Vectors."&"'Result)
and then
Vectors."&"'Result.Capacity >= Length (Left) + 1;
Returns a vector comprising the elements of Left followed by the element Right.
function "&" (Left : Element_Type;
Right : Vector) return Vector
with Pre => Length (Right) <= Maximum_Length - 1
or else raise Constraint_Error,
Post => Length (Vectors."&"'Result) = Length (Right) + 1 and then
not Tampering_With_Elements_Prohibited (Vectors."&"'Result)
and then
not Tampering_With_Cursors_Prohibited (Vectors."&"'Result)
and then
Vectors."&"'Result.Capacity >= Length (Right) + 1;
Returns a vector comprising the element Left followed by the elements of Right.
function "&" (Left, Right : Element_Type) return Vector
with Pre => Maximum_Length >= 2 or else raise Constraint_Error,
Post => Length ("&"'Result) = 2 and then
not Tampering_With_Elements_Prohibited (Vectors."&"'Result)
and then
not Tampering_With_Cursors_Prohibited (Vectors."&"'Result)
and then
Vectors."&"'Result.Capacity >= 2;
Returns a vector comprising the element Left followed by the element Right.
function Capacity (Container : Vector) return Count_Type
with Nonblocking, Global => null, Use_Formal => null;
Returns the capacity of Container.
procedure Reserve_Capacity (Container : in out Vector;
Capacity : in Count_Type)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Container.Capacity >= Capacity;
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.
function Length (Container : Vector) return Count_Type
with Nonblocking, Global => null, Use_Formal => null;
Returns the number of elements in Container.
procedure Set_Length (Container : in out Vector;
Length : in Count_Type)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Length <= Maximum_Length or else raise Constraint_Error),
Post => Container.Length = Length and then
Capacity (Container) >= Length;
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.
function Is_Empty (Container : Vector) return Boolean
with Nonblocking, Global => null, Use_Formal => null,
Post => Is_Empty'Result = (Length (Container) = 0);
Returns True if Container is empty .
procedure Clear (Container : in out Vector)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Length (Container) = 0;
Removes all the elements from Container. The capacity of Container does not change.
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, Global => null, Use_Formal => null;
Returns a cursor designating the element at position Index in Container; returns No_Element if Index does not designate an element . 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)].
function To_Index (Position : Cursor) return Extended_Index
with Nonblocking, Global => in all, Use_Formal => null;
If Position is No_Element, No_Index is returned. Otherwise, the index (within its containing vector) of the element designated by Position is returned.
function To_Index (Container : Vector;
Position : Cursor) return Extended_Index
with Pre => Position = No_Element or else
Has_Element (Container, Position) or else
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, Global => null, Use_Formal => null;
Returns the index (within Container) of the element designated by Position; returns No_Index if Position does not designate an element. For the purposes of determining whether the parameters overlap in a call to To_Index, the Container parameter is not considered to overlap with any object [(including itself)].
function Element (Container : Vector;
Index : Index_Type)
return Element_Type
with Pre => Index in First_Index (Container) .. Last_Index (Container)
or else raise Constraint_Error,
Nonblocking, Global => null, Use_Formal => Element_Type;
Element returns the element at position Index.
function Element (Position : Cursor) return Element_Type
with Pre => Position /= No_Element or else raise Constraint_Error,
Nonblocking, Global => in all, Use_Formal => Element_Type;
Element returns the element designated by Position.
function Element (Container : Vector;
Position : Cursor) return Element_Type
with Pre => (Position /= No_Element
or else raise Constraint_Error) and then
(Has_Element (Container, Position)
or else raise Program_Error),
Nonblocking, Global => null, Use_Formal => Element_Type;
Element returns the element designated by Position in Container.
procedure Replace_Element (Container : in out Vector;
Index : in Index_Type;
New_Item : in Element_Type)
with Pre => (not Tampering_With_Elements_Prohibited (Container)
or else raise Program_Error) and then
(Index in First_Index (Container) .. Last_Index (Container)
or else raise Constraint_Error);
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.
procedure Replace_Element (Container : in out Vector;
Position : in Cursor;
New_Item : in Element_Type)
with Pre => (not Tampering_With_Elements_Prohibited (Container)
or else raise Program_Error) and then
(Position /= No_Element
or else raise Constraint_Error) and then
(Has_Element (Container, Position)
or else raise Program_Error);
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)].
procedure Query_Element
(Container : in Vector;
Index : in Index_Type;
Process : not null access procedure (Element : in Element_Type))
with Pre => Index in First_Index (Container) .. Last_Index (Container)
or else raise Constraint_Error;
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.
procedure Query_Element
(Position : in Cursor;
Process : not null access procedure (Element : in Element_Type))
with Pre => Position /= No_Element or else raise Constraint_Error
Global => in all;
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.
procedure Query_Element
(Container : in Vector;
Position : in Cursor;
Process : not null access procedure (Element : in Element_Type))
with Pre => (Position /= No_Element
or else raise Constraint_Error) and then
(Has_Element (Container, Position)
or else raise Program_Error);
Query_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.
procedure Update_Element
(Container : in out Vector;
Index : in Index_Type;
Process : not null access procedure
(Element : in out Element_Type))
with Pre => Index in First_Index (Container) .. Last_Index (Container)
or else raise Constraint_Error;
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.
If Element_Type is unconstrained and definite, then the actual Element parameter of Process.all shall be unconstrained.
The element at position Index is not an empty element after successful completion of this operation.
procedure Update_Element
(Container : in out Vector;
Position : in Cursor;
Process : not null access procedure
(Element : in out Element_Type))
with Pre => (Position /= No_Element
or else raise Constraint_Error) and then
(Has_Element (Container, Position)
or else raise Program_Error);
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.
If Element_Type is unconstrained and definite, then the actual Element parameter of Process.all shall be unconstrained.
The element designated by Position is not an empty element after successful completion of this operation.
type Constant_Reference_Type
(Element : not null access constant Element_Type) is private
with Implicit_Dereference => Element,
Nonblocking, Global => in out synchronized,
Default_Initial_Condition => (raise Program_Error);
147.2/5type Reference_Type (Element : not null access Element_Type) is private
with Implicit_Dereference => Element,
Nonblocking, Global => in out synchronized,
Default_Initial_Condition => (raise Program_Error);
The types Constant_Reference_Type and Reference_Type need finalization.
This paragraph was deleted.
function Constant_Reference (Container : aliased in Vector;
Index : in Index_Type)
return Constant_Reference_Type
with Pre => Index in First_Index (Container) .. Last_Index (Container)
or else raise Constraint_Error,
Post => Tampering_With_Cursors_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
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.
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.
function Reference (Container : aliased in out Vector;
Index : in Index_Type)
return Reference_Type
with Pre => Index in First_Index (Container) .. Last_Index (Container)
or else raise Constraint_Error,
Post => Tampering_With_Cursors_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
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.
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.
The element at position Index is not an empty element after successful completion of this operation.
function Constant_Reference (Container : aliased in Vector;
Position : in Cursor)
return Constant_Reference_Type
with Pre => (Position /= No_Element
or else raise Constraint_Error) and then
(Has_Element (Container, Position)
or else raise Program_Error),
Post => Tampering_With_Cursors_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
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.
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.
function Reference (Container : aliased in out Vector;
Position : in Cursor)
return Reference_Type
with Pre => (Position /= No_Element
or else raise Constraint_Error) and then
(Has_Element (Container, Position)
or else raise Program_Error),
Post => Tampering_With_Cursors_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
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.
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.
The element designated by Position is not an empty element after successful completion of this operation.
procedure Assign (Target : in out Vector; Source : in Vector)
with Pre => not Tampering_With_Cursors_Prohibited (Target)
or else raise Program_Error,
Post => Length (Source) = Length (Target) and then
Capacity (Target) >= Length (Target);
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).
function Copy (Source : Vector; Capacity : Count_Type := 0)
return Vector
with Pre => Capacity = 0 or else Capacity >= Length (Source)
or else raise Capacity_Error,
Post => Length (Copy'Result) = Length (Source) and then
not Tampering_With_Elements_Prohibited (Copy'Result)
and then
not Tampering_With_Cursors_Prohibited (Copy'Result)
and then
Copy'Result.Capacity >= (if Capacity = 0 then
Length (Source) else Capacity);
Returns a vector whose elements are initialized from the corresponding elements of Source.
procedure Move (Target : in out Vector;
Source : in out Vector)
with Pre => (not Tampering_With_Cursors_Prohibited (Target)
or else raise Program_Error) and then
(not Tampering_With_Cursors_Prohibited (Source)
or else raise Program_Error),
Post => (if not Target'Has_Same_Storage (Source) then
Length (Target) = Length (Source)'Old and then
Length (Source) = 0 and then
Capacity (Target) >= Length (Source)'Old);
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.
procedure Insert_Vector (Container : in out Vector;
Before : in Extended_Index;
New_Item : in Vector)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before in
First_Index (Container) .. Last_Index (Container) + 1
or else raise Constraint_Error) and then
(Length (Container) <= Maximum_Length - Length (New_Item)
or else raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) and then
Capacity (Container) >= Length (Container);
If Length(New_Item) is 0, then Insert_Vector 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.
If the current vector capacity is less than NL, Reserve_Capacity (Container, NL) is called to increase the vector capacity. Then Insert_Vector 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.
procedure Insert_Vector (Container : in out Vector;
Before : in Cursor;
New_Item : in Vector)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before = No_Element or else
Has_Element (Container, Before)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Length (New_Item)
or else raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) and then
Capacity (Container) >= Length (Container);
If Length(New_Item) is 0, then Insert_Vector does nothing. If Before is No_Element, then the call is equivalent to Insert_Vector (Container, Last_Index (Container) + 1, New_Item); otherwise, the call is equivalent to Insert_Vector (Container, To_Index (Before), New_Item);
procedure Insert_Vector (Container : in out Vector;
Before : in Cursor;
New_Item : in Vector;
Position : out Cursor)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before = No_Element or else
Has_Element (Container, Before)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Length (New_Item)
or else raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) and then
Has_Element (Container, Position) and then
Capacity (Container) >= Length (Container);
If Before equals No_Element, then let T be Last_Index (Container) + 1; otherwise, let T be To_Index (Before). Insert_Vector (Container, T, New_Item) is called, and then Position is set to To_Cursor (Container, T).
procedure Insert (Container : in out Vector;
Before : in Extended_Index;
New_Item : in Element_Type;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before in
First_Index (Container) .. Last_Index (Container) + 1
or else raise Constraint_Error) and then
(Length (Container) <= Maximum_Length - Count
or else raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
Equivalent to Insert (Container, Before, To_Vector (New_Item, Count));
procedure Insert (Container : in out Vector;
Before : in Cursor;
New_Item : in Element_Type;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before = No_Element or else
Has_Element (Container, Before)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Count
or else raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
Equivalent to Insert (Container, Before, To_Vector (New_Item, Count));
procedure Insert (Container : in out Vector;
Before : in Cursor;
New_Item : in Element_Type;
Position : out Cursor;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before = No_Element or else
Has_Element (Container, Before)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Count
or else raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Has_Element (Container, Position) and then
Capacity (Container) >= Length (Container);
Equivalent to Insert (Container, Before, To_Vector (New_Item, Count), Position);
procedure Insert (Container : in out Vector;
Before : in Extended_Index;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before in
First_Index (Container) .. Last_Index (Container) + 1
or else raise Constraint_Error) and then
(Length (Container) <= Maximum_Length - Count
or else raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
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.
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.
procedure Insert (Container : in out Vector;
Before : in Cursor;
Position : out Cursor;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before = No_Element or else
Has_Element (Container, Before)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Count
or else raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Has_Element (Container, Position) and then
Capacity (Container) >= Length (Container);
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).
procedure Prepend_Vector (Container : in out Vector;
New_Item : in Vector)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Length (New_Item)
or else raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) and then
Capacity (Container) >= Length (Container);
Equivalent to Insert (Container, First_Index (Container), New_Item).
procedure Prepend (Container : in out Vector;
New_Item : in Element_Type;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Count
or else raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
Equivalent to Insert (Container, First_Index (Container), New_Item, Count).
procedure Append_Vector (Container : in out Vector;
New_Item : in Vector)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Length (New_Item)
or else raise Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) and then
Capacity (Container) >= Length (Container);
Equivalent to Insert (Container, Last_Index (Container) + 1, New_Item).
procedure Append (Container : in out Vector;
New_Item : in Element_Type;
Count : in Count_Type )
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Count
or else raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
Equivalent to Insert (Container, Last_Index (Container) + 1, New_Item, Count).
procedure Append (Container : in out Vector;
New_Item : in Element_Type)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - 1
or else raise Constraint_Error),
Post => Length (Container)'Old + 1 = Length (Container) and then
Capacity (Container) >= Length (Container);
Equivalent to Insert (Container, Last_Index (Container) + 1, New_Item, 1).
procedure Insert_Space (Container : in out Vector;
Before : in Extended_Index;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before in
First_Index (Container) .. Last_Index (Container) + 1
or else raise Constraint_Error) and then
(Length (Container) <= Maximum_Length - Count
or else raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Capacity (Container) >= Length (Container);
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.
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.
procedure Insert_Space (Container : in out Vector;
Before : in Cursor;
Position : out Cursor;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Before = No_Element or else
Has_Element (Container, Before)
or else raise Program_Error) and then
(Length (Container) <= Maximum_Length - Count
or else raise Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) and then
Has_Element (Container, Position) and then
Capacity (Container) >= Length (Container);
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).
procedure Delete (Container : in out Vector;
Index : in Extended_Index;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Index in
First_Index (Container) .. Last_Index (Container) + 1
or else raise Constraint_Error),
Post => Length (Container)'Old - Count <= Length (Container);
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.
procedure Delete (Container : in out Vector;
Position : in out Cursor;
Count : in Count_Type := 1)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Position /= No_Element
or else raise Constraint_Error) and then
(Has_Element (Container, Position)
or else raise Program_Error),
Post => Length (Container)'Old - Count <= Length (Container)
and then Position = No_Element;
Delete (Container, To_Index (Position), Count) is called, and then Position is set to No_Element.
procedure Delete_First (Container : in out Vector;
Count : in Count_Type := 1)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Length (Container)'Old - Count <= Length (Container);
Equivalent to Delete (Container, First_Index (Container), Count).
procedure Delete_Last (Container : in out Vector;
Count : in Count_Type := 1)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Length (Container)'Old - Count <= Length (Container);
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).
procedure Reverse_Elements (Container : in out Vector)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error;
Reorders the elements of Container in reverse order.
procedure Swap (Container : in out Vector;
I, J : in Index_Type)
with Pre => (not Tampering_With_Elements_Prohibited (Container)
or else raise Program_Error) and then
(I in First_Index (Container) .. Last_Index (Container)
or else raise Constraint_Error) and then
(J in First_Index (Container) .. Last_Index (Container)
or else raise Constraint_Error);
Swap exchanges the values of the elements at positions I and J.
procedure Swap (Container : in out Vector;
I, J : in Cursor)
with Pre => (not Tampering_With_Elements_Prohibited (Container)
or else raise Program_Error) and then
(I /= No_Element or else Constraint_Error) and then
(J /= No_Element or else Constraint_Error) and then
(Has_Element (Container, I)
or else raise Program_Error) and then
(Has_Element (Container, J)
or else raise Program_Error);
Swap exchanges the values of the elements designated by I and J.
function First_Index (Container : Vector) return Index_Type
with Nonblocking, Global => null, Use_Formal => null,
Post => First_Index'Result = Index_Type'First;
Returns the value Index_Type'First.
function First (Container : Vector) return Cursor
with Nonblocking, Global => null, Use_Formal => null,
Post => (if not Is_Empty (Container)
then Has_Element (Container, First'Result)
else First'Result = No_Element);
If Container is empty, First returns No_Element. Otherwise, it returns a cursor that designates the first element in Container.
function First_Element (Container : Vector)
return Element_Type
with Pre => (not Is_Empty (Container)
or else raise Constraint_Error);
Equivalent to Element (Container, First_Index (Container)).
function Last_Index (Container : Vector) return Extended_Index
with Nonblocking, Global => null, Use_Formal => null,
Post => (if Length (Container) = 0 then Last_Index'Result = No_Index
else Count_Type(Last_Index'Result - Index_Type'First) =
Length (Container) - 1);
If Container is empty, Last_Index returns No_Index. Otherwise, it returns the position of the last element in Container.
function Last (Container : Vector) return Cursor
with Nonblocking, Global => null, Use_Formal => null,
Post => (if not Is_Empty (Container)
then Has_Element (Container, Last'Result)
else Last'Result = No_Element);
If Container is empty, Last returns No_Element. Otherwise, it returns a cursor that designates the last element in Container.
function Last_Element (Container : Vector)
return Element_Type
with Pre => (not Is_Empty (Container)
or else raise Constraint_Error);
Equivalent to Element (Container, Last_Index (Container)).
function Next (Position : Cursor) return Cursor
with Nonblocking, Global => in all, Use_Formal => null,
Post => (if Position = No_Element then Next'Result = No_Element);
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.
function Next (Container : Vector;
Position : Cursor) return Cursor
with Nonblocking, Global => null, Use_Formal => null,
Pre => Position = No_Element or else
Has_Element (Container, Position)
or else raise Program_Error,
Post => (if Position = No_Element then Next'Result = No_Element
elsif Has_Element (Container, Next'Result) then
To_Index (Container, Next'Result) =
To_Index (Container, Position) + 1
elsif Next'Result = No_Element then
Position = Last (Container)
else False);
Returns a cursor designating the next element in Container, if any.
procedure Next (Position : in out Cursor)
with Nonblocking, Global => in all, Use_Formal => null;
Equivalent to Position := Next (Position).
procedure Next (Container : in Vector;
Position : in out Cursor)
with Nonblocking, Global => null, Use_Formal => null,
Pre => Position = No_Element or else
Has_Element (Container, Position)
or else raise Program_Error,
Post => (if Position /= No_Element
then Has_Element (Container, Position));
Equivalent to Position := Next (Container, Position).
function Previous (Position : Cursor) return Cursor
with Nonblocking, Global => in all, Use_Formal => null,
Post => (if Position = No_Element
then Previous'Result = No_Element);
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.
function Previous (Container : Vector;
Position : Cursor) return Cursor
with Nonblocking, Global => null, Use_Formal => null,
Pre => Position = No_Element or else
Has_Element (Container, Position)
or else raise Program_Error,
Post => (if Position = No_Element then Previous'Result = No_Element
elsif Has_Element (Container, Previous'Result) then
To_Index (Container, Previous'Result) =
To_Index (Container, Position) - 1
elsif Previous'Result = No_Element then
Position = First (Container)
else False);
Returns a cursor designating the previous element in Container, if any.
procedure Previous (Position : in out Cursor)
with Nonblocking, Global => in all, Use_Formal => null;
Equivalent to Position := Previous (Position).
procedure Previous (Container : in Vector;
Position : in out Cursor)
with Nonblocking, Global => null, Use_Formal => null,
Pre => Position = No_Element or else
Has_Element (Container, Position)
or else raise Program_Error,
Post => (if Position /= No_Element
then Has_Element (Container, Position));
Equivalent to Position := Previous (Container, Position).
function Find_Index (Container : Vector;
Item : Element_Type;
Index : Index_Type := Index_Type'First)
return Extended_Index;
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.
function Find (Container : Vector;
Item : Element_Type;
Position : Cursor := No_Element)
return Cursor
with Pre => Position = No_Element or else
Has_Element (Container, Position)
or else raise Program_Error,
Post => (if Find'Result /= No_Element
then Has_Element (Container, Find'Result));
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.
function Reverse_Find_Index (Container : Vector;
Item : Element_Type;
Index : Index_Type := Index_Type'Last)
return Extended_Index;
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.
function Reverse_Find (Container : Vector;
Item : Element_Type;
Position : Cursor := No_Element)
return Cursor
with Pre => Position = No_Element or else
Has_Element (Container, Position)
or else raise Program_Error,
Post => (if Reverse_Find'Result /= No_Element
then Has_Element (Container, Reverse_Find'Result));
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.
function Contains (Container : Vector;
Item : Element_Type) return Boolean;
Equivalent to Has_Element (Find (Container, Item)).
Paragraphs 225 and 226 were moved above.
procedure Iterate
(Container : in Vector;
Process : not null access procedure (Position : in Cursor))
with Allows_Exit;
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.
procedure Reverse_Iterate
(Container : in Vector;
Process : not null access procedure (Position : in Cursor))
with Allows_Exit;
Iterates over the elements in Container as per procedure Iterate, except that elements are traversed in reverse index order.
function Iterate (Container : in Vector)
return Vector_Iterator_Interfaces.Parallel_Reversible_Iterator 'Class
with Post => Tampering_With_Cursors_Prohibited (Container);
Iterate returns an 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, and processing all nodes concurrently when used as a parallel 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.
function Iterate (Container : in Vector; Start : in Cursor)
return Vector_Iterator_Interfaces.Reversible_Iterator'Class
with Pre => (Start /= No_Element
or else raise Constraint_Error) and then
(Has_Element (Container, Start)
or else raise Program_Error),
Post => Tampering_With_Cursors_Prohibited (Container);
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.
exit when Cur = Stop;
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.
function Is_Sorted (Container : Vector) return Boolean;
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.
procedure Sort (Container : in out Vector)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error;
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.
procedure Merge (Target : in out Vector;
Source : in out Vector)
with Pre => (not Tampering_With_Cursors_Prohibited (Target)
or else raise Program_Error) and then
(not Tampering_With_Cursors_Prohibited (Source)
or else raise Program_Error) and then
(Length (Target) <= Maximum_Length - Length (Source)
or else raise Constraint_Error) and then
((Length (Source) = 0 or else
not Target'Has_Same_Storage (Source))
or else raise Program_Error),
Post => (declare
Result_Length : constant Count_Type :=
Length (Source)'Old + Length (Target)'Old;
begin
(Length (Source) = 0 and then
Length (Target) = Result_Length and then
Capacity (Target) >= Result_Length));
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.
The nested package Vectors.Stable provides a type Stable.Vector that represents a stable vector, which is one that cannot grow and shrink. Such a vector can be created by calling the To_Vector or Copy functions, or by establishing a stabilized view of an ordinary vector.