A.18.5 The Generic Package Containers.Hashed_Maps
Static Semantics
The generic library
package Containers.Hashed_Maps has the following declaration:
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 :=
implementation-defined)
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);
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);
procedure 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);
procedure 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);
procedure 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);
procedure 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;
procedure 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);
procedure 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;
procedure 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;
function 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);
function Next (Position : Cursor)
return Cursor
with Nonblocking, Global =>
in all, Use_Formal =>
null,
Post => (
if Position = No_Element
then Next'Result = No_Element);
function 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));
procedure Next (Position :
in out Cursor)
with Nonblocking, Global =>
in all, Use_Formal =>
null;
procedure 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));
function Find (Container : Map;
Key : Key_Type)
return Cursor
with Post => (
if Find'Result /= No_Element
then Has_Element (Container, Find'Result));
function Element (Container : Map;
Key : Key_Type)
return Element_Type;
function Contains (Container : Map;
Key : Key_Type)
return Boolean;
This paragraph
was deleted.
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;
function Equivalent_Keys (Left : Cursor;
Right : Key_Type)
return Boolean
with Pre => Left /= No_Element
or else raise Constraint_Error,
Global =>
in all;
function Equivalent_Keys (Left : Key_Type;
Right : Cursor)
return Boolean
with Pre => Right /= No_Element
or else raise Constraint_Error,
Global =>
in all;
procedure Iterate
(Container :
in Map;
Process :
not null access procedure (Position :
in Cursor))
with Allows_Exit;
function Iterate (Container : in Map)
return Map_Iterator_Interfaces.Parallel_Iterator'Class
with Post => Tampering_With_Cursors_Prohibited (Container);
type Map (Base :
not null access Hashed_Maps.Map)
is
tagged limited private
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;
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;
package Map_Iterator_Interfaces
is new
Ada.Iterator_Interfaces (Cursor, Has_Element);
procedure Assign (Target :
in out Hashed_Maps.Map;
Source :
in Map)
with Post => Length (Source) = Length (Target);
function Copy (Source : Hashed_Maps.Map)
return Map
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);
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);
-- Additional subprograms as described in the text
-- are declared here.
private
... -- not specified by the language
end Stable;
private
... -- not specified by the language
end Ada.Containers.Hashed_Maps;
An object of type Map contains an expandable hash
table, which is used to provide direct access to nodes. The
capacity
of an object of type Map is the maximum number of nodes that can be inserted
into the hash table prior to it being automatically expanded.
Two keys
K1 and
K2
are defined to be
equivalent if Equivalent_Keys (
K1,
K2)
returns True.
The actual function for the generic formal function
Hash is expected to return the same value each time it is called with
a particular key value. For any two equivalent key values, the actual
for Hash is expected to return the same value. If the actual for Hash
behaves in some other manner, the behavior of this package is unspecified.
Which subprograms of this package call Hash, and how many times they
call it, is unspecified.
The actual function for the generic formal function
Equivalent_Keys on Key_Type values is expected to return the same value
each time it is called with a particular pair of key values. It should
define an equivalence relationship, that is, be reflexive, symmetric,
and transitive. If the actual for Equivalent_Keys behaves in some other
manner, the behavior of this package is unspecified. Which subprograms
of this package call Equivalent_Keys, and how many times they call it,
is unspecified.
If the value of a key stored in a node of a map is
changed other than by an operation in this package such that at least
one of Hash or Equivalent_Keys give different results, the behavior of
this package is unspecified.
Which
nodes are the first node and the last node of a map, and which node is
the successor of a given node, are unspecified, other than the general
semantics described in
A.18.4.
function Empty (Capacity : Count_Type := implementation-defined)
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;
Returns an empty
map.
function Capacity (Container : Map) return Count_Type
with Nonblocking, Global => null, Use_Formal => null;
Returns the capacity
of 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 allocates a new hash table such
that the length of the resulting map can become at least the value Capacity
without requiring an additional call to Reserve_Capacity, and is large
enough to hold the current length of Container. Reserve_Capacity then
rehashes the nodes in Container onto the new hash table. It replaces
the old hash table with the new hash table, and then deallocates the
old hash table. Any exception raised during allocation is propagated
and Container is not modified.
This
paragraph was deleted.
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;
In addition to the
semantics described in
A.18.4, Clear does
not affect the capacity of 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);
In addition to the
semantics described in
A.18.4, if the length
of Source is greater than the capacity of Target, Reserve_Capacity (Target,
Length (Source)) is called before assigning any elements.
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);
Returns a map whose
keys and elements are initialized from the keys and elements of 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);
In addition to the
semantics described in
A.18.4, if Length
(Container) equals Capacity (Container), then Insert first calls Reserve_Capacity
to increase the capacity of Container to some larger value.
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 to 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 to 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 to 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 returns
an iterator object (see
5.5.1) that will
generate a value for a loop parameter (see
5.5.2)
designating each node in Container, starting with the first node and
moving the cursor according to the successor relation when used as a
forward iterator, and processing all nodes concurrently when used as
a parallel iterator. Tampering with the cursors of Container is prohibited
while the iterator object exists (in particular, in the
sequence_of_statements
of the
loop_statement
whose
iterator_specification
denotes this object). The iterator object needs finalization.
Implementation Advice
If N is the length of a map, the average time
complexity of the subprograms Element, Insert, Include, Replace, Delete,
Exclude, and Find that take a key parameter should be O(log N).
The average time complexity of the subprograms that take a cursor parameter
should be O(1). The average time complexity of Reserve_Capacity
should be O(N).
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe
