Ada Conformity Assessment Authority      Home Conformity Assessment   Test Suite ARGAda Standard
 
Ada Reference Manual (Ada 202x Draft 25)Legal Information
Contents   Index   References   Search   Previous   Next 

A.18.5 The Generic Package Containers.Hashed_Maps

Static Semantics

1/2
The generic library package Containers.Hashed_Maps has the following declaration: 
2/5
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 => null is
3/5
   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));
   pragma Preelaborable_Initialization(Map);
4/2
   type Cursor is private;
   pragma Preelaborable_Initialization(Cursor);
5/2
   Empty_Map : constant Map;
6/2
   No_Element : constant Cursor;
6.1/5
   function Has_Element (Position : Cursor) return Boolean
      with Nonblocking, Global => (in alluse null);
6.2/5
   function Has_Element (Container : Map; Position : Cursor)
      return Boolean
      with Nonblocking, Global => (nulluse null);
6.3/5
   package Map_Iterator_Interfaces is new
       Ada.Iterator_Interfaces (Cursor, Has_Element);
7/2
   function "=" (Left, Right : Map) return Boolean;
7.1/5
   function Tampering_With_Cursors_Prohibited
      (Container : Map) return Boolean
      with Nonblocking, Global => (nulluse null);
7.2/5
   function Tampering_With_Elements_Prohibited
      (Container : Map) return Boolean
      with Nonblocking, Global => (nulluse null);
7.3/5
   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;
8/5
   function Capacity (Container : Map) return Count_Type
      with Nonblocking, Global => (nulluse null);
9/5
   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;
10/5
   function Length (Container : Map) return Count_Type
      with Nonblocking, Global => (nulluse null);
11/5
   function Is_Empty (Container : Map) return Boolean
      with Nonblocking, Global => (nulluse null),
           Post => Is_Empty'Result = (Length (Container) = 0);
12/5
   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;
13/5
   function Key (Position : Cursor) return Key_Type
      with Pre  => Position /= No_Element or else raise Constraint_Error,
           Nonblocking => Key_Type'Nonblocking,
           Global => (in alluse Key_Type);
13.1/5
   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 => Key_Type'Nonblocking,
           Global => (nulluse Key_Type);
14/5
   function Element (Position : Cursor) return Element_Type
      with Pre  => Position /= No_Element or else raise Constraint_Error,
           Nonblocking => Element_Type'Nonblocking,
           Global => (in alluse Element_Type);
14.1/5
   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 => Element_Type'Nonblocking,
           Global => (nulluse Element_Type);
15/5
   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);
16/5
   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;
16.1/5
   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);
17/5
   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);
17.1/5
   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);
17.2/5
   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);
17.3/5
   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 => (nulluse null);
17.4/5
   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 => (nulluse null);
17.5/5
   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 => (nulluse null);
17.6/5
   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 => (nulluse null);
17.7/5
   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);
17.8/5
   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);
18/5
   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 Target = Source then True
                    else
                       Length (Target) = Length (Source'Old) and then
                       Length (Source) = 0);
19/5
   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);
20/5
   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);
21/5
   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);
22/5
   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);
23/5
   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;
24/5
   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);
25/5
   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;
26/5
   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;
27/5
   function First (Container : Map) return Cursor
      with Nonblocking, Global => (nulluse null),
           Post => (if not Is_Empty (Container)
                    then Has_Element (Container, First'Result)
                    else First'Result = No_Element);
28/5
   function Next (Position : Cursor) return Cursor
      with Nonblocking, Global => (in alluse null),
           Post => (if Position = No_Element then Next'Result = No_Element
                    else True);
28.1/5
   function Next (Container : Map;
                  Position : Cursor) return Cursor
      with Nonblocking, Global => (nulluse 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));
29/5
   procedure Next (Position : in out Cursor)
      with Nonblocking, Global => (in alluse null);
29.1/5
   procedure Next (Container : in     Map;
                   Position  : in out Cursor)
      with Nonblocking, Global => (nulluse 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));
