The Generic Package Containers.Hashed

with Ada.Iterator_Interfaces;
generic
   type Element_Type is private;
   with function Hash (Element : Element_Type) return Hash_Type;
   with function Equivalent_Elements (Left, Right : Element_Type)
                 return Boolean;
   with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Hashed_Sets
   with Preelaborate, Remote_Types,
        Nonblocking, Global => in out synchronized is

   type Set is tagged private
      with Constant_Indexing => Constant_Reference,
           Default_Iterator  => Iterate,
           Iterator_Element  => Element_Type,
           Iterator_View     => Stable.Set,
           Aggregate         => (Empty       => Empty,
                                 Add_Unnamed => Include),
           Stable_Properties => (Length,
                                 Tampering_With_Cursors_Prohibited),
           Default_Initial_Condition =>
              Length (Set) = 0 and then
              (not Tampering_With_Cursors_Prohibited (Set)),
           Preelaborable_Initialization;

type Cursor is private
with Preelaborable_Initialization;

Empty_Set : constant Set;

No_Element : constant Cursor;

function Has_Element (Position : Cursor) return Boolean
with Nonblocking, Global => in all, Use_Formal => null;

   function Has_Element (Container : Set; Position : Cursor)
      return Boolean
      with Nonblocking, Global => null, Use_Formal => null;

package Set_Iterator_Interfaces is new
Ada.Iterator_Interfaces (Cursor, Has_Element);

function "=" (Left, Right : Set) return Boolean;

