Spec-Zone.ru › Ada 2022
Справочник по Ada (Ada 2022)

A.18.5 Обобщённый пакет Containers.Hashed_Maps

Статическая семантика

Обобщённый пакет библиотек Containers.Hashed_Maps имеет следующее объявление:
with Ada.Iterator_Interfaces;
generic
type Key_Type is private;
type Element_Type is private;
with function Hash (Key : Key_Type) return Hash_Type;
with function Equivalent_Keys (Left, Right : Key_Type)
return Boolean;
with function "=" (Left, Right : Element_Type)
return Boolean is <>;
package Ada.Containers.Hashed_Maps
with Preelaborate, Remote_Types,
Nonblocking, Global => in out synchronized is
type Map is tagged private
with Constant_Indexing => Constant_Reference,
Variable_Indexing => Reference,
Default_Iterator => Iterate,
Iterator_Element => Element_Type,
Iterator_View => Stable.Map,
Aggregate => (Empty => Empty,
Add_Named => Insert),
Stable_Properties => (Length,
Tampering_With_Cursors_Prohibited,
Tampering_With_Elements_Prohibited),
Default_Initial_Condition =>
Length (Map) = 0 and then
(not Tampering_With_Cursors_Prohibited (Map)) and then
(not Tampering_With_Elements_Prohibited (Map)),
Preelaborable_Initialization;
type Cursor is private
with Preelaborable_Initialization;
Empty_Map : constant Map;
No_Element : constant Cursor;
function Has_Element (Position : Cursor) return Boolean
with Nonblocking, Global => in all, Use_Formal => null;
function Has_Element (Container : Map; Position : Cursor)
return Boolean
with Nonblocking, Global => null, Use_Formal => null;
package Map_Iterator_Interfaces is new
Ada.Iterator_Interfaces (Cursor, Has_Element);
function "=" (Left, Right : Map) return Boolean;
function Tampering_With_Cursors_Prohibited
(Container : Map) return Boolean
with Nonblocking, Global => null, Use_Formal => null;
function Tampering_With_Elements_Prohibited
(Container : Map) return Boolean
with Nonblocking, Global => null, Use_Formal => null;
function Empty (Capacity : Count_Type := определяется реализацией)
return Map
with 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 Capacity (Container : Map) return Count_Type
with Nonblocking, Global => null, Use_Formal => null;
procedure Reserve_Capacity (Container : in out Map;
Capacity : in Count_Type)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Container.Capacity >= Capacity;
function Length (Container : Map) return Count_Type
with Nonblocking, Global => null, Use_Formal => null;
function Is_Empty (Container : Map) return Boolean
with Nonblocking, Global => null, Use_Formal => null,
Post => Is_Empty'Result = (Length (Container) = 0);
procedure Clear (Container : in out Map)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Capacity (Container) = Capacity (Container)'Old and then
Length (Container) = 0;
function Key (Position : Cursor) return Key_Type
with Pre => Position /= No_Element
or else raise Constraint_Error,
Nonblocking, Global => in all, Use_Formal => Key_Type;
function Key (Container : Map;
Position : Cursor) return Key_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 => Key_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;
function Element (Container : Map;
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;
procedure Replace_Element (Container : in out Map;
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);
procedure Query_Element
(Position : in Cursor;
Process : not null access procedure (Key : in Key_Type;
Element : in Element_Type))
with Pre => Position /= No_Element
or else raise Constraint_Error,
Global => in all;
procedure Query_Element
(Container : in Map;
Position : in Cursor;
Process : not null access procedure (Key : in Key_Type;
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);
procedure Update_Element
(Container : in out Map;
Position : in Cursor;
Process : not null access procedure
(Key : in Key_Type;
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);
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);
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);
function Constant_Reference (Container : aliased in Map;
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;
function Reference (Container : aliased in out Map;
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;
function Constant_Reference (Container : aliased in Map;
Key : in Key_Type)
return Constant_Reference_Type
with Pre => Find (Container, Key) /= No_Element
or else raise Constraint_Error,
Post => Tampering_With_Cursors_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
function Reference (Container : aliased in out Map;
Key : in Key_Type)
return Reference_Type
with Pre => Find (Container, Key) /= No_Element
or else raise Constraint_Error,
Post => Tampering_With_Cursors_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
procedure Assign (Target : in out Map; Source : in Map)
with Pre => not Tampering_With_Cursors_Prohibited (Target)
or else raise Program_Error,
Post => Length (Source) = Length (Target) and then
Capacity (Target) >= Length (Source);
function Copy (Source : Map; Capacity : Count_Type := 0)
return Map
with Pre => Capacity = 0 or else Capacity >= Length (Source)
or else raise Capacity_Error,
Post =>
Length (Copy'Result) = Length (Source) and then
not Tampering_With_Elements_Prohibited (Copy'Result) and then
not Tampering_With_Cursors_Prohibited (Copy'Result) and then
Copy'Result.Capacity = (if Capacity = 0 then
Length (Source) else Capacity);
procedure Move (Target : in out Map;
Source : in out Map)
with Pre => (not Tampering_With_Cursors_Prohibited (Target)
or else raise Program_Error) and then
(not Tampering_With_Cursors_Prohibited (Source)
or else raise Program_Error),
Post => (if not Target'Has_Same_Storage (Source) then
Length (Target) = Length (Source'Old) and then
Length (Source) = 0);
END_OF_DOCUMENT_MARKER
процедура Insert (Container : in out Map;
Key : in Key_Type;
New_Item : in Element_Type;
Position : out Cursor;
Inserted : out Boolean)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Length (Container) <= Count_Type'Last - 1
or else raise Constraint_Error),
Post => (declare
Original_Length : constant Count_Type :=
Length (Container)'Old;
begin
Has_Element (Container, Position) and then
(if Inserted then
Length (Container) = Original_Length + 1
else
Length (Container) = Original_Length)) and then
Capacity (Container) >= Length (Container);
процедура Insert (Container : in out Map;
Key : in Key_Type;
Position : out Cursor;
Inserted : out Boolean)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Length (Container) <= Count_Type'Last - 1
or else raise Constraint_Error),
Post => (declare
Original_Length : constant Count_Type :=
Length (Container)'Old;
begin
Has_Element (Container, Position) and then
(if Inserted then
Length (Container) = Original_Length + 1
else
Length (Container) = Original_Length)) and then
Capacity (Container) >= Length (Container);
процедура Insert (Container : in out Map;
Key : in Key_Type;
New_Item : in Element_Type)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Length (Container) <= Count_Type'Last - 1
or else raise Constraint_Error),
Post => Length (Container) = Length (Container)'Old + 1 and then
Capacity (Container) >= Length (Container);
процедура Include (Container : in out Map;
Key : in Key_Type;
New_Item : in Element_Type)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Length (Container) <= Count_Type'Last - 1
or else raise Constraint_Error),
Post => (declare
Original_Length : constant Count_Type :=
Length (Container)'Old;
begin
Length (Container)
in Original_Length | Original_Length + 1) and then
Capacity (Container) >= Length (Container);
процедура Replace (Container : in out Map;
Key : in Key_Type;
New_Item : in Element_Type)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Length (Container) = Length (Container)'Old;
процедура Exclude (Container : in out Map;
Key : in Key_Type)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => (declare
Original_Length : constant Count_Type :=
Length (Container)'Old;
begin
Length (Container)
in Original_Length - 1 | Original_Length);
процедура Delete (Container : in out Map;
Key : in Key_Type)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Length (Container) = Length (Container)'Old - 1;
процедура Delete (Container : in out Map;
Position : in out Cursor)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Position /= No_Element
or else raise Constraint_Error) and then
(Has_Element (Container, Position)
or else raise Program_Error),
Post => Length (Container) = Length (Container)'Old - 1 and then
Position = No_Element;
функция First (Container : Map) return Cursor
with Nonblocking, Global => null, Use_Formal => null,
Post => (if not Is_Empty (Container)
then Has_Element (Container, First'Result)
else First'Result = No_Element);
функция Next (Position : Cursor) return Cursor
with Nonblocking, Global => in all, Use_Formal => null,
Post => (if Position = No_Element then Next'Result = No_Element);
функция Next (Container : Map;
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 Next'Result = No_Element then
Position = Last (Container)
else Has_Element (Container, Next'Result));
процедура Next (Position : in out Cursor)
with Nonblocking, Global => in all, Use_Formal => null;
процедура Next (Container : in Map;
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));
функция Find (Container : Map;
Key : Key_Type)
return Cursor
with Post => (if Find'Result /= No_Element
then Has_Element (Container, Find'Result));
функция Element (Container : Map;
Key : Key_Type)
return Element_Type;
функция Contains (Container : Map;
Key : Key_Type) return Boolean;
Этот абзац был удалён.
функция Equivalent_Keys (Left, Right : Cursor)
return Boolean
with Pre => (Left /= No_Element and then Right /= No_Element)
or else raise Constraint_Error,
Global => in all;
функция Equivalent_Keys (Left : Cursor;
Right : Key_Type)
return Boolean
with Pre => Left /= No_Element or else raise Constraint_Error,
Global => in all;
функция Equivalent_Keys (Left : Key_Type;
Right : Cursor)
return Boolean
with Pre => Right /= No_Element or else raise Constraint_Error,
Global => in all;
процедура Iterate
(Container : in Map;
Process : not null access procedure (Position : in Cursor))
with Allows_Exit;
функция Iterate (Container : in Map)
return Map_Iterator_Interfaces.Parallel_Iterator'Class
with Post => Tampering_With_Cursors_Prohibited (Container);
пакет Stable is
тип Map (Base : not null access Hashed_Maps.Map) is
меченый ограниченный частный
with Constant_Indexing => Constant_Reference,
Variable_Indexing => Reference,
Default_Iterator => Iterate,
Iterator_Element => Element_Type,
Stable_Properties => (Length),
Global => null,
Default_Initial_Condition => Length (Map) = 0,
Preelaborable_Initialization;
тип Cursor is private
with Preelaborable_Initialization;
Empty_Map : constant Map;
No_Element : constant Cursor;
функция Has_Element (Position : Cursor) return Boolean
with Nonblocking, Global => in all, Use_Formal => null;
пакет Map_Iterator_Interfaces is new
Ada.Iterator_Interfaces (Cursor, Has_Element);
процедура Assign (Target : in out Hashed_Maps.Map;
Source : in Map)
with Post => Length (Source) = Length (Target);
функция Copy (Source : Hashed_Maps.Map) return Map
with Post => Length (Copy'Result) = Length (Source);
тип 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);
тип 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);
-- Дополнительные подпрограммы, как описано в тексте
-- объявляются здесь.
частный
... -- не указано языком
конец Stable;
частный
... -- не указано языком
конец Ada.Containers.Hashed_Maps;
Объект типа Map содержит расширяемую хеш-таблицу, которая используется для обеспечения прямого доступа к узлам. Ёмкость объекта типа Map — это максимальное количество узлов, которые могут быть вставлены в хеш-таблицу перед её автоматическим расширением.
Два ключа K1 и K2 определяются как эквивалентные, если Equivalent_Keys (K1, K2) возвращает True.
Фактическая функция для обобщенного формального параметра Hash должна возвращать одно и то же значение каждый раз, когда она вызывается со значением ключа. Для любых двух эквивалентных значений ключа фактическая функция Hash должна возвращать одно и то же значение. Если фактическая функция Hash ведет себя каким-либо другим образом, поведение данного пакета не определено. Какие подпрограммы данного пакета вызывают Hash и сколько раз они её вызывают, не определено.
Ожидается, что фактическая функция для универсальной формальной функции Equivalent_Keys для значений Key_Type каждый раз будет возвращать одно и то же значение при вызове с конкретной парой значений ключа. Она должна определять отношение эквивалентности, то есть быть рефлексивной, симметричной и транзитивной. Если фактическое поведение функции Equivalent_Keys отличается, поведение этого пакета не определено. Какие подпрограммы этого пакета вызывают Equivalent_Keys и сколько раз они это делают, не определено.
Если значение ключа, хранящегося в узле карты, изменяется не через операцию в этом пакете таким образом, что по крайней мере один из Hash или Equivalent_Keys дают разные результаты, поведение этого пакета не определено.
Какие узлы являются первым и последним узлом карты, а какой узел является преемником данного узла, не определено, за исключением общей семантики, описанной в A.18.4.
function Empty (Capacity : Count_Type := определяемое реализацией)
return Map
with 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 Capacity (Container : Map) return Count_Type
with Nonblocking, Global => null, Use_Formal => null;
Возвращает емкость Container.
procedure Reserve_Capacity (Container : in out Map;
Capacity : in Count_Type)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Container.Capacity >= Capacity;
Reserve_Capacity выделяет новую хеш-таблицу таким образом, что длина полученной карты может стать по крайней мере равной значению Capacity без необходимости дополнительного вызова Reserve_Capacity, и достаточно велика, чтобы содержать текущую длину Container. Reserve_Capacity затем перехеширует узлы в Container в новую хеш-таблицу. Она заменяет старую хеш-таблицу новой и затем освобождает старую хеш-таблицу. Любое исключение, возникшее во время выделения, распространяется, и Container не изменяется.
Этот абзац был удалён.
procedure Clear (Container : in out Map)
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => Capacity (Container) = Capacity (Container)'Old and then
Length (Container) = 0;
В дополнение к семантике, описанной в A.18.4, Clear не влияет на емкость Container.
procedure Assign (Target : in out Map; Source : in Map)
with Pre => not Tampering_With_Cursors_Prohibited (Target)
or else raise Program_Error,
Post => Length (Source) = Length (Target) and then
Capacity (Target) >= Length (Source);
В дополнение к семантике, описанной в A.18.4, если длина Source больше емкости Target, вызывается Reserve_Capacity (Target, Length (Source)) перед назначением каких-либо элементов.
function Copy (Source : Map; Capacity : Count_Type := 0)
return Map
with Pre => Capacity = 0 or else Capacity >= Length (Source)
or else raise Capacity_Error,
Post =>
Length (Copy'Result) = Length (Source) and then
not Tampering_With_Elements_Prohibited (Copy'Result) and then
not Tampering_With_Cursors_Prohibited (Copy'Result) and then
Copy'Result.Capacity = (if Capacity = 0 then
Length (Source) else Capacity);
Возвращает карту, ключи и элементы которой инициализированы из ключей и элементов Source.
procedure Insert (Container : in out Map;
Key : in Key_Type;
New_Item : in Element_Type;
Position : out Cursor;
Inserted : out Boolean)
with Pre => (not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error) and then
(Length (Container) <= Count_Type'Last - 1
or else raise Constraint_Error),
Post => (declare
Original_Length : constant Count_Type :=
Length (Container)'Old;
begin
Has_Element (Container, Position) and then
(if Inserted then
Length (Container) = Original_Length + 1
else
Length (Container) = Original_Length)) and then
Capacity (Container) >= Length (Container);
В дополнение к семантике, описанной в A.18.4, если Length (Container) равно Capacity (Container), то Insert сначала вызывает Reserve_Capacity для увеличения емкости Container до некоторого большего значения.
function Equivalent_Keys (Left, Right : Cursor)
return Boolean
with Pre => (Left /= No_Element and then Right /= No_Element)
or else raise Constraint_Error,
Global => in all;
Эквивалентно Equivalent_Keys (Key (Left), Key (Right)).
function Equivalent_Keys (Left : Cursor;
Right : Key_Type) return Boolean
with Pre => Left /= No_Element or else raise Constraint_Error,
Global => in all;
Эквивалентно Equivalent_Keys (Key (Left), Right).
function Equivalent_Keys (Left : Key_Type;
Right : Cursor) return Boolean
with Pre => Right /= No_Element or else raise Constraint_Error,
Global => in all;
Эквивалентно Equivalent_Keys (Left, Key (Right)).
function Iterate (Container : in Map)
return Map_Iterator_Interfaces.Parallel_Iterator'Class
with Post => Tampering_With_Cursors_Prohibited (Container);
Iterate возвращает объект итератора (см. 5.5.1), который сгенерирует значение для параметра цикла (см. 5.5.2), обозначающее каждый узел в Container, начиная с первого узла и перемещая курсор в соответствии с отношением преемника при использовании в качестве итератора вперёд, и обрабатывая все узлы параллельно при использовании в качестве параллельного итератора. Изменение курсоров Container запрещено до тех пор, пока существует объект итератора (в частности, в sequence_of_statements оператора loop_statement, в котором iterator_specification обозначает этот объект). Объект итератора требует завершения.

Рекомендации по реализации

Если N — длина карты, средняя временная сложность подпрограмм Element, Insert, Include, Replace, Delete, Exclude и Find, которые принимают параметр ключа, должна составлять O(log N). Средняя временная сложность подпрограмм, которые принимают параметр курсора, должна составлять O(1). Средняя временная сложность Reserve_Capacity должна составлять O(N).


Spec-Zone.ru

Настройки Оффлайн Что нового Помощь О нас
Spec-Zone .ru
спецификации, руководства, описания, API