30/5
   function Find (Container : Map;
                  Key       : Key_Type)
      return Cursor
      with Post => (if Find'Result = No_Element then True
                    else Has_Element (Container, Find'Result));
31/2
   function Element (Container : Map;
                     Key       : Key_Type)
      return Element_Type;
32/2
   function Contains (Container : Map;
                      Key       : Key_Type) return Boolean;
33/3
This paragraph was deleted.
34/5
   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;
35/5
   function Equivalent_Keys (Left  : Cursor;
                             Right : Key_Type)
      return Boolean
      with Pre    => Left /= No_Element or else raise Constraint_Error,
           Global => in all;
36/5
   function Equivalent_Keys (Left  : Key_Type;
                             Right : Cursor)
      return Boolean
      with Pre    => Right /= No_Element or else raise Constraint_Error,
           Global => in all;
37/5
   procedure Iterate
     (Container : in Map;
      Process   : not null access procedure (Position : in Cursor))
      with Allows_Exit;
37.1/5
   function Iterate (Container : in Map)
      return Map_Iterator_Interfaces.Parallel_Iterator'Class
      with Post => Tampering_With_Cursors_Prohibited (Container);
37.2/5
   package Stable is
37.3/5
      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,
              Aggregate         => (Empty      => Empty,
                                    Add_Named  => Insert),
              Stable_Properties => (Length),
      Global => null,
              Default_Initial_Condition => Length (Map) = 0;
      pragma Preelaborable_Initialization(Map);
37.4/5
      type Cursor is private;
      pragma Preelaborable_Initialization(Cursor);
37.5/5
      Empty_Map : constant Map;
37.6/5
      No_Element : constant Cursor;
37.7/5
      function Has_Element (Position : Cursor) return Boolean
         with Nonblocking, Global => (in alluse null);
37.8/5
      package Map_Iterator_Interfaces is new
         Ada.Iterator_Interfaces (Cursor, Has_Element);
37.9/5
      procedure Assign (Target : in out Hashed_Maps.Map;
                        Source : in Map)
         with Post => Length (Source) = Length (Target);
37.10/5
      function Copy (Source : Hashed_Maps.Map) return Map
         with Post => Length (Copy'Result) = Length (Source);
37.11/5
      type Constant_Reference_Type
            (Element : not null access constant Element_Type) is private
         with Implicit_Dereference => Element,
              Nonblocking, Global => (nulluse null),
              Default_Initial_Condition => (raise Program_Error);
37.12/5
      type Reference_Type
            (Element : not null access Element_Type) is private
         with Implicit_Dereference => Element,
              Nonblocking, Global => (nulluse null),
              Default_Initial_Condition => (raise Program_Error);
37.13/5
      -- Additional subprograms as described in the text
      -- are declared here.
37.14/5
   private
37.15/5
      ... -- not specified by the language
37.16/5
   end Stable;
38/2
private
39/2
   ... -- not specified by the language
40/2
end Ada.Containers.Hashed_Maps;
41/2
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.
42/2
Two keys K1 and K2 are defined to be equivalent if Equivalent_Keys (K1, K2) returns True.
43/2
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.
44/2
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.
45/2
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.
46/2
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.
46.1/5
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;
46.2/2
Returns an empty map.
47/5
function Capacity (Container : Map) return Count_Type
   with Nonblocking, Global => (nulluse null);
48/2
Returns the capacity of Container.
49/5
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;
50/2
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.
51/5
This paragraph was deleted.
52/5
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;
53/2
In addition to the semantics described in A.18.4, Clear does not affect the capacity of Container.
53.1/5
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);
53.2/3
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.
53.3/5
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);
53.4/5
Returns a map whose keys and elements are initialized from the keys and elements of Source.
54/5
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);
55/2
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.
56/5
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;
57/2
Equivalent to Equivalent_Keys (Key (Left), Key (Right)).
58/5
function Equivalent_Keys (Left  : Cursor;
                          Right : Key_Type) return Boolean
   with Pre    => Left /= No_Element or else raise Constraint_Error,
        Global => in all;
59/2
Equivalent to Equivalent_Keys (Key (Left), Right).
60/5
function Equivalent_Keys (Left  : Key_Type;
                          Right : Cursor) return Boolean
   with Pre    => Right /= No_Element or else raise Constraint_Error,
        Global => in all;
61/2
Equivalent to Equivalent_Keys (Left, Key (Right)).
61.1/5
function Iterate (Container : in Map)
   return Map_Iterator_Interfaces.Parallel_Iterator'Class
   with Post => Tampering_With_Cursors_Prohibited (Container);
61.2/5
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

62/2
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). 

Contents   Index   References   Search   Previous   Next 
Ada-Europe Ada 2005 and 2012 Editions sponsored in part by Ada-Europe