function Equivalent_Sets (Left, Right : Set) return Boolean;

   function Tampering_With_Cursors_Prohibited
      (Container : Set) return Boolean
      with Nonblocking, Global => null, Use_Formal => null;

   function Empty (Capacity : Count_Type := implementation-defined)
      return Set
      with Post =>
              Capacity (Empty'Result) >= Capacity and then
              not Tampering_With_Cursors_Prohibited (Empty'Result) and then
              Length (Empty'Result) = 0;

   function To_Set (New_Item : Element_Type) return Set
      with Post => Length (To_Set'Result) = 1 and then
                 not Tampering_with_Cursors_Prohibited (To_Set'Result);

function Capacity (Container : Set) return Count_Type
with Nonblocking, Global => null, Use_Formal => null;

   procedure Reserve_Capacity (Container : in out Set;
                               Capacity  : in     Count_Type)
      with Pre  => not Tampering_With_Cursors_Prohibited (Container)
                      or else raise Program_Error,
           Post => Container.Capacity >= Capacity;

function Length (Container : Set) return Count_Type
with Nonblocking, Global => null, Use_Formal => null;

   function Is_Empty (Container : Set) return Boolean
      with Nonblocking, Global => null, Use_Formal => null,
           Post => Is_Empty'Result = (Length (Container) = 0);

   procedure Clear (Container : in out Set)
      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 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 : Set;
                     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 Set;
                              Position  : in     Cursor;
                              New_item  : in     Element_Type)
      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);

   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;

   procedure Query_Element
     (Container : in Set;
      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);

   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);

   function Constant_Reference (Container : aliased in Set;
                                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;

   procedure Assign (Target : in out Set; Source : in Set)
      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 : Set; Capacity : Count_Type := 0)
      return Set
      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_Cursors_Prohibited (Copy'Result) and then
              Copy'Result.Capacity = (if Capacity = 0 then
                 Length (Source) else Capacity);

   procedure Move (Target : in out Set;
                   Source : in out Set)
      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 Set;
                     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 Set;
                     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 Set;
                      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 Set;
                      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 Set;
                      Item      : in     Element_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 Set;
                     Item      : in     Element_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 Set;
                     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;

   procedure Union (Target : in out Set;
                    Source : in     Set)
      with Pre  => not Tampering_With_Cursors_Prohibited (Target)
                      or else raise Program_Error,
           Post => Length (Target) <= Length (Target)'Old + Length (Source);

   function Union (Left, Right : Set) return Set
      with Post => Length (Union'Result) <=
                      Length (Left) + Length (Right) and then
                   not Tampering_With_Cursors_Prohibited (Union'Result);

function "or" (Left, Right : Set) return Set renames Union;

   procedure Intersection (Target : in out Set;
                           Source : in     Set)
      with Pre  => not Tampering_With_Cursors_Prohibited (Target)
                      or else raise Program_Error,
           Post => Length (Target) <= Length (Target)'Old + Length (Source);

   function Intersection (Left, Right : Set) return Set
      with Post =>
              Length (Intersection'Result) <=
                 Length (Left) + Length (Right) and then
              not Tampering_With_Cursors_Prohibited (Intersection'Result);

function "and" (Left, Right : Set) return Set renames Intersection;

   procedure Difference (Target : in out Set;
                         Source : in     Set)
      with Pre  => not Tampering_With_Cursors_Prohibited (Target)
                      or else raise Program_Error,
           Post => Length (Target) <= Length (Target)'Old + Length (Source);

   function Difference (Left, Right : Set) return Set
      with Post =>
              Length (Difference'Result) <=
                 Length (Left) + Length (Right) and then
              not Tampering_With_Cursors_Prohibited (Difference'Result);

function "-" (Left, Right : Set) return Set renames Difference;

   procedure Symmetric_Difference (Target : in out Set;
                                   Source : in     Set)
      with Pre  => not Tampering_With_Cursors_Prohibited (Target)
                      or else raise Program_Error,
           Post => Length (Target) <= Length (Target)'Old + Length (Source);

   function Symmetric_Difference (Left, Right : Set) return Set
      with Post =>
              Length (Symmetric_Difference'Result) <=
                 Length (Left) + Length (Right) and then
              not Tampering_With_Cursors_Prohibited (
                 Symmetric_Difference'Result);

function "xor" (Left, Right : Set) return Set
renames Symmetric_Difference;

function Overlap (Left, Right : Set) return Boolean;

function Is_Subset (Subset : Set;
Of_Set : Set) return Boolean;

   function First (Container : Set) 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 : Set;
                  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     Set;
                   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 : Set;
                  Item      : Element_Type)
      return Cursor
      with Post => (if Find'Result /= No_Element
                    then Has_Element (Container, Find'Result));

function Contains (Container : Set;
Item : Element_Type) return Boolean;

This paragraph was deleted.

   function Equivalent_Elements (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_Elements (Left  : Cursor;
                                 Right : Element_Type)
      return Boolean
      with Pre    => Left /= No_Element or else raise Constraint_Error,
           Global => in all;

   function Equivalent_Elements (Left  : Element_Type;
                                 Right : Cursor)
      return Boolean
      with Pre    => Right /= No_Element or else raise Constraint_Error,
           Global => in all;

   procedure Iterate
     (Container : in Set;
      Process   : not null access procedure (Position : in Cursor))
      with Allows_Exit;

   function Iterate (Container : in Set)
      return Set_Iterator_Interfaces.Parallel_Iterator'Class
      with Post => Tampering_With_Cursors_Prohibited (Container);

   generic
      type Key_Type (<>) is private;
      with function Key (Element : Element_Type) return Key_Type;
      with function Hash (Key : Key_Type) return Hash_Type;
      with function Equivalent_Keys (Left, Right : Key_Type)
                                     return Boolean;
   package Generic_Keys
   with Nonblocking, Global => null is

      function Key (Position : Cursor) return Key_Type
         with Pre  => Position /= No_Element or else raise Constraint_Error,
              Global => in all;

      function Key (Container : Set;
                    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);

      function Element (Container : Set;
                        Key       : Key_Type)
        return Element_Type;

      procedure Replace (Container : in out Set;
                         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 Set;
                         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 Set;
                        Key       : in     Key_Type)
         with Pre  => not Tampering_With_Cursors_Prohibited (Container)
                          or else raise Program_Error,
              Post => Length (Container) = Length (Container)'Old - 1;

      function Find (Container : Set;
                     Key       : Key_Type)
         return Cursor
         with Post => (if Find'Result = No_Element
                       then Has_Element (Container, Find'Result));

      function Contains (Container : Set;
                         Key       : Key_Type)
         return Boolean;

      procedure Update_Element_Preserving_Key
        (Container : in out Set;
         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);

      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 Reference_Preserving_Key (Container : aliased in out Set;
                                         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);

      function Constant_Reference (Container : aliased in Set;
                                   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);

      function Reference_Preserving_Key (Container : aliased in out Set;
                                         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);

end Generic_Keys;

package Stable is

      type Set (Base : not null access Hashed_Sets.Set) is
         tagged limited private
         with Constant_Indexing => Constant_Reference,
              Default_Iterator  => Iterate,
              Iterator_Element  => Element_Type,
              Stable_Properties => (Length),
              Global            => null,
              Default_Initial_Condition => Length (Set) = 0,
              Preelaborable_Initialization;

type Cursor is private
with Preelaborable_Initialization;

Empty_Set : constant Set;

No_Element : constant Cursor;

function Has_Element (Position : Cursor) return Boolean
with Nonblocking, Global => in all, Use_Formal => null;

package Set_Iterator_Interfaces is new
Ada.Iterator_Interfaces (Cursor, Has_Element);

      procedure Assign (Target : in out Hashed_Sets.Set;
                        Source : in Set)
         with Post => Length (Source) = Length (Target);

function Copy (Source : Hashed_Sets.Set) return Set
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);

-- Additional subprograms as described in the text
-- are declared here.

... -- not specified by the language

end Ada.Containers.Hashed_Sets;

An object of type Set contains an expandable hash table, which is used to provide direct access to elements. The capacity of an object of type Set is the maximum number of elements that can be inserted into the hash table prior to it being automatically expanded.

The actual function for the generic formal function Hash is expected to return the same value each time it is called with a particular element value. For any two equivalent elements, 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_Elements is expected to return the same value each time it is called with a particular pair of Element values. It should define an equivalence relationship, that is, be reflexive, symmetric, and transitive. If the actual for Equivalent_Elements behaves in some other manner, the behavior of this package is unspecified. Which subprograms of this package call Equivalent_Elements, and how many times they call it, is unspecified.

If the value of an element stored in a set is changed other than by an operation in this package such that at least one of Hash or Equivalent_Elements give different results, the behavior of this package is unspecified.

function Empty (Capacity : Count_Type := implementation-defined)
   return Set
   with Post =>
           Capacity (Empty'Result) >= Capacity and then
           not Tampering_With_Cursors_Prohibited (Empty'Result) and then
           Length (Empty'Result) = 0;

function Capacity (Container : Set) return Count_Type
with Nonblocking, Global => null, Use_Formal => null;

procedure Reserve_Capacity (Container : in out Set;
                            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 set 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 elements 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.

procedure Clear (Container : in out Set)
   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 Copy (Source : Set; Capacity : Count_Type := 0)
   return Set
   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_Cursors_Prohibited (Copy'Result) and then
           Copy'Result.Capacity = (if Capacity = 0 then
              Length (Source) else Capacity);

procedure Insert (Container : in out Set;
                  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.7, if Length (Container) equals Capacity (Container), then Insert first calls Reserve_Capacity to increase the capacity of Container to some larger value.

function First (Container : Set) return Cursor;

function Equivalent_Elements (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_Elements (Left  : Cursor;
                              Right : Element_Type) return Boolean
   with Pre    => Left /= No_Element or else raise Constraint_Error,
        Global => in all;

function Equivalent_Elements (Left  : Element_Type;
                              Right : Cursor) return Boolean
   with Pre    => Right /= No_Element or else raise Constraint_Error,
        Global => in all;

function Iterate (Container : in Set)
return Set_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 element in Container, starting with the first element 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.

For any element E, the actual function for the generic formal function Generic_Keys.Hash is expected to be such that Hash (E) = Generic_Keys.Hash (Key (E)). If the actuals for Key or Generic_Keys.Hash behave in some other manner, the behavior of Generic_Keys is unspecified. Which subprograms of Generic_Keys call Generic_Keys.Hash, and how many times they call it, is unspecified.

For any two elements E1 and E2, the boolean values Equivalent_Elements (E1, E2) and Equivalent_Keys (Key (E1), Key (E2)) are expected to be equal. If the actuals for Key or Equivalent_Keys behave in some other manner, the behavior of Generic_Keys is unspecified. Which subprograms of Generic_Keys call Equivalent_Keys, and how many times they call it, is unspecified.

Implementation Advice

If N is the length of a set, the average time complexity of the subprograms Insert, Include, Replace, Delete, Exclude, and Find that take an element 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).

A.18.8 The Generic Package Containers.Hashed_Sets

Static Semantics

Implementation Advice