Руководство по Ada (Ada 2022)
A.18.2 Обобщенный пакет Containers.Vectors
Определяемый языком обобщенный пакет Containers.Vectors предоставляет приватные типы Vector и Cursor, а также набор операций для каждого типа. Контейнер типа vector позволяет вставлять и удалять элементы в любой позиции, но он оптимизирован для вставки и удаления в конце контейнера (с наибольшим индексом). Контейнер типа vector также предоставляет произвольный доступ к своим элементам.
Контейнер типа vector концептуально ведет себя как массив, который расширяется по мере необходимости при вставке элементов. *Длина* вектора — это количество элементов, которые содержит вектор. *Ёмкость* вектора — это максимальное количество элементов, которые могут быть вставлены в вектор до его автоматического расширения.
Элементы в контейнере типа vector могут быть обращены по индексу значения из обобщенного формального типа. Первый элемент вектора всегда имеет значение индекса, равное нижней границе формального типа.
Контейнер типа vector может содержать *пустые элементы*. Пустые элементы не имеют заданного значения.
Статическая семантика
Обобщенный пакет библиотек Containers.Vectors имеет следующее объявление:
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
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;
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;
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;
type Cursor is private
with Preelaborable_Initialization;
with Preelaborable_Initialization;
Empty_Vector : constant Vector;
No_Element : constant Cursor;
function Has_Element (Position : Cursor) return Boolean
with Nonblocking, Global => in all, Use_Formal => null;
with Nonblocking, Global => in all, Use_Formal => null;
function Has_Element (Container : Vector; Position : Cursor)
return Boolean
with Nonblocking, Global => null, Use_Formal => null;
return Boolean
with Nonblocking, Global => null, Use_Formal => null;
package Vector_Iterator_Interfaces is new
Ada.Iterator_Interfaces (Cursor, Has_Element);
Ada.Iterator_Interfaces (Cursor, Has_Element);
function "=" (Left, Right : Vector) return Boolean;
function Tampering_With_Cursors_Prohibited
(Container : Vector) return Boolean
with Nonblocking, Global => null, Use_Formal => null;
(Container : Vector) return Boolean
with Nonblocking, Global => null, Use_Formal => null;
function Tampering_With_Elements_Prohibited
(Container : Vector) return Boolean
with Nonblocking, Global => null, Use_Formal => null;
(Container : Vector) return Boolean
with Nonblocking, Global => null, Use_Formal => null;
function Maximum_Length return Count_Type
with Nonblocking, Global => null, Use_Formal => null;
with Nonblocking, Global => null, Use_Formal => null;
function Empty (Capacity : Count_Type := определяемое реализацией)
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;
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;
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;
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;
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;
(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;
function New_Vector (First, Last : Index_Type) return Vector is
(To_Vector (Count_Type (Last - First + 1)))
with Pre => First = Index_Type'First;
(To_Vector (Count_Type (Last - First + 1)))
with Pre => First = Index_Type'First;
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);
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);
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;
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;
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;
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;
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;
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;
function Capacity (Container : Vector) return Count_Type
with Nonblocking, Global => null, Use_Formal => null;
with Nonblocking, Global => null, Use_Formal => null;
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;
Capacity : in Count_Type)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Container.Capacity >= Capacity;
function Length (Container : Vector) return Count_Type
with Nonblocking, Global => null, Use_Formal => null;
with Nonblocking, Global => null, Use_Formal => null;
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;
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;
function Is_Empty (Container : Vector) return Boolean
with Nonblocking, Global => null, Use_Formal => null,
Post => Is_Empty'Result = (Length (Container) = 0);
with Nonblocking, Global => null, Use_Formal => null,
Post => Is_Empty'Result = (Length (Container) = 0);
procedure Clear (Container : in out Vector)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Length (Container) = 0;
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Length (Container) = 0;
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;
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;
function To_Index (Position : Cursor) return Extended_Index
with Nonblocking, Global => in all;
with Nonblocking, Global => in all;
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;
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;
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;
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;
with Pre => Position /= No_Element or else raise Constraint_Error,
Nonblocking, Global => in all, Use_Formal => Element_Type;
функция Element (Container : Vector;
Position : Cursor) возвращает Element_Type
с Pre => (Position /= No_Element или
вызвать Constraint_Error) и затем
(Has_Element (Container, Position)
или вызвать Program_Error),
Nonblocking, Global => null, Use_Formal => Element_Type;
Position : Cursor) возвращает Element_Type
с Pre => (Position /= No_Element или
вызвать Constraint_Error) и затем
(Has_Element (Container, Position)
или вызвать Program_Error),
Nonblocking, Global => null, Use_Formal => Element_Type;
процедура Replace_Element (Container : вход/выход Vector;
Index : вход Index_Type;
New_Item : вход Element_Type)
с Pre => (не Tampering_With_Elements_Prohibited (Container)
или вызвать Program_Error) и затем
(Index в
First_Index (Container) .. Last_Index (Container)
или вызвать Constraint_Error);
Index : вход Index_Type;
New_Item : вход Element_Type)
с Pre => (не Tampering_With_Elements_Prohibited (Container)
или вызвать Program_Error) и затем
(Index в
First_Index (Container) .. Last_Index (Container)
или вызвать Constraint_Error);
процедура Replace_Element (Container : вход/выход Vector;
Position : вход Cursor;
New_item : вход Element_Type)
с Pre => (не Tampering_With_Elements_Prohibited (Container)
или вызвать Program_Error) и затем
(Position /= No_Element
или вызвать Constraint_Error) и затем
(Has_Element (Container, Position)
или вызвать Program_Error);
Position : вход Cursor;
New_item : вход Element_Type)
с Pre => (не Tampering_With_Elements_Prohibited (Container)
или вызвать Program_Error) и затем
(Position /= No_Element
или вызвать Constraint_Error) и затем
(Has_Element (Container, Position)
или вызвать Program_Error);
процедура Query_Element
(Container : вход Vector;
Index : вход Index_Type;
Process : не null доступная процедура (Element : вход Element_Type))
с Pre => Index в
First_Index (Container) .. Last_Index (Container)
или вызвать Constraint_Error;
(Container : вход Vector;
Index : вход Index_Type;
Process : не null доступная процедура (Element : вход Element_Type))
с Pre => Index в
First_Index (Container) .. Last_Index (Container)
или вызвать Constraint_Error;
процедура Query_Element
(Position : вход Cursor;
Process : не null доступная процедура (Element : вход Element_Type))
с Pre => Position /= No_Element или вызвать Constraint_Error,
Global => в всех;
(Position : вход Cursor;
Process : не null доступная процедура (Element : вход Element_Type))
с Pre => Position /= No_Element или вызвать Constraint_Error,
Global => в всех;
процедура Query_Element
(Container : вход Vector;
Position : вход Cursor;
Process : не null доступная процедура (Element : вход Element_Type))
с Pre => (Position /= No_Element
или вызвать Constraint_Error) и затем
(Has_Element (Container, Position)
или вызвать Program_Error);
(Container : вход Vector;
Position : вход Cursor;
Process : не null доступная процедура (Element : вход Element_Type))
с Pre => (Position /= No_Element
или вызвать Constraint_Error) и затем
(Has_Element (Container, Position)
или вызвать Program_Error);
процедура Update_Element
(Container : вход/выход Vector;
Index : вход Index_Type;
Process : не null доступная процедура
(Element : вход/выход Element_Type))
с Pre => Index в
First_Index (Container) .. Last_Index (Container)
или вызвать Constraint_Error;
(Container : вход/выход Vector;
Index : вход Index_Type;
Process : не null доступная процедура
(Element : вход/выход Element_Type))
с Pre => Index в
First_Index (Container) .. Last_Index (Container)
или вызвать Constraint_Error;
процедура Update_Element
(Container : вход/выход Vector;
Position : вход Cursor;
Process : не null доступная процедура
(Element : вход/выход Element_Type))
с Pre => (Position /= No_Element
или вызвать Constraint_Error) и затем
(Has_Element (Container, Position)
или вызвать Program_Error);
(Container : вход/выход Vector;
Position : вход Cursor;
Process : не null доступная процедура
(Element : вход/выход Element_Type))
с Pre => (Position /= No_Element
или вызвать Constraint_Error) и затем
(Has_Element (Container, Position)
или вызвать Program_Error);
тип Constant_Reference_Type
(Element : не null доступная константа Element_Type) является частным
с Implicit_Dereference => Element,
Nonblocking, Global => вход/выход синхронизированный,
Default_Initial_Condition => (вызвать Program_Error);
(Element : не null доступная константа Element_Type) является частным
с Implicit_Dereference => Element,
Nonblocking, Global => вход/выход синхронизированный,
Default_Initial_Condition => (вызвать Program_Error);
тип Reference_Type (Element : не null доступная Element_Type) является частным
с Implicit_Dereference => Element,
Nonblocking, Global => вход/выход синхронизированный,
Default_Initial_Condition => (вызвать Program_Error);
с Implicit_Dereference => Element,
Nonblocking, Global => вход/выход синхронизированный,
Default_Initial_Condition => (вызвать Program_Error);
функция Constant_Reference (Container : алиасированный вход Vector;
Index : вход Index_Type)
возвращает Constant_Reference_Type
с Pre => Index в
First_Index (Container) .. Last_Index (Container)
или вызвать Constraint_Error,
Post => Tampering_With_Cursors_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
Index : вход Index_Type)
возвращает Constant_Reference_Type
с Pre => Index в
First_Index (Container) .. Last_Index (Container)
или вызвать Constraint_Error,
Post => Tampering_With_Cursors_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
функция Reference (Container : алиасированный вход/выход Vector;
Index : вход Index_Type)
возвращает Reference_Type
с Pre => Index в
First_Index (Container) .. Last_Index (Container)
или вызвать Constraint_Error,
Post => Tampering_With_Cursors_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
Index : вход Index_Type)
возвращает Reference_Type
с Pre => Index в
First_Index (Container) .. Last_Index (Container)
или вызвать Constraint_Error,
Post => Tampering_With_Cursors_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
функция Constant_Reference (Container : алиасированный вход Vector;
Position : вход Cursor)
возвращает Constant_Reference_Type
с Pre => (Position /= No_Element
или вызвать Constraint_Error) и затем
(Has_Element (Container, Position)
или вызвать Program_Error),
Post => Tampering_With_Cursors_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
Position : вход Cursor)
возвращает Constant_Reference_Type
с Pre => (Position /= No_Element
или вызвать Constraint_Error) и затем
(Has_Element (Container, Position)
или вызвать Program_Error),
Post => Tampering_With_Cursors_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
функция Reference (Container : алиасированный вход/выход Vector;
Position : вход Cursor)
возвращает Reference_Type
с Pre => (Position /= No_Element
или вызвать Constraint_Error) и затем
(Has_Element (Container, Position)
или вызвать Program_Error),
Post => Tampering_With_Cursors_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
Position : вход Cursor)
возвращает Reference_Type
с Pre => (Position /= No_Element
или вызвать Constraint_Error) и затем
(Has_Element (Container, Position)
или вызвать Program_Error),
Post => Tampering_With_Cursors_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
процедура Assign (Target : вход/выход Vector; Source : вход Vector)
с Pre => не Tampering_With_Cursors_Prohibited (Target)
или вызвать Program_Error,
Post => Length (Source) = Length (Target) и затем
Capacity (Target) >= Length (Target);
с Pre => не Tampering_With_Cursors_Prohibited (Target)
или вызвать Program_Error,
Post => Length (Source) = Length (Target) и затем
Capacity (Target) >= Length (Target);
функция Copy (Source : Vector; Capacity : Count_Type := 0)
возвращает Vector
с Pre => Capacity = 0 или Capacity >= Length (Source)
или вызвать Capacity_Error,
Post => Length (Copy'Result) = Length (Source) и затем
не Tampering_With_Elements_Prohibited (Copy'Result)
и затем
не Tampering_With_Cursors_Prohibited (Copy'Result)
и затем
Copy'Result.Capacity >= (если Capacity = 0 то
Length (Source) иначе Capacity);
возвращает Vector
с Pre => Capacity = 0 или Capacity >= Length (Source)
или вызвать Capacity_Error,
Post => Length (Copy'Result) = Length (Source) и затем
не Tampering_With_Elements_Prohibited (Copy'Result)
и затем
не Tampering_With_Cursors_Prohibited (Copy'Result)
и затем
Copy'Result.Capacity >= (если Capacity = 0 то
Length (Source) иначе Capacity);
процедура Move (Target : вход/выход Vector;
Source : вход/выход Vector)
с Pre => (не Tampering_With_Cursors_Prohibited (Target)
или вызвать Program_Error) и затем
(не Tampering_With_Cursors_Prohibited (Source)
или вызвать Program_Error),
Post => (если не Target'Has_Same_Storage (Source) то
Length (Target) = Length (Source)'Old и затем
Length (Source) = 0 и затем
Capacity (Target) >= Length (Source)'Old);
Source : вход/выход Vector)
с Pre => (не Tampering_With_Cursors_Prohibited (Target)
или вызвать Program_Error) и затем
(не Tampering_With_Cursors_Prohibited (Source)
или вызвать Program_Error),
Post => (если не Target'Has_Same_Storage (Source) то
Length (Target) = Length (Source)'Old и затем
Length (Source) = 0 и затем
Capacity (Target) >= Length (Source)'Old);
процедура Insert_Vector (Container : вход/выход Vector;
Before : вход Extended_Index;
New_Item : вход Vector)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или вызвать Program_Error) и затем
(Before в
First_Index (Container) .. Last_Index (Container) + 1
или вызвать Constraint_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
или вызвать Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Capacity (Container) >= Length (Container);
Before : вход Extended_Index;
New_Item : вход Vector)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или вызвать Program_Error) и затем
(Before в
First_Index (Container) .. Last_Index (Container) + 1
или вызвать Constraint_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
или вызвать Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Capacity (Container) >= Length (Container);
процедура Insert_Vector (Container : вход/выход Vector;
Before : вход Cursor;
New_Item : вход Vector)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или вызвать Program_Error) и затем
(Before = No_Element или
Has_Element (Container, Before)
или вызвать Program_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
или вызвать Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Capacity (Container) >= Length (Container);
Before : вход Cursor;
New_Item : вход Vector)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или вызвать Program_Error) и затем
(Before = No_Element или
Has_Element (Container, Before)
или вызвать Program_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
или вызвать Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Capacity (Container) >= Length (Container);
процедура Insert_Vector (Container : вход/выход Vector;
Before : вход Cursor;
New_Item : вход Vector;
Position : выход Cursor)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или вызвать Program_Error) и затем
(Before = No_Element или
Has_Element (Container, Before)
или вызвать Program_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
или вызвать Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Has_Element (Container, Position) и затем
Capacity (Container) >= Length (Container);
Before : вход Cursor;
New_Item : вход Vector;
Position : выход Cursor)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или вызвать Program_Error) и затем
(Before = No_Element или
Has_Element (Container, Before)
или вызвать Program_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
или вызвать Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Has_Element (Container, Position) и затем
Capacity (Container) >= Length (Container);
процедура Insert (Container : вход/выход Vector;
Before : вход Extended_Index;
New_Item : вход Element_Type;
Count : вход Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или вызвать Program_Error) и затем
(Before в
First_Index (Container) .. Last_Index (Container) + 1
или вызвать Constraint_Error) и затем
(Length (Container) <= Maximum_Length - Count
или вызвать Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) и затем
Capacity (Container) >= Length (Container);
Before : вход Extended_Index;
New_Item : вход Element_Type;
Count : вход Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или вызвать Program_Error) и затем
(Before в
First_Index (Container) .. Last_Index (Container) + 1
или вызвать Constraint_Error) и затем
(Length (Container) <= Maximum_Length - Count
или вызвать Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) и затем
Capacity (Container) >= Length (Container);
процедура Insert (Container : вход/выход Vector;
Before : вход Cursor;
New_Item : вход Element_Type;
Count : вход Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или вызвать Program_Error) и затем
(Before = No_Element или
Has_Element (Container, Before)
или вызвать Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
или вызвать Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) и затем
Capacity (Container) >= Length (Container);
Before : вход Cursor;
New_Item : вход Element_Type;
Count : вход Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или вызвать Program_Error) и затем
(Before = No_Element или
Has_Element (Container, Before)
или вызвать Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
или вызвать Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) и затем
Capacity (Container) >= Length (Container);
процедура Insert (Container : вход/выход Vector;
Before : вход Cursor;
New_Item : вход Element_Type;
Position : выход Cursor;
Count : вход Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или вызвать Program_Error) и затем
(Before = No_Element или
Has_Element (Container, Before)
или вызвать Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
или вызвать Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) и затем
Has_Element (Container, Position) и затем
Capacity (Container) >= Length (Container);
Before : вход Cursor;
New_Item : вход Element_Type;
Position : выход Cursor;
Count : вход Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или вызвать Program_Error) и затем
(Before = No_Element или
Has_Element (Container, Before)
или вызвать Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
или вызвать Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) и затем
Has_Element (Container, Position) и затем
Capacity (Container) >= Length (Container);
процедура Insert (Container : in out Vector;
Before : in Extended_Index;
Count : in Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Before в
First_Index (Container) .. Last_Index (Container) + 1
или иначе поднять Constraint_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) и затем
Capacity (Container) >= Length (Container);
Before : in Extended_Index;
Count : in Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Before в
First_Index (Container) .. Last_Index (Container) + 1
или иначе поднять Constraint_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) и затем
Capacity (Container) >= Length (Container);
процедура Insert (Container : in out Vector;
Before : in Cursor;
Position : out Cursor;
Count : in Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Before = No_Element или
Has_Element (Container, Before)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container)
и затем Has_Element (Container, Position) и затем
Capacity (Container) >= Length (Container);
Before : in Cursor;
Position : out Cursor;
Count : in Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Before = No_Element или
Has_Element (Container, Before)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container)
и затем Has_Element (Container, Position) и затем
Capacity (Container) >= Length (Container);
процедура Prepend_Vector (Container : in out Vector;
New_Item : in Vector)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Capacity (Container) >= Length (Container);
New_Item : in Vector)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Capacity (Container) >= Length (Container);
процедура Prepend (Container : in out Vector;
New_Item : in Element_Type;
Count : in Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) и затем
Capacity (Container) >= Length (Container);
New_Item : in Element_Type;
Count : in Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) и затем
Capacity (Container) >= Length (Container);
процедура Append_Vector (Container : in out Vector;
New_Item : in Vector)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Capacity (Container) >= Length (Container);
New_Item : in Vector)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Capacity (Container) >= Length (Container);
процедура Append (Container : in out Vector;
New_Item : in Element_Type;
Count : in Count_Type)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post =>
Length (Container)'Old + Count = Length (Container) и затем
Capacity (Container) >= Length (Container);
New_Item : in Element_Type;
Count : in Count_Type)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post =>
Length (Container)'Old + Count = Length (Container) и затем
Capacity (Container) >= Length (Container);
процедура Append (Container : in out Vector;
New_Item : in Element_Type)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - 1
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + 1 = Length (Container) и затем
Capacity (Container) >= Length (Container);
New_Item : in Element_Type)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - 1
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + 1 = Length (Container) и затем
Capacity (Container) >= Length (Container);
процедура Insert_Space (Container : in out Vector;
Before : in Extended_Index;
Count : in Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Before в
First_Index (Container) .. Last_Index (Container) + 1
или иначе поднять Constraint_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) и затем
Capacity (Container) >= Length (Container);
Before : in Extended_Index;
Count : in Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Before в
First_Index (Container) .. Last_Index (Container) + 1
или иначе поднять Constraint_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) и затем
Capacity (Container) >= Length (Container);
процедура Insert_Space (Container : in out Vector;
Before : in Cursor;
Position : out Cursor;
Count : in Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Before = No_Element или
Has_Element (Container, Before)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) и затем
Has_Element (Container, Position) и затем
Capacity (Container) >= Length (Container);
Before : in Cursor;
Position : out Cursor;
Count : in Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Before = No_Element или
Has_Element (Container, Before)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Count =
Length (Container) и затем
Has_Element (Container, Position) и затем
Capacity (Container) >= Length (Container);
процедура Delete (Container : in out Vector;
Index : in Extended_Index;
Count : in Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Index в
First_Index (Container) .. Last_Index (Container) + 1
или иначе поднять Constraint_Error),
Post => Length (Container)'Old - Count <=
Length (Container);
Index : in Extended_Index;
Count : in Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Index в
First_Index (Container) .. Last_Index (Container) + 1
или иначе поднять Constraint_Error),
Post => Length (Container)'Old - Count <=
Length (Container);
процедура Delete (Container : in out Vector;
Position : in out Cursor;
Count : in Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Position /= No_Element
или иначе поднять Constraint_Error) и затем
(Has_Element (Container, Position)
или иначе поднять Program_Error),
Post => Length (Container)'Old - Count <=
Length (Container) и затем
Position = No_Element;
Position : in out Cursor;
Count : in Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Position /= No_Element
или иначе поднять Constraint_Error) и затем
(Has_Element (Container, Position)
или иначе поднять Program_Error),
Post => Length (Container)'Old - Count <=
Length (Container) и затем
Position = No_Element;
процедура Delete_First (Container : in out Vector;
Count : in Count_Type := 1)
с Pre => не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error,
Post => Length (Container)'Old - Count <= Length (Container);
Count : in Count_Type := 1)
с Pre => не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error,
Post => Length (Container)'Old - Count <= Length (Container);
процедура Delete_Last (Container : in out Vector;
Count : in Count_Type := 1)
с Pre => не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error,
Post => Length (Container)'Old - Count <= Length (Container);
Count : in Count_Type := 1)
с Pre => не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error,
Post => Length (Container)'Old - Count <= Length (Container);
процедура Reverse_Elements (Container : in out Vector)
с Pre => не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error;
с Pre => не Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error;
процедура Swap (Container : in out Vector;
I, J : in Index_Type)
с Pre => (не Tampering_With_Elements_Prohibited (Container)
или иначе поднять Program_Error) и затем
(I в First_Index (Container) .. Last_Index (Container)
или иначе поднять Constraint_Error) и затем
(J в First_Index (Container) .. Last_Index (Container)
или иначе поднять Constraint_Error);
I, J : in Index_Type)
с Pre => (не Tampering_With_Elements_Prohibited (Container)
или иначе поднять Program_Error) и затем
(I в First_Index (Container) .. Last_Index (Container)
или иначе поднять Constraint_Error) и затем
(J в First_Index (Container) .. Last_Index (Container)
или иначе поднять Constraint_Error);
процедура Swap (Container : in out Vector;
I, J : in Cursor)
с Pre => (не Tampering_With_Elements_Prohibited (Container)
или иначе поднять Program_Error) и затем
(I /= No_Element или Constraint_Error) и затем
(J /= No_Element или Constraint_Error) и затем
(Has_Element (Container, I)
или иначе поднять Program_Error) и затем
(Has_Element (Container, J)
или иначе поднять Program_Error);
I, J : in Cursor)
с Pre => (не Tampering_With_Elements_Prohibited (Container)
или иначе поднять Program_Error) и затем
(I /= No_Element или Constraint_Error) и затем
(J /= No_Element или Constraint_Error) и затем
(Has_Element (Container, I)
или иначе поднять Program_Error) и затем
(Has_Element (Container, J)
или иначе поднять Program_Error);
функция First_Index (Container : Vector) возвращает Index_Type
с Nonblocking, Global => null, Use_Formal => null,
Post => First_Index'Result = Index_Type'First;
с Nonblocking, Global => null, Use_Formal => null,
Post => First_Index'Result = Index_Type'First;
функция First (Container : Vector) возвращает Cursor
с Nonblocking, Global => null, Use_Formal => null,
Post => (если не Is_Empty (Container)
то Has_Element (Container, First'Result)
иначе First'Result = No_Element);
с Nonblocking, Global => null, Use_Formal => null,
Post => (если не Is_Empty (Container)
то Has_Element (Container, First'Result)
иначе First'Result = No_Element);
функция First_Element (Container : Vector)
возвращает Element_Type
с Pre => (не Is_Empty (Container)
или иначе поднять Constraint_Error);
возвращает Element_Type
с Pre => (не Is_Empty (Container)
или иначе поднять Constraint_Error);
функция Last_Index (Container : Vector) возвращает Extended_Index
с Nonblocking, Global => null, Use_Formal => null,
Post => (если Length (Container) = 0
то Last_Index'Result = No_Index
иначе Count_Type(Last_Index'Result - Index_Type'First) =
Length (Container) - 1);
с Nonblocking, Global => null, Use_Formal => null,
Post => (если Length (Container) = 0
то Last_Index'Result = No_Index
иначе Count_Type(Last_Index'Result - Index_Type'First) =
Length (Container) - 1);
функция Last (Container : Vector) возвращает Cursor
с Nonblocking, Global => null, Use_Formal => null,
Post => (если не Is_Empty (Container)
то Has_Element (Container, Last'Result)
иначе Last'Result = No_Element);
с Nonblocking, Global => null, Use_Formal => null,
Post => (если не Is_Empty (Container)
то Has_Element (Container, Last'Result)
иначе Last'Result = No_Element);
функция Last_Element (Container : Vector)
возвращает Element_Type
с Pre => (не Is_Empty (Container)
или иначе поднять Constraint_Error);
возвращает Element_Type
с Pre => (не Is_Empty (Container)
или иначе поднять Constraint_Error);
функция Next (Position : Cursor) возвращает Cursor
с Nonblocking, Global => in all, Use_Formal => null,
Post => (если Position = No_Element то Next'Result = No_Element);
с Nonblocking, Global => in all, Use_Formal => null,
Post => (если Position = No_Element то Next'Result = No_Element);
функция Next (Container : Vector; Position : Cursor) возвращает Cursor
с Nonblocking, Global => null, Use_Formal => null,
Pre => Position = No_Element или
Has_Element (Container, Position)
или иначе поднять Program_Error,
Post => (если Position = No_Element то Next'Result = No_Element
иначе Has_Element (Container, Next'Result) то
To_Index (Container, Next'Result) =
To_Index (Container, Position) + 1
иначе Next'Result = No_Element то
Position = Last (Container)
иначе False);
с Nonblocking, Global => null, Use_Formal => null,
Pre => Position = No_Element или
Has_Element (Container, Position)
или иначе поднять Program_Error,
Post => (если Position = No_Element то Next'Result = No_Element
иначе Has_Element (Container, Next'Result) то
To_Index (Container, Next'Result) =
To_Index (Container, Position) + 1
иначе Next'Result = No_Element то
Position = Last (Container)
иначе False);
процедура Next (Position : in out Cursor)
с Nonblocking, Global => in all, Use_Formal => null;
с Nonblocking, Global => in all, Use_Formal => null;
процедура Next (Container : in Vector;
Position : in out Cursor)
с Nonblocking, Global => null, Use_Formal => null,
Pre => Position = No_Element или
Has_Element (Container, Position)
или иначе поднять Program_Error,
Post => (если Position /= No_Element
то Has_Element (Container, Position));
END_OF_DOCUMENT_MARKER Position : in out Cursor)
с Nonblocking, Global => null, Use_Formal => null,
Pre => Position = No_Element или
Has_Element (Container, Position)
или иначе поднять Program_Error,
Post => (если Position /= No_Element
то Has_Element (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);
with Nonblocking, Global => in all, Use_Formal => null,
Post => (if Position = No_Element
then Previous'Result = No_Element);
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);
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);
procedure Previous (Position : in out Cursor)
with Nonblocking, Global => in all, Use_Formal => null;
with Nonblocking, Global => in all, Use_Formal => null;
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));
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));
function Find_Index (Container : Vector;
Item : Element_Type;
Index : Index_Type := Index_Type'First)
return Extended_Index;
Item : Element_Type;
Index : Index_Type := Index_Type'First)
return Extended_Index;
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));
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));
function Reverse_Find_Index (Container : Vector;
Item : Element_Type;
Index : Index_Type := Index_Type'Last)
return Extended_Index;
Item : Element_Type;
Index : Index_Type := Index_Type'Last)
return Extended_Index;
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));
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));
function Contains (Container : Vector;
Item : Element_Type) return Boolean;
Item : Element_Type) return Boolean;
Этот абзац был удалён.
procedure Iterate
(Container : in Vector;
Process : not null access procedure (Position : in Cursor))
with Allows_Exit;
(Container : in Vector;
Process : not null access procedure (Position : in Cursor))
with Allows_Exit;
procedure Reverse_Iterate
(Container : in Vector;
Process : not null access procedure (Position : in Cursor))
with Allows_Exit;
(Container : in Vector;
Process : not null access procedure (Position : in Cursor))
with Allows_Exit;
function Iterate (Container : in Vector)
return Vector_Iterator_Interfaces.Parallel_Reversible_Iterator'Class
with Post => Tampering_With_Cursors_Prohibited (Container);
return Vector_Iterator_Interfaces.Parallel_Reversible_Iterator'Class
with Post => Tampering_With_Cursors_Prohibited (Container);
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);
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);
generic
with function "<" (Left, Right : Element_Type)
return Boolean is <>;
package Generic_Sorting
with Nonblocking, Global => null is
with function "<" (Left, Right : Element_Type)
return Boolean is <>;
package Generic_Sorting
with Nonblocking, Global => null is
function Is_Sorted (Container : Vector) return Boolean;
procedure Sort (Container : in out Vector)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error;
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error;
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));
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));
end Generic_Sorting;
package Stable is
type 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;
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;
with Preelaborable_Initialization;
Empty_Vector : constant Vector;
No_Element : constant Cursor;
function Has_Element (Position : Cursor) return Boolean
with Nonblocking, Global => in all, Use_Formal => null;
with Nonblocking, Global => in all, Use_Formal => null;
package Vector_Iterator_Interfaces is new
Ada.Iterator_Interfaces (Cursor, Has_Element);
Ada.Iterator_Interfaces (Cursor, Has_Element);
procedure Assign (Target : in out Vectors.Vector;
Source : in Vector)
with Post => Length (Source) = Length (Target) and then
Capacity (Target) >= Length (Target);
Source : in Vector)
with Post => Length (Source) = Length (Target) and then
Capacity (Target) >= Length (Target);
function Copy (Source : Vectors.Vector) return Vector
with Post => Length (Copy'Result) = Length (Source);
with Post => Length (Copy'Result) = Length (Source);
type 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);
(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);
type 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);
(Element : not null access Element_Type) is private
with Implicit_Dereference => Element,
Nonblocking, Global => null, Use_Formal => null,
Default_Initial_Condition => (raise Program_Error);
-- Дополнительные подпрограммы, как описано в тексте
-- объявлены здесь.
-- объявлены здесь.
private
... -- не указано языком
end Stable;
private
... -- не указано языком
end Ada.Containers.Vectors;
Ожидается, что фактическая функция для обобщённого формального оператора "=" для значений Element_Type определит рефлексивное и симметричное отношение и вернёт одно и то же значение результата каждый раз, когда она вызывается с конкретной парой значений. Если она работает по-другому, функции, использующие её, возвращают неопределённое значение. Точные аргументы и количество вызовов этой обобщённой формальной функции функциями, использующими её, не определены.
Тип Vector используется для представления векторов. Тип Vector требует финализации (см. 7.6).
Empty_Vector представляет собой пустой объект вектора. Его длина равна 0. Если объект типа Vector не инициализирован иначе, он инициализируется тем же значением, что и Empty_Vector.
No_Element представляет собой курсор, который не обозначает ни одного элемента. Если объект типа Cursor не инициализирован иначе, он инициализируется тем же значением, что и No_Element.
Примитивный оператор "=" для типа Cursor возвращает True, если оба курсора являются No_Element или обозначают один и тот же элемент в одном и том же контейнере.
Выполнение стандартной реализации атрибутов Input, Output, Read или Write типа Cursor вызывает Program_Error.
Vector'Write для объекта вектора V записывает Length(V) элементов вектора в поток. Также он может записать дополнительную информацию о векторе.
Vector'Read считывает представление вектора из потока и присваивает Item вектор с той же длиной и элементами, что и был записан Vector'Write.
No_Index представляет собой позицию, которая не соответствует ни одному элементу. Подтип Extended_Index включает индексы, покрываемые Index_Type, плюс значение No_Index и, если оно существует, преемника Index_Type'Last.
Некоторые операции проверяют «вмешательство в курсоры» контейнера, потому что они зависят от того, чтобы набор элементов контейнера оставался постоянным, а другие проверяют «вмешательство в элементы» контейнера, потому что они зависят от того, чтобы элементы контейнера не заменялись. Когда вмешательство в курсоры запрещено для конкретного объекта вектора V, Program_Error передаётся при финализации V, а также при вызове, передающем V в определённые операции этого пакета, как указано в предусловии такой операции. Аналогично, когда вмешательство в элементы запрещено для V, Program_Error передаётся при вызове, передающем V в определённые другие операции этого пакета, как указано в предусловии такой операции.
Абзацы с 91 по 97 удалены, поскольку теперь эти правила описаны в предусловиях.
function Has_Element (Position : Cursor) return Boolean
with Nonblocking, Global => in all, Use_Formal => null;
with Nonblocking, Global => in all, Use_Formal => null;
Возвращает True, если Position обозначает элемент, и False в противном случае.
function Has_Element (Container : Vector; Position : Cursor)
return Boolean
with Nonblocking, Global => null, Use_Formal => null;
return Boolean
with Nonblocking, Global => null, Use_Formal => null;
Возвращает True, если Position обозначает элемент в Container, и False в противном случае.
function "=" (Left, Right : Vector) return Boolean;
Если Left и Right обозначают один и тот же объект вектора, функция возвращает True. Если у Left и Right разная длина, функция возвращает False. В противном случае она сравнивает каждый элемент в Left с соответствующим элементом в Right, используя универсальный формальный оператор равенства. Если любое такое сравнение возвращает False, функция возвращает False; в противном случае — True. Любое исключение, возникшее во время оценки равенства элементов, передаётся дальше.
function Tampering_With_Cursors_Prohibited
(Container : Vector) return Boolean
with Nonblocking, Global => null, Use_Formal => null;
(Container : Vector) return Boolean
with Nonblocking, Global => null, Use_Formal => null;
Возвращает True, если вмешательство в курсоры или вмешательство в элементы в данный момент запрещено для Container, и False в противном случае.
function Tampering_With_Elements_Prohibited
(Container : Vector) return Boolean
with Nonblocking, Global => null, Use_Formal => null;
(Container : Vector) return Boolean
with Nonblocking, Global => null, Use_Formal => null;
Всегда возвращает False, независимо от того, запрещено ли вмешательство в элементы.
function Maximum_Length return Count_Type
with Nonblocking, Global => null, Use_Formal => null;
with Nonblocking, Global => null, Use_Formal => null;
Возвращает максимальную длину вектора, исходя из типа индекса.
function Empty (Capacity : Count_Type := определённое реализацией)
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;
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;
Возвращает пустой вектор.
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;
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;
Возвращает вектор длины Length, заполненный пустыми элементами.
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;
(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;
Возвращает вектор длины Length, заполненный элементами, инициализированными значением 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);
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);
Возвращает вектор, содержащий элементы Left, после которых следуют элементы 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;
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;
Возвращает вектор, содержащий элементы Left, после которых следует элемент 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;
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;
Возвращает вектор, содержащий элемент Left, после которого следуют элементы 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;
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;
Возвращает вектор, содержащий элемент Left, после которого следует элемент Right.
function Capacity (Container : Vector) return Count_Type
with Nonblocking, Global => null, Use_Formal => null;
with Nonblocking, Global => null, Use_Formal => null;
Возвращает ёмкость 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;
Capacity : in Count_Type)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Container.Capacity >= Capacity;
Если ёмкость Container уже больше или равна Capacity, Reserve_Capacity не оказывает никакого влияния. В противном случае Reserve_Capacity выделяет дополнительное хранилище по мере необходимости, чтобы обеспечить, что длина результирующего вектора может стать по крайней мере равной значению Capacity без необходимости в дополнительном вызове Reserve_Capacity, и достаточно велика, чтобы содержать текущую длину Container. Reserve_Capacity затем, при необходимости, перемещает элементы в новое хранилище и освобождает любое больше не нужное хранилище. Любое исключение, возникающее во время выделения, передаётся дальше, и Container не изменяется.
function Length (Container : Vector) return Count_Type
with Nonblocking, Global => null, Use_Formal => null;
with Nonblocking, Global => null, Use_Formal => null;
Возвращает количество элементов в 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;
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;
Если Length больше ёмкости Container, Set_Length вызывает Reserve_Capacity (Container, Length), затем устанавливает длину Container равной Length. Если Length больше исходной длины Container, к Container добавляются пустые элементы; в противном случае элементы удаляются из Container.
function Is_Empty (Container : Vector) return Boolean
with Nonblocking, Global => null, Use_Formal => null,
Post => Is_Empty'Result = (Length (Container) = 0);
with Nonblocking, Global => null, Use_Formal => null,
Post => Is_Empty'Result = (Length (Container) = 0);
Возвращает True, если Container пустой.
procedure Clear (Container : in out Vector)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Length (Container) = 0;
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Length (Container) = 0;
Удаляет все элементы из Container. Ёмкость Container не меняется.
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;
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;
Возвращает курсор, обозначающий элемент в позиции Index в Container; возвращает No_Element, если Index не обозначает элемент. В целях определения перекрытия параметров в вызове To_Cursor параметр Container не считается перекрывающимся ни с каким объектом (включая себя).
function To_Index (Position : Cursor) return Extended_Index
with Nonblocking, Global => in all, Use_Formal => null;
with Nonblocking, Global => in all, Use_Formal => null;
Если Position равно No_Element, возвращается No_Index. В противном случае возвращается индекс (в содержащем векторе) элемента, обозначенного Position.
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;
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;
Возвращает индекс (в Container) элемента, обозначенного Position; возвращает No_Index, если Position не обозначает элемент. В целях определения перекрытия параметров в вызове To_Index параметр Container не считается перекрывающимся ни с каким объектом (включая себя).
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;
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 возвращает элемент в позиции 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;
with Pre => Position /= No_Element or else raise Constraint_Error,
Nonblocking, Global => in all, Use_Formal => Element_Type;
Element возвращает элемент, обозначенный 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;
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 возвращает элемент, обозначенный Position в 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);
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 присваивает значение New_Item элементу в позиции Index. Любое исключение, возникающее во время присваивания, передаётся дальше. Элемент в позиции Index не является пустым после успешного вызова Replace_Element. Для целей определения перекрытия параметров в вызове Replace_Element параметр Container не считается перекрывающимся ни с каким объектом (включая сам себя), а параметр Index считается перекрывающимся с элементом в позиции 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);
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 присваивает New_Item элементу, обозначенному Position. Любое исключение, возникающее во время присваивания, передаётся дальше. Элемент в позиции Position не является пустым после успешного вызова Replace_Element. Для целей определения перекрытия параметров в вызове Replace_Element параметр Container не считается перекрывающимся ни с каким объектом (включая сам себя).
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;
(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 вызывает Process.all с элементом в позиции Index в качестве аргумента. Изменение элементов Container запрещено во время выполнения вызова Process.all. Любое исключение, возбуждённое Process.all, передаётся дальше.
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;
(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 вызывает Process.all с элементом, обозначенным Position, в качестве аргумента. Изменение элементов вектора, содержащего элемент, обозначенный Position, запрещено во время выполнения вызова Process.all. Любое исключение, возбуждённое Process.all, передаётся дальше.
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);
(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 вызывает Process.all с элементом, обозначенным Position, в качестве аргумента. Изменение элементов Container запрещено во время выполнения вызова Process.all. Любое исключение, возбуждённое Process.all, передаётся дальше.
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;
(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 вызывает Process.all с элементом в позиции Index в качестве аргумента. Изменение элементов Container запрещено во время выполнения вызова Process.all. Любое исключение, возбуждённое Process.all, передаётся дальше.
Если Element_Type не ограничен и определён, то фактический параметр Element Process.all должен быть неограниченным.
Элемент в позиции Index не является пустым после успешного завершения этой операции.
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);
(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 вызывает Process.all с элементом, обозначенным Position, в качестве аргумента. Изменение элементов Container запрещено во время выполнения вызова Process.all. Любое исключение, возбуждённое Process.all, передаётся дальше.
Если Element_Type не ограничен и определён, то фактический параметр Element Process.all должен быть неограниченным.
Элемент, обозначенный Position, не является пустым после успешного завершения этой операции.
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);
(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);
with Implicit_Dereference => Element,
Nonblocking, Global => in out synchronized,
Default_Initial_Condition => (raise Program_Error);
Типы Constant_Reference_Type и Reference_Type нуждаются в завершении.
Этот абзац был удалён.
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;
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;
Эта функция (в сочетании с Constant_Indexing и Implicit_Dereference) предоставляет удобный способ получения чтения доступа к отдельному элементу вектора по заданному индексу.
Constant_Reference возвращает объект, дискриминант которого является значением доступа, указывающим на элемент в позиции Index. Изменение элементов Container запрещено, пока объект, возвращаемый Constant_Reference, существует и не завершен.
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;
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;
Эта функция (в сочетании с Variable_Indexing и Implicit_Dereference) предоставляет удобный способ получения чтения и записи доступа к отдельному элементу вектора по заданному индексу.
Reference возвращает объект, дискриминант которого является значением доступа, указывающим на элемент в позиции Index. Изменение элементов Container запрещено, пока объект, возвращаемый Reference, существует и не завершен.
Элемент в позиции Index не является пустым после успешного завершения этой операции.
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;
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;
Эта функция (в сочетании с Constant_Indexing и Implicit_Dereference) предоставляет удобный способ получения чтения доступа к отдельному элементу вектора по заданному курсору.
Constant_Reference возвращает объект, дискриминант которого является значением доступа, указывающим на элемент, обозначенный Position. Изменение элементов Container запрещено, пока объект, возвращаемый Constant_Reference, существует и не завершен.
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;
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;
Эта функция (в сочетании с аспектами Variable_Indexing и Implicit_Dereference) предоставляет удобный способ получения чтения и записи доступа к отдельному элементу вектора, используя указатель.
Ссылка возвращает объект, дискриминант которого — это значение доступа, обозначающее элемент, указанный Position. Изменение элементов Container запрещено, пока объект, возвращённый Reference, существует и не завершён.
Элемент, указанный Position, не является пустым элементом после успешного выполнения этой операции.
процедура Assign (Target : вход-выход Vector; Source : вход Vector)
с Pre => не Tampering_With_Cursors_Prohibited (Target)
иначе повысить Program_Error,
Post => Length (Source) = Length (Target) и затем
Capacity (Target) >= Length (Target);
с Pre => не Tampering_With_Cursors_Prohibited (Target)
иначе повысить Program_Error,
Post => Length (Source) = Length (Target) и затем
Capacity (Target) >= Length (Target);
Если Target обозначает тот же объект, что и Source, операция не имеет эффекта. Если длина Source больше, чем ёмкость Target, вызывается Reserve_Capacity (Target, Length (Source)). Элементы Source затем копируются в Target так же, как и при операторе присваивания Source в Target (включая установку длины Target равной длине Source).
функция Copy (Source : Vector; Capacity : Count_Type := 0)
возвращает Vector
с Pre => Capacity = 0 иначе Capacity >= Length (Source)
иначе повысить Capacity_Error,
Post => Length (Copy'Result) = Length (Source) и затем
не Tampering_With_Elements_Prohibited (Copy'Result)
и затем
не Tampering_With_Cursors_Prohibited (Copy'Result)
и затем
Copy'Result.Capacity >= (если Capacity = 0 то
Length (Source) иначе Capacity);
возвращает Vector
с Pre => Capacity = 0 иначе Capacity >= Length (Source)
иначе повысить Capacity_Error,
Post => Length (Copy'Result) = Length (Source) и затем
не Tampering_With_Elements_Prohibited (Copy'Result)
и затем
не Tampering_With_Cursors_Prohibited (Copy'Result)
и затем
Copy'Result.Capacity >= (если Capacity = 0 то
Length (Source) иначе Capacity);
Возвращает вектор, элементы которого инициализированы из соответствующих элементов Source.
процедура Move (Target : вход-выход Vector;
Source : вход-выход Vector)
с Pre => (не Tampering_With_Cursors_Prohibited (Target)
иначе повысить Program_Error) и затем
(не Tampering_With_Cursors_Prohibited (Source)
иначе повысить Program_Error),
Post => (если не Target'Has_Same_Storage (Source) то
Length (Target) = Length (Source)'Old и затем
Length (Source) = 0 и затем
Capacity (Target) >= Length (Source)'Old);
Source : вход-выход Vector)
с Pre => (не Tampering_With_Cursors_Prohibited (Target)
иначе повысить Program_Error) и затем
(не Tampering_With_Cursors_Prohibited (Source)
иначе повысить Program_Error),
Post => (если не Target'Has_Same_Storage (Source) то
Length (Target) = Length (Source)'Old и затем
Length (Source) = 0 и затем
Capacity (Target) >= Length (Source)'Old);
Если Target обозначает тот же объект, что и Source, то операция не имеет эффекта. В противном случае Move сначала вызывает Reserve_Capacity (Target, Length (Source)), а затем Clear (Target); затем каждый элемент из Source удаляется из Source и вставляется в Target в исходном порядке.
процедура Insert_Vector (Container : вход-выход Vector;
Before : вход Extended_Index;
New_Item : вход Vector)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
иначе повысить Program_Error) и затем
(Before в
First_Index (Container) .. Last_Index (Container) + 1
иначе повысить Constraint_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
иначе повысить Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Capacity (Container) >= Length (Container);
Before : вход Extended_Index;
New_Item : вход Vector)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
иначе повысить Program_Error) и затем
(Before в
First_Index (Container) .. Last_Index (Container) + 1
иначе повысить Constraint_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
иначе повысить Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Capacity (Container) >= Length (Container);
Если Length(New_Item) равно 0, то Insert_Vector ничего не делает. В противном случае она вычисляет новую длину NL как сумму текущей длины и Length (New_Item); если значение Last, соответствующее длине NL, будет больше, чем Index_Type'Last, то Constraint_Error передаётся.
Если текущая ёмкость вектора меньше, чем NL, вызывается Reserve_Capacity (Container, NL) для увеличения ёмкости вектора. Затем Insert_Vector сдвигает элементы в диапазоне Before .. Last_Index (Container) вверх на Length(New_Item) позиций, а затем копирует элементы New_Item в позиции, начиная с Before. Любое исключение, поднятое во время копирования, передаётся.
процедура Insert_Vector (Container : вход-выход Vector;
Before : вход Cursor;
New_Item : вход Vector)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
иначе повысить Program_Error) и затем
(Before = No_Element иначе
Has_Element (Container, Before)
иначе повысить Program_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
иначе повысить Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Capacity (Container) >= Length (Container);
Before : вход Cursor;
New_Item : вход Vector)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
иначе повысить Program_Error) и затем
(Before = No_Element иначе
Has_Element (Container, Before)
иначе повысить Program_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
иначе повысить Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Capacity (Container) >= Length (Container);
Если Length(New_Item) равно 0, то Insert_Vector ничего не делает. Если Before равно No_Element, то вызов эквивалентен Insert_Vector (Container, Last_Index (Container) + 1, New_Item); в противном случае вызов эквивалентен Insert_Vector (Container, To_Index (Before), New_Item);
процедура Insert_Vector (Container : вход-выход Vector;
Before : вход Cursor;
New_Item : вход Vector;
Position : выход Cursor)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
иначе возврат Program_Error) и затем
(Before = No_Element или иначе
Has_Element (Container, Before)
иначе возврат Program_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
иначе возврат Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Has_Element (Container, Position) и затем
Capacity (Container) >= Length (Container);
Before : вход Cursor;
New_Item : вход Vector;
Position : выход Cursor)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
иначе возврат Program_Error) и затем
(Before = No_Element или иначе
Has_Element (Container, Before)
иначе возврат Program_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
иначе возврат Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Has_Element (Container, Position) и затем
Capacity (Container) >= Length (Container);
Если Before равно No_Element, то пусть T будет Last_Index (Container) + 1; иначе, пусть T будет To_Index (Before). Вызывается Insert_Vector (Container, T, New_Item), а затем Position устанавливается в To_Cursor (Container, T).
процедура Insert (Container : вход-выход Vector;
Before : вход Extended_Index;
New_Item : вход Element_Type;
Count : вход Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
иначе возврат Program_Error) и затем
(Before в
First_Index (Container) .. Last_Index (Container) + 1
иначе возврат Constraint_Error) и затем
(Length (Container) <= Maximum_Length - Count
иначе возврат Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) и затем
Capacity (Container) >= Length (Container);
Before : вход Extended_Index;
New_Item : вход Element_Type;
Count : вход Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
иначе возврат Program_Error) и затем
(Before в
First_Index (Container) .. Last_Index (Container) + 1
иначе возврат Constraint_Error) и затем
(Length (Container) <= Maximum_Length - Count
иначе возврат Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) и затем
Capacity (Container) >= Length (Container);
Эквивалентно Insert (Container, Before, To_Vector (New_Item, Count));
процедура Insert (Container : вход-выход Vector;
Before : вход Cursor;
New_Item : вход Element_Type;
Count : вход Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
иначе возврат Program_Error) и затем
(Before = No_Element или иначе
Has_Element (Container, Before)
иначе возврат Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
иначе возврат Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) и затем
Capacity (Container) >= Length (Container);
Before : вход Cursor;
New_Item : вход Element_Type;
Count : вход Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
иначе возврат Program_Error) и затем
(Before = No_Element или иначе
Has_Element (Container, Before)
иначе возврат Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
иначе возврат Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) и затем
Capacity (Container) >= Length (Container);
Эквивалентно Insert (Container, Before, To_Vector (New_Item, Count));
процедура Insert (Container : вход-выход Vector;
Before : вход Cursor;
New_Item : вход Element_Type;
Position : выход Cursor;
Count : вход Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
иначе возврат Program_Error) и затем
(Before = No_Element или иначе
Has_Element (Container, Before)
иначе возврат Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
иначе возврат Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) и затем
Has_Element (Container, Position) и затем
Capacity (Container) >= Length (Container);
Before : вход Cursor;
New_Item : вход Element_Type;
Position : выход Cursor;
Count : вход Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
иначе возврат Program_Error) и затем
(Before = No_Element или иначе
Has_Element (Container, Before)
иначе возврат Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
иначе возврат Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) и затем
Has_Element (Container, Position) и затем
Capacity (Container) >= Length (Container);
Эквивалентно Insert (Container, Before, To_Vector (New_Item, Count), Position);
процедура Insert (Container : вход-выход Vector;
Before : вход Extended_Index;
Count : вход Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
иначе возврат Program_Error) и затем
(Before в
First_Index (Container) .. Last_Index (Container) + 1
иначе возврат Constraint_Error) и затем
(Length (Container) <= Maximum_Length - Count
иначе возврат Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) и затем
Capacity (Container) >= Length (Container);
Before : вход Extended_Index;
Count : вход Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
иначе возврат Program_Error) и затем
(Before в
First_Index (Container) .. Last_Index (Container) + 1
иначе возврат Constraint_Error) и затем
(Length (Container) <= Maximum_Length - Count
иначе возврат Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) и затем
Capacity (Container) >= Length (Container);
Если Count равно 0, то Insert ничего не делает. Иначе вычисляется новая длина NL как сумма текущей длины и Count; если значение Last, соответствующее длине NL, было бы больше, чем Index_Type'Last, то Constraint_Error передаётся.
Если текущая ёмкость вектора меньше NL, то вызывается Reserve_Capacity (Container, NL) для увеличения ёмкости вектора. Затем Insert сдвигает элементы в диапазоне Before .. Last_Index (Container) вверх на Count позиций, а затем вставляет элементы, инициализированные по умолчанию (см. 3.3.1), начиная с позиции Before.
процедура Insert (Container : вход-выход Vector;
Before : вход Cursor;
Position : выход Cursor;
Count : вход Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
иначе возврат Program_Error) и затем
(Before = No_Element или иначе
Has_Element (Container, Before)
иначе возврат Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
иначе возврат Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) и затем
Has_Element (Container, Position) и затем
Capacity (Container) >= Length (Container);
Before : вход Cursor;
Position : выход Cursor;
Count : вход Count_Type := 1)
с Pre => (не Tampering_With_Cursors_Prohibited (Container)
иначе возврат Program_Error) и затем
(Before = No_Element или иначе
Has_Element (Container, Before)
иначе возврат Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
иначе возврат Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) и затем
Has_Element (Container, Position) и затем
Capacity (Container) >= Length (Container);
Если Before равно No_Element, то пусть T будет Last_Index (Container) + 1; иначе, пусть T будет To_Index (Before). Вызывается Insert (Container, T, Count), а затем Position устанавливается в To_Cursor (Container, T).
процедура Prepend_Vector (Container : in out Vector;
New_Item : in Vector)
с Pre => (not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Capacity (Container) >= Length (Container);
New_Item : in Vector)
с Pre => (not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Capacity (Container) >= Length (Container);
Эквивалентно Insert (Container, First_Index (Container), New_Item).
процедура Prepend (Container : in out Vector;
New_Item : in Element_Type;
Count : in Count_Type := 1)
с Pre => (not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) и затем
Capacity (Container) >= Length (Container);
New_Item : in Element_Type;
Count : in Count_Type := 1)
с Pre => (not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) и затем
Capacity (Container) >= Length (Container);
Эквивалентно Insert (Container, First_Index (Container), New_Item, Count).
процедура Append_Vector (Container : in out Vector;
New_Item : in Vector)
с Pre => (not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Capacity (Container) >= Length (Container);
New_Item : in Vector)
с Pre => (not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Length (New_Item)
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Length (New_Item) =
Length (Container) и затем
Capacity (Container) >= Length (Container);
Эквивалентно Insert (Container, Last_Index (Container) + 1, New_Item).
процедура Append (Container : in out Vector;
New_Item : in Element_Type;
Count : in Count_Type)
с Pre => (not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) и затем
Capacity (Container) >= Length (Container);
New_Item : in Element_Type;
Count : in Count_Type)
с Pre => (not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) и затем
Capacity (Container) >= Length (Container);
Эквивалентно Insert (Container, Last_Index (Container) + 1, New_Item, Count).
процедура Append (Container : in out Vector;
New_Item : in Element_Type)
с Pre => (not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - 1
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + 1 = Length (Container) и затем
Capacity (Container) >= Length (Container);
New_Item : in Element_Type)
с Pre => (not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - 1
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + 1 = Length (Container) и затем
Capacity (Container) >= Length (Container);
Эквивалентно Insert (Container, Last_Index (Container) + 1, New_Item, 1).
процедура Insert_Space (Container : in out Vector;
Before : in Extended_Index;
Count : in Count_Type := 1)
с Pre => (not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Before в
First_Index (Container) .. Last_Index (Container) + 1
или иначе поднять Constraint_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) и затем
Capacity (Container) >= Length (Container);
Before : in Extended_Index;
Count : in Count_Type := 1)
с Pre => (not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Before в
First_Index (Container) .. Last_Index (Container) + 1
или иначе поднять Constraint_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) и затем
Capacity (Container) >= Length (Container);
Если Count равно 0, то Insert_Space ничего не делает. В противном случае, она вычисляет новую длину NL как сумму текущей длины и Count; если значение Last, соответствующее длине NL, будет больше, чем Index_Type'Last, то Constraint_Error передаётся.
Если текущая ёмкость вектора меньше, чем NL, вызывается Reserve_Capacity (Container, NL) для увеличения ёмкости вектора. Затем Insert_Space сдвигает элементы в диапазоне Before .. Last_Index (Container) вверх на Count позиций, а затем вставляет пустые элементы в позиции, начиная с Before.
процедура Insert_Space (Container : in out Vector;
Before : in Cursor;
Position : out Cursor;
Count : in Count_Type := 1)
с Pre => (not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Before = No_Element или else
Has_Element (Container, Before)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) и затем
Has_Element (Container, Position) и затем
Capacity (Container) >= Length (Container);
Before : in Cursor;
Position : out Cursor;
Count : in Count_Type := 1)
с Pre => (not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Before = No_Element или else
Has_Element (Container, Before)
или иначе поднять Program_Error) и затем
(Length (Container) <= Maximum_Length - Count
или иначе поднять Constraint_Error),
Post => Length (Container)'Old + Count = Length (Container) и затем
Has_Element (Container, Position) и затем
Capacity (Container) >= Length (Container);
Если Before равно No_Element, то пусть T будет Last_Index (Container) + 1; в противном случае, пусть T будет To_Index (Before). Вызывается Insert_Space (Container, T, Count), а затем Position устанавливается в To_Cursor (Container, T).
процедура Delete (Container : in out Vector;
Index : in Extended_Index;
Count : in Count_Type := 1)
с Pre => (not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Index в
First_Index (Container) .. Last_Index (Container) + 1
или иначе поднять Constraint_Error),
Post => Length (Container)'Old - Count <= Length (Container);
Index : in Extended_Index;
Count : in Count_Type := 1)
с Pre => (not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Index в
First_Index (Container) .. Last_Index (Container) + 1
или иначе поднять Constraint_Error),
Post => Length (Container)'Old - Count <= Length (Container);
Если Count равно 0, Delete не оказывает никакого влияния. В противном случае, Delete сдвигает элементы (если таковые имеются) начиная с позиции Index + Count вниз до Index. Любое исключение, возникшее во время присваивания элемента, передаётся.
процедура Delete (Container : in out Vector;
Position : in out Cursor;
Count : in Count_Type := 1)
с Pre => (not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Position /= No_Element
или иначе поднять Constraint_Error) и затем
(Has_Element (Container, Position)
или иначе поднять Program_Error),
Post => Length (Container)'Old - Count <= Length (Container)
и затем Position = No_Element;
Position : in out Cursor;
Count : in Count_Type := 1)
с Pre => (not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error) и затем
(Position /= No_Element
или иначе поднять Constraint_Error) и затем
(Has_Element (Container, Position)
или иначе поднять Program_Error),
Post => Length (Container)'Old - Count <= Length (Container)
и затем Position = No_Element;
Вызывается Delete (Container, To_Index (Position), Count), а затем Position устанавливается в No_Element.
процедура Delete_First (Container : in out Vector;
Count : in Count_Type := 1)
с Pre => not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error,
Post => Length (Container)'Old - Count <= Length (Container);
Count : in Count_Type := 1)
с Pre => not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error,
Post => Length (Container)'Old - Count <= Length (Container);
Эквивалентно Delete (Container, First_Index (Container), Count).
процедура Delete_Last (Container : in out Vector;
Count : in Count_Type := 1)
с Pre => not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error,
Post => Length (Container)'Old - Count <= Length (Container);
Count : in Count_Type := 1)
с Pre => not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error,
Post => Length (Container)'Old - Count <= Length (Container);
Если Length (Container) <= Count, то Delete_Last эквивалентно Clear (Container). В противном случае, оно эквивалентно Delete (Container, Index_Type'Val(Index_Type'Pos(Last_Index (Container)) – Count + 1), Count).
процедура Reverse_Elements (Container : in out Vector)
с Pre => not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error;
с Pre => not Tampering_With_Cursors_Prohibited (Container)
или иначе поднять Program_Error;
Переупорядочивает элементы Container в обратном порядке.
процедура Swap (Container : in out Vector;
I, J : in Index_Type)
с Pre => (not Tampering_With_Elements_Prohibited (Container)
или иначе поднять Program_Error) и затем
(I в First_Index (Container) .. Last_Index (Container)
или иначе поднять Constraint_Error) и затем
(J в First_Index (Container) .. Last_Index (Container)
или иначе поднять Constraint_Error);
I, J : in Index_Type)
с Pre => (not Tampering_With_Elements_Prohibited (Container)
или иначе поднять Program_Error) и затем
(I в First_Index (Container) .. Last_Index (Container)
или иначе поднять Constraint_Error) и затем
(J в First_Index (Container) .. Last_Index (Container)
или иначе поднять Constraint_Error);
Swap меняет значения элементов в позициях I и J.
процедура Swap (Container : in out Vector;
I, J : in Cursor)
с Pre => (not Tampering_With_Elements_Prohibited (Container)
или иначе поднять Program_Error) и затем
(I /= No_Element или else Constraint_Error) и затем
(J /= No_Element или else Constraint_Error) и затем
(Has_Element (Container, I)
или иначе поднять Program_Error) и затем
(Has_Element (Container, J)
или иначе поднять Program_Error);
I, J : in Cursor)
с Pre => (not Tampering_With_Elements_Prohibited (Container)
или иначе поднять Program_Error) и затем
(I /= No_Element или else Constraint_Error) и затем
(J /= No_Element или else Constraint_Error) и затем
(Has_Element (Container, I)
или иначе поднять Program_Error) и затем
(Has_Element (Container, J)
или иначе поднять Program_Error);
Swap меняет значения элементов, обозначенных I и J.
функция First_Index (Container : Vector) возвращает Index_Type
с Nonblocking, Global => null, Use_Formal => null,
Post => First_Index'Result = Index_Type'First;
с Nonblocking, Global => null, Use_Formal => null,
Post => First_Index'Result = Index_Type'First;
Возвращает значение Index_Type'First.
функция First (Container : Vector) возвращает Cursor
с Nonblocking, Global => null, Use_Formal => null,
Post => (если не Is_Empty (Container)
тогда Has_Element (Container, First'Result)
иначе First'Result = No_Element);
с Nonblocking, Global => null, Use_Formal => null,
Post => (если не Is_Empty (Container)
тогда Has_Element (Container, First'Result)
иначе First'Result = No_Element);
Если Container пуст, First возвращает No_Element. В противном случае, она возвращает курсор, который указывает на первый элемент в Container.
функция First_Element (Container : Vector)
возвращает Element_Type
с Pre => (not Is_Empty (Container)
или иначе поднять Constraint_Error);
возвращает Element_Type
с Pre => (not Is_Empty (Container)
или иначе поднять Constraint_Error);
Эквивалентно Element (Container, First_Index (Container)).
функция Last_Index (Container : Vector) возвращает Extended_Index
с Nonblocking, Global => null, Use_Formal => null,
Post => (если Length (Container) = 0 тогда Last_Index'Result = No_Index
иначе Count_Type(Last_Index'Result - Index_Type'First) =
Length (Container) - 1);
с Nonblocking, Global => null, Use_Formal => null,
Post => (если Length (Container) = 0 тогда Last_Index'Result = No_Index
иначе Count_Type(Last_Index'Result - Index_Type'First) =
Length (Container) - 1);
Если Container пуст, Last_Index возвращает No_Index. В противном случае, она возвращает позицию последнего элемента в 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);
with Nonblocking, Global => null, Use_Formal => null,
Post => (if not Is_Empty (Container)
then Has_Element (Container, Last'Result)
else Last'Result = No_Element);
Если Container пуст, Last возвращает No_Element. В противном случае, он возвращает курсор, который указывает на последний элемент в Container.
function Last_Element (Container : Vector)
return Element_Type
with Pre => (not Is_Empty (Container)
or else raise Constraint_Error);
return Element_Type
with Pre => (not Is_Empty (Container)
or else raise Constraint_Error);
Эквивалентно 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);
with Nonblocking, Global => in all, Use_Formal => null,
Post => (if Position = No_Element then Next'Result = No_Element);
Если Position равно No_Element или указывает на последний элемент контейнера, то Next возвращает значение No_Element. В противном случае, он возвращает курсор, который указывает на элемент с индексом To_Index (Position) + 1 в том же векторе, что и 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);
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);
Возвращает курсор, указывающий на следующий элемент в Container, если таковой имеется.
procedure Next (Position : in out Cursor)
with Nonblocking, Global => in all, Use_Formal => null;
with Nonblocking, Global => in all, Use_Formal => null;
Эквивалентно 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));
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));
Эквивалентно 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);
with Nonblocking, Global => in all, Use_Formal => null,
Post => (if Position = No_Element
then Previous'Result = No_Element);
Если Position равно No_Element или указывает на первый элемент контейнера, то Previous возвращает значение No_Element. В противном случае, он возвращает курсор, который указывает на элемент с индексом To_Index (Position) – 1 в том же векторе, что и 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);
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);
Возвращает курсор, указывающий на предыдущий элемент в Container, если таковой имеется.
procedure Previous (Position : in out Cursor)
with Nonblocking, Global => in all, Use_Formal => null;
with Nonblocking, Global => in all, Use_Formal => null;
Эквивалентно 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));
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));
Эквивалентно Position := Previous (Container, Position).
function Find_Index (Container : Vector;
Item : Element_Type;
Index : Index_Type := Index_Type'First)
return Extended_Index;
Item : Element_Type;
Index : Index_Type := Index_Type'First)
return Extended_Index;
Ищет элементы в Container, равные Item (используя генерическое формальное оператор равенства). Поиск начинается с позиции Index и продолжается до Last_Index (Container). Если элемент не найден, Find_Index возвращает No_Index. В противном случае возвращает индекс первого найденного совпадающего элемента.
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));
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 ищет элементы в Container, равные Item (используя генерическое формальное оператор равенства). Поиск начинается с первого элемента, если Position равно No_Element, и с элемента, указанного Position в противном случае. Поиск продолжается до последнего элемента Container. Если элемент не найден, Find возвращает No_Element. В противном случае возвращает курсор, указывающий на первый найденный совпадающий элемент.
function Reverse_Find_Index (Container : Vector;
Item : Element_Type;
Index : Index_Type := Index_Type'Last)
return Extended_Index;
Item : Element_Type;
Index : Index_Type := Index_Type'Last)
return Extended_Index;
Ищет элементы в Container, равные Item (используя генерическое формальное оператор равенства). Поиск начинается с позиции Index или, если Index больше Last_Index (Container), с позиции Last_Index (Container). Поиск продолжается в сторону First_Index (Container). Если элемент не найден, то Reverse_Find_Index возвращает No_Index. В противном случае возвращает индекс первого найденного совпадающего элемента.
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));
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 ищет элементы в Container, равные Item (используя генерическое формальное оператор равенства). Поиск начинается с последнего элемента, если Position равно No_Element, и с элемента, указанного Position в противном случае. Поиск продолжается в сторону первого элемента Container. Если элемент не найден, то Reverse_Find возвращает No_Element. В противном случае возвращает курсор, указывающий на первый найденный совпадающий элемент.
function Contains (Container : Vector;
Item : Element_Type) return Boolean;
Item : Element_Type) return Boolean;
Эквивалентно Has_Element (Find (Container, Item)).
Абзацы 225 и 226 были перемещены выше.
procedure Iterate
(Container : in Vector;
Process : not null access procedure (Position : in Cursor))
with Allows_Exit;
(Container : in Vector;
Process : not null access procedure (Position : in Cursor))
with Allows_Exit;
Вызывает Process.all с курсором, указывающим на каждый элемент в Container в порядке индексов. Изменение курсоров Container запрещено во время выполнения вызова Process.all. Любые исключения, поднятые Process.all, передаются.
procedure Reverse_Iterate
(Container : in Vector;
Process : not null access procedure (Position : in Cursor))
with Allows_Exit;
(Container : in Vector;
Process : not null access procedure (Position : in Cursor))
with Allows_Exit;
Итерирует по элементам в Container, как и процедура Iterate, за исключением того, что элементы проходятся в обратном порядке индексов.
function Iterate (Container : in Vector)
return Vector_Iterator_Interfaces.Parallel_Reversible_Iterator'Class
with Post => Tampering_With_Cursors_Prohibited (Container);
return Vector_Iterator_Interfaces.Parallel_Reversible_Iterator'Class
with Post => Tampering_With_Cursors_Prohibited (Container);
Iterate возвращает объект итератора (см. 5.5.1), который будет генерировать значение для параметра цикла (см. 5.5.2), обозначающее каждый узел в Container, начиная с первого узла и перемещая курсор в соответствии с функцией Next при использовании в качестве прямого итератора, и начиная с последнего узла и перемещая курсор в соответствии с функцией Previous при использовании в качестве обратного итератора, и обрабатывая все узлы параллельно при использовании в качестве параллельного итератора. Изменение курсоров Container запрещено, пока существует объект итератора (в частности, в sequence_of_statements оператора loop_statement, iterator_specification которого обозначает этот объект). Объект итератора требует завершения.
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);
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 возвращает обратимый объект итератора (см. 5.5.1), который будет генерировать значение для параметра цикла (см. 5.5.2), обозначающего каждый узел в Container, начиная с узла, обозначенного Start, и перемещая курсор в соответствии с функцией Next при использовании его как прямого итератора или перемещая курсор в соответствии с функцией Previous при использовании его как обратного итератора. Запрещается вмешиваться в курсоры Container, пока существует объект итератора (в частности, в sequence_of_statements оператора цикла loop_statement, чьё iterator_specification обозначает этот объект). Объект итератора требует финализации.
Ожидается, что фактическая функция для обобщённого формального оператора «<» в Generic_Sorting будет возвращать одно и то же значение каждый раз, когда она вызывается с конкретной парой значений элементов. Она должна определять строго слабое отношение упорядочения (см. A.18); она не должна изменять Container. Если фактическая функция «<» ведёт себя иным образом, поведение подпрограмм Generic_Sorting не определено. Количество вызовов «<» подпрограммами Generic_Sorting не определено.
функция Is_Sorted (Container : Vector) возвращает Boolean;
Возвращает True, если элементы отсортированы в порядке возрастания, как определено обобщённым формальным оператором «<»; в противном случае Is_Sorted возвращает False. Любое исключение, возбуждённое во время вычисления «<», распространяется.
процедура Sort (Container : in out Vector)
с Пре => не Tampering_With_Cursors_Prohibited (Container)
или иначе возбудить Program_Error;
с Пре => не Tampering_With_Cursors_Prohibited (Container)
или иначе возбудить Program_Error;
Переупорядочивает элементы Container таким образом, чтобы они были отсортированы в порядке возрастания, как определено обобщённым формальным оператором «<». Любое исключение, возбуждённое во время вычисления «<», распространяется.
процедура Merge (Target : in out Vector;
Source : in out Vector)
с Пре => (не Tampering_With_Cursors_Prohibited (Target)
или иначе возбудить Program_Error) и затем
(не Tampering_With_Cursors_Prohibited (Source)
или иначе возбудить Program_Error) и затем
(Длина (Target) <= Максимальная_Длина - Длина (Source)
или иначе возбудить Constraint_Error) и затем
((Длина (Source) = 0 или иначе
не Target_Has_Same_Storage (Source))
или иначе возбудить Program_Error),
Post => (объявить
Result_Length : константа Count_Type :=
Длина (Source)'Старое + Длина (Target)'Старое;
начать
(Длина (Source) = 0 и затем
Длина (Target) = Result_Length и затем
Емкость (Target) >= Result_Length));
Source : in out Vector)
с Пре => (не Tampering_With_Cursors_Prohibited (Target)
или иначе возбудить Program_Error) и затем
(не Tampering_With_Cursors_Prohibited (Source)
или иначе возбудить Program_Error) и затем
(Длина (Target) <= Максимальная_Длина - Длина (Source)
или иначе возбудить Constraint_Error) и затем
((Длина (Source) = 0 или иначе
не Target_Has_Same_Storage (Source))
или иначе возбудить Program_Error),
Post => (объявить
Result_Length : константа Count_Type :=
Длина (Source)'Старое + Длина (Target)'Старое;
начать
(Длина (Source) = 0 и затем
Длина (Target) = Result_Length и затем
Емкость (Target) >= Result_Length));
Merge удаляет элементы из Source и вставляет их в Target; после этого Target содержит объединение элементов, которые первоначально находились в Source и Target; Source остается пустым. Если Target и Source изначально отсортированы в порядке возрастания, то Target упорядочивается в порядке возрастания, как определено обобщённым формальным оператором «<»; в противном случае порядок элементов в Target не определён. Любое исключение, возбуждённое во время вычисления «<», распространяется.
Вложенный пакет Vectors.Stable предоставляет тип Stable.Vector, представляющий стабильный вектор, который не может расти и уменьшаться. Такой вектор можно создать, вызвав функции To_Vector или Copy, или установив стабилизированный вид обычного вектора.
Подпрограммы пакета Containers.Vectors, имеющие параметр или результат типа Vector, включаются во вложенный пакет Stable с тем же спецификацией, за исключением следующих:
Tampering_With_Cursors_Prohibited, Tampering_With_Elements_Prohibited, Reserve_Capacity, Assign, Move, Insert, Insert_Space, Insert_Vector, Append, Append_Vector, Prepend, Prepend_Vector, Clear, Delete, Delete_First, Delete_Last и Set_Length
Обобщённый пакет Generic_Sorting также включается с той же спецификацией, за исключением Merge.
Операции этого пакета эквивалентны операциям для обычных векторов, за исключением того, что вызовы Tampering_With_Cursors_Prohibited и Tampering_With_Elements_Prohibited, которые встречаются в предусловиях, заменяются на False, а все, встречающиеся в постусловиях, заменяются на True.
Если стабильный вектор объявлен с дискриминантом Base, обозначающим существующий обычный вектор, то стабильный вектор представляет стабилизированный вид базового обычного вектора, и любая операция со стабильным вектором отражается на базовом обычном векторе. Пока существует стабилизированный вид, любая операция, изменяющая элементы, выполняемая над базовым вектором, запрещена. Финализация стабильного вектора, предоставляющего такой вид, снимает это ограничение на базовый обычный вектор (хотя может существовать другое ограничение из-за других одновременных итераций или стабилизированных видов).
Если стабильный вектор объявлен без указания Base, то объект обязательно инициализируется. Выражение инициализации стабильного вектора, как правило, вызов To_Vector или Copy, определяет Длину вектора. Длина стабильного вектора никогда не изменяется после инициализации.
Ограниченные (временные) ошибки
Чтение значения пустого элемента путём вызова Element, Query_Element, Update_Element, Constant_Reference, Reference, Swap, Is_Sorted, Sort, Merge, «=», Find или Reverse_Find является ограниченной ошибкой. Реализация может рассматривать элемент как имеющий любое обычное значение (см. 13.9.1) типа элемента или возбудить Constraint_Error или Program_Error до изменения вектора.
Вызов Merge в экземпляре Generic_Sorting с Source или Target, не отсортированными в порядке возрастания с использованием предоставленного обобщённого формального оператора «<», является ограниченной ошибкой. Либо Program_Error возбуждается после обновления Target, как описано для Merge, или операция работает как определено.
Это ограниченная ошибка, если фактическая функция, связанная с обобщённым формальным подпрограммой, когда она вызывается в рамках операции этого пакета, изменяет элементы любого параметра Vector операции. Либо возбуждается Program_Error, либо операция работает как определено на значении Vector до или после некоторых или всех изменений Vector.
Вызов любой подпрограммы, объявленной в видимой части Containers.Vectors, когда связанный контейнер был финализирован, является ограниченной ошибкой. Если операция принимает Container как параметр in out, то она возбуждает Constraint_Error или Program_Error. В противном случае операция либо выполняется так, как это было бы для пустого контейнера, либо она возбуждает Constraint_Error или Program_Error.
Значение Cursor является неопределённым, если после его создания произошло любое из следующего:
- Вызваны Insert, Insert_Space, Insert_Vector или Delete для вектора, содержащего элемент, на который указывает курсор, с индексным значением (или курсор, обозначающий элемент в таком индексном значении) меньше или равно индексного значения элемента, обозначенного курсором; или
- Вектор, содержащий элемент, на который он указывает, был передан в процедуры Sort или Merge экземпляра Generic_Sorting или в процедуру Reverse_Elements.
Вызов любой подпрограммы, кроме «=» или Has_Element, объявленной в Containers.Vectors, с неопределённым (но не невалидным, см. ниже) параметром курсора, является ограниченной ошибкой. Возможные результаты:
- Курсор может обрабатываться так, как если бы он был No_Element;
- Курсор может обозначать какой-то элемент в векторе (но не обязательно тот, который он изначально обозначал);
- Может быть возбуждено Constraint_Error; или
- Может быть возбуждено Program_Error.
Ошибочное выполнение
Значение Cursor является невалидным, если после его создания произошло любое из следующего:
- Вектор, содержащий элемент, на который он указывает, был финализирован;
- Вектор, содержащий элемент, на который он указывает, был использован как Target вызова Assign или как цель оператора assignment_statement;
- Вектор, содержащий элемент, на который он указывает, был использован как Source или Target вызова Move; или
- Элемент, на который он указывает, был удалён или удалён из вектора, который ранее содержал элемент.
Результат «=» или Has_Element не определён, если он вызывается с невалидным параметром курсора. Выполнение является ошибочным, если любая другая подпрограмма, объявленная в Containers.Vectors, вызывается с невалидным параметром курсора.
Выполнение является ошибочным, если вектор, связанный с результатом вызова Reference или Constant_Reference, финализируется до финализации объекта-результата, возвращённого вызовом Reference или Constant_Reference.
Требования к реализации
Память, связанная с объектом вектора, не должна теряться при присваивании или выходе из области видимости.
Выполнение оператора assignment_statement для вектора должно иметь эффект копирования элементов из исходного вектора в целевой вектор и изменения длины целевого объекта на длину исходного объекта.
Рекомендации по реализации
Containers.Vectors должен быть реализован аналогично массиву. В частности, если длина вектора равна N, то
- худший случай времени выполнения Element должен быть O(log N);
- худший случай времени выполнения Append с Count=1, когда N меньше ёмкости вектора, должен быть O(log N); и
- худший случай времени выполнения Prepend с Count=1 и Delete_First с Count=1 должен быть O(N log N).
Наихудшее время выполнения вызова процедуры Sort экземпляра Containers.Vectors.Generic_Sorting должно быть O(N**2), а среднее время выполнения должно быть лучше, чем O(N**2).
Containers.Vectors.Generic_Sorting.Sort и Containers.Vectors.Generic_Sorting.Merge должны минимизировать копирование элементов.
Move не должно копировать элементы и должно минимизировать копирование внутренних структур данных.
Если исключение распространяется из операции над вектором, никакой памяти не должно быть потеряно, а также никакие элементы не должны быть удалены из вектора, если это не указано операцией.
ПРИМЕЧАНИЕ 1 Все элементы вектора занимают места во внутренней таблице. Если требуется разреженный контейнер, можно использовать Hashed_Map вместо вектора.
ПРИМЕЧАНИЕ 2 Если Index_Type'Base'First = Index_Type'First, экземпляр Ada.Containers.Vectors вызовет Constraint_Error. Требуется значение ниже Index_Type'First, чтобы у пустого вектора было осмысленное значение Last_Index.