Ada Reference Manual (Ada 2022)Legal Information
Contents   Index   References   Search   Previous   Next 

A.18.6 The Generic Package Containers.Ordered_Maps

Static Semantics

1/2
The generic library package Containers.Ordered_Maps has the following declaration: 
2/5
with Ada.Iterator_Interfaces;
generic
   type Key_Type is private;
   type Element_Type is private;
   with function "<" (Left, Right : Key_Type) return Boolean is <>;
   with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Ordered_Maps
   with Preelaborate, Remote_Types,
        Nonblocking, Global => in out synchronized is
3/5
   function Equivalent_Keys (Left, Right : Key_Type) return Boolean
      is (not ((Left < Right) or (Right < Left)));
4/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)),
           Preelaborable_Initialization;
5/5
   type Cursor is private
      with Preelaborable_Initialization;
6/2
   Empty_Map : constant Map;
7/2
   No_Element : constant Cursor;
7.1/5
   function Has_Element (Position : Cursor) return Boolean
      with Nonblocking, Global => in all, Use_Formal => null;
7.2/5
   function Has_Element (Container : Map; Position : Cursor)
      return Boolean
      with Nonblocking, Global => null, Use_Formal => null;
7.3/5
   package Map_Iterator_Interfaces is new
       Ada.Iterator_Interfaces (Cursor, Has_Element);
8/2
   function "=" (Left, Right : Map) return Boolean;
8.1/5
   function Tampering_With_Cursors_Prohibited
      (Container : Map) return Boolean
      with Nonblocking, Global => null, Use_Formal => null;
8.2/5
   function Tampering_With_Elements_Prohibited
      (Container : Map) return Boolean
      with Nonblocking, Global => null, Use_Formal => null;
8.3/5
   function Empty return Map
      is (Empty_Map)
      with Post =>
              not Tampering_With_Elements_Prohibited (Empty'Result) and then
              not Tampering_With_Cursors_Prohibited (Empty'Result) and then
              Length (Empty'Result) = 0;
9/5
   function Length (Container : Map) return Count_Type
      with Nonblocking, Global => null, Use_Formal => null;
10/5
   function Is_Empty (Container : Map) return Boolean
      with Nonblocking, Global => null, Use_Formal => null,
           Post => Is_Empty'Result = (Length (Container) = 0);
11/5
   procedure Clear (Container : in out Map)
      with Pre  => not Tampering_With_Cursors_Prohibited (Container)
                       or else raise Program_Error,
           Post => Length (Container) = 0;
12/5
   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;
12.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, Global => null, Use_Formal => Key_Type;
13/5
   function Element (Position : Cursor) return Element_Type
      with Pre  => Position /= No_Element or else raise Constraint_Error,
           Nonblocking, Global => null, Use_Formal => Element_Type;
13.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, Global => null, Use_Formal => Element_Type;
14/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);
15/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;
15.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);
16/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);
16.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);
16.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);
16.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 => null, Use_Formal => null;
16.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 => null, Use_Formal => null;
16.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 => null, Use_Formal => null;
16.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 => null, Use_Formal => null;
16.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);
16.8/5
   function Copy (Source : Map)
      return Map
      with Post =>
         Length (Copy'Result) = Length (Source) and then
         not Tampering_With_Elements_Prohibited (Copy'Result) and then
         not Tampering_With_Cursors_Prohibited (Copy'Result);
17/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 not Target'Has_Same_Storage (Source) then
                       Length (Target) = Length (Source'Old) and then
                       Length (Source) = 0);
18/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));
19/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));
20/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;
21/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);
22/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;
23/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);
24/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;
25/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;
26/5
   procedure Delete_First (Container : in out Map)
      with Pre  => not Tampering_With_Cursors_Prohibited (Container)
                       or else raise Program_Error,
           Post => (declare
                      Original_Length : constant Count_Type :=
                         Length (Container)'Old;
                    begin
                      (if Original_Length = 0 then Length (Container) = 0
                       else Length (Container) = Original_Length - 1));
27/5
   procedure Delete_Last (Container : in out Map)
      with Pre  => not Tampering_With_Cursors_Prohibited (Container)
                       or else raise Program_Error,
           Post => (declare
                      Original_Length : constant Count_Type :=
                         Length (Container)'Old;
                    begin
                      (if Original_Length = 0 then Length (Container) = 0
                       else Length (Container) = Original_Length - 1));
28/5
   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);
29/5
   function First_Element (Container : Map) return Element_Type
      with Pre => (not Is_Empty (Container) 
                      or else raise Constraint_Error);
30/5
   function First_Key (Container : Map) return Key_Type
      with Pre => (not Is_Empty (Container) 
                      or else raise Constraint_Error);
31/5
   function Last (Container : Map) return Cursor
      with Nonblocking, Global => null, Use_Formal => null,
           Post => (if not Is_Empty (Container)
                    then Has_Element (Container, Last'Result)
                    else Last'Result = No_Element);
32/5
   function Last_Element (Container : Map) return Element_Type
      with Pre => (not Is_Empty (Container) 
                      or else raise Constraint_Error);
33/5
   function Last_Key (Container : Map) return Key_Type
      with Pre => (not Is_Empty (Container) 
                      or else raise Constraint_Error);
34/5
   function Next (Position : Cursor) return Cursor
      with Nonblocking, Global => in all, Use_Formal => null,
           Post => (if Position = No_Element then Next'Result = No_Element);
34.1/5
   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));
35/5
   procedure Next (Position : in out Cursor)
      with Nonblocking, Global => in all, Use_Formal => null;
35.1/5
   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));
36/5
   function Previous (Position : Cursor) return Cursor
      with Nonblocking, Global => in all, Use_Formal => null,
           Post => (if Position = No_Element then
                       Previous'Result = No_Element);
36.1/5
   function Previous (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
                      Previous'Result = No_Element
                    elsif Previous'Result = No_Element then
                      Position = First (Container)
                    else Has_Element (Container, Previous'Result));
37/5
   procedure Previous (Position : in out Cursor)
      with Nonblocking, Global => in all, Use_Formal => null;
37.1/5
   procedure Previous (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));
38/5
   function Find (Container : Map;
                  Key       : Key_Type) return Cursor
      with Post => (if Find'Result /= No_Element
                    then Has_Element (Container, Find'Result));
39/2
   function Element (Container : Map;
                     Key       : Key_Type) return Element_Type;
40/5
   function Floor (Container : Map;
                   Key       : Key_Type) return Cursor
      with Post => (if Floor'Result /= No_Element
                    then Has_Element (Container, Floor'Result));
41/5
   function Ceiling (Container : Map;
                     Key       : Key_Type) return Cursor
      with Post => (if Ceiling'Result /= No_Element
                    then Has_Element (Container, Ceiling'Result));
42/2
   function Contains (Container : Map;
                      Key       : Key_Type) return Boolean;
43/3
This paragraph was deleted.
44/5
   function "<" (Left, Right : Cursor) return Boolean
      with Pre    => (Left /= No_Element and then Right /= No_Element)
                         or else raise Constraint_Error,
           Global => in all;
45/5
   function ">" (Left, Right : Cursor) return Boolean
      with Pre    => (Left /= No_Element and then Right /= No_Element)
                         or else raise Constraint_Error,
           Global => in all;
46/5
   function "<" (Left : Cursor; Right : Key_Type) return Boolean
      with Pre    => Left /= No_Element or else raise Constraint_Error,
           Global => in all;
47/5
   function ">" (Left : Cursor; Right : Key_Type) return Boolean
      with Pre    => Left /= No_Element or else raise Constraint_Error,
           Global => in all;
48/5
   function "<" (Left : Key_Type; Right : Cursor) return Boolean
      with Pre    => Right /= No_Element or else raise Constraint_Error,
           Global => in all;
49/5
   function ">" (Left : Key_Type; Right : Cursor) return Boolean
      with Pre    => Right /= No_Element or else raise Constraint_Error,
           Global => in all;
50/5
   procedure  Iterate
     (Container : in Map;
      Process   : not null access procedure (Position : in Cursor))
      with Allows_Exit;
51/5
   procedure Reverse_Iterate
     (Container : in Map;
      Process   : not null access procedure (Position : in Cursor))
      with Allows_Exit;
51.1/5
   function Iterate (Container : in Map)
      return Map_Iterator_Interfaces.Parallel_Reversible_Iterator'Class
      with Post => Tampering_With_Cursors_Prohibited (Container);
51.2/5
   function Iterate (Container : in Map; Start : in Cursor)
      return Map_Iterator_Interfaces.Reversible_Iterator'Class
      with Pre  => (Start /= No_Element
                      or else raise Constraint_Error) and then
                   (Has_Element (Container, Start)
                      or else raise Program_Error),
           Post => Tampering_With_Cursors_Prohibited (Container);
51.3/5
   package Stable is
51.4/5
      type Map (Base : not null access Ordered_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;
51.5/5
      type Cursor is private
         with Preelaborable_Initialization;
51.6/5
      Empty_Map : constant Map;
51.7/5
      No_Element : constant Cursor;
51.8/5
      function Has_Element (Position : Cursor) return Boolean
         with Nonblocking, Global => in all, Use_Formal => null;
51.9/5
      package Map_Iterator_Interfaces is new
         Ada.Iterator_Interfaces (Cursor, Has_Element);
51.10/5
      procedure Assign (Target : in out Ordered_Maps.Map;
                        Source : in Map)
         with Post => Length (Source) = Length (Target);
51.11/5
      function Copy (Source : Ordered_Maps.Map) return Map
         with Post => Length (Copy'Result) = Length (Source);
51.12/5
      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);
51.13/5
      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);
51.14/5
      -- Additional subprograms as described in the text
      -- are declared here.
51.15/5
   private
51.16/5
      ... -- not specified by the language
51.17/5
   end Stable;
52/2
private
53/2
   ... -- not specified by the language
54/2
end Ada.Containers.Ordered_Maps;
55/2
Two keys K1 and K2 are equivalent if both K1 < K2 and K2 < K1 return False, using the generic formal "<" operator for keys. Function Equivalent_Keys returns True if Left and Right are equivalent, and False otherwise.
56/3
The actual function for the generic formal function "<" 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 a strict weak ordering relationship (see A.18). If the actual for "<" behaves in some other manner, the behavior of this package is unspecified. Which subprograms of this package call "<" and how many times they call it, is unspecified.
57/2
If the value of a key stored in a map is changed other than by an operation in this package such that at least one of "<" or "=" give different results, the behavior of this package is unspecified.
58/3
The first node of a nonempty map is the one whose key is less than the key of all the other nodes in the map. The last node of a nonempty map is the one whose key is greater than the key of all the other elements in the map. The successor of a node is the node with the smallest key that is larger than the key of the given node. The predecessor of a node is the node with the largest key that is smaller than the key of the given node. All comparisons are done using the generic formal "<" operator for keys.
58.1/5
function Copy (Source : Map)
   return Map
   with Post =>
      Length (Copy'Result) = Length (Source) and then
      not Tampering_With_Elements_Prohibited (Copy'Result) and then
      not Tampering_With_Cursors_Prohibited (Copy'Result);
58.2/3
Returns a map whose keys and elements are initialized from the corresponding keys and elements of Source.
59/5
procedure Delete_First (Container : in out Map)
   with Pre  => not Tampering_With_Cursors_Prohibited (Container)
                    or else raise Program_Error,
        Post => (declare
                   Original_Length : constant Count_Type :=
                      Length (Container)'Old;
                 begin
                   (if Original_Length = 0 then Length (Container) = 0
                    else Length (Container) = Original_Length - 1));
60/3
If Container is empty, Delete_First has no effect. Otherwise, the node designated by First (Container) is removed from Container. Delete_First tampers with the cursors of Container.
61/5
procedure Delete_Last (Container : in out Map)
   with Pre  => not Tampering_With_Cursors_Prohibited (Container)
                    or else raise Program_Error,
        Post => (declare
                   Original_Length : constant Count_Type :=
                      Length (Container)'Old;
                 begin
                   (if Original_Length = 0 then Length (Container) = 0
                    else Length (Container) = Original_Length - 1));
62/3
If Container is empty, Delete_Last has no effect. Otherwise, the node designated by Last (Container) is removed from Container. Delete_Last tampers with the cursors of Container.
63/5
function First_Element (Container : Map) return Element_Type
   with Pre => (not Is_Empty (Container) 
                   or else raise Constraint_Error);
64/2
Equivalent to Element (First (Container)).
65/5
function First_Key (Container : Map) return Key_Type
   with Pre => (not Is_Empty (Container) 
                   or else raise Constraint_Error);
66/2
Equivalent to Key (First (Container)).
67/5
function Last (Container : Map) return Cursor
   with Nonblocking, Global => null, Use_Formal => null,
        Post => (if not Is_Empty (Container)
                 then Has_Element (Container, Last'Result)
                 else Last'Result = No_Element);
68/2
Returns a cursor that designates the last node in Container. If Container is empty, returns No_Element.
69/5
function Last_Element (Container : Map) return Element_Type
   with Pre => (not Is_Empty (Container) 
                   or else raise Constraint_Error);
70/2
Equivalent to Element (Last (Container)).
71/5
function Last_Key (Container : Map) return Key_Type
   with Pre => (not Is_Empty (Container) 
                   or else raise Constraint_Error);
72/2
Equivalent to Key (Last (Container)).
73/5
function Previous (Position : Cursor) return Cursor
   with Nonblocking, Global => in all, Use_Formal => null,
        Post => (if Position = No_Element then
                    Previous'Result = No_Element);
74/3
If Position equals No_Element, then Previous returns No_Element. Otherwise, Previous returns a cursor designating the predecessor node of the one designated by Position. If Position designates the first element, then Previous returns No_Element.
74.1/5
function Previous (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
                   Previous'Result = No_Element
                 elsif Previous'Result = No_Element then
                   Position = First (Container)
                 else Has_Element (Container, Previous'Result));
74.2/5
Returns a cursor designating the predecessor of the node designated by Position in Container, if any.
75/5
procedure Previous (Position : in out Cursor)
   with Nonblocking, Global => in all, Use_Formal => null;
76/2
Equivalent to Position := Previous (Position).
76.1/5
procedure Previous (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));
76.2/5
Equivalent to Position := Previous (Container, Position).
77/5
function Floor (Container : Map;
                Key       : Key_Type) return Cursor
   with Post => (if Floor'Result /= No_Element
                 then Has_Element (Container, Floor'Result));
78/3
Floor searches for the last node whose key is not greater than Key, using the generic formal "<" operator for keys. If such a node is found, a cursor that designates it is returned. Otherwise, No_Element is returned.
79/5
function Ceiling (Container : Map;
                  Key       : Key_Type) return Cursor
   with Post => (if Ceiling'Result /= No_Element
                 then Has_Element (Container, Ceiling'Result));
80/3
Ceiling searches for the first node whose key is not less than Key, using the generic formal "<" operator for keys. If such a node is found, a cursor that designates it is returned. Otherwise, No_Element is returned.
81/5
function "<" (Left, Right : Cursor) return Boolean
   with Pre    => (Left /= No_Element and then Right /= No_Element)
                      or else raise Constraint_Error,
        Global => in all;
82/2
Equivalent to Key (Left) < Key (Right).
83/5
function ">" (Left, Right : Cursor) return Boolean
   with Pre    => (Left /= No_Element and then Right /= No_Element)
                      or else raise Constraint_Error,
        Global => in all;
84/2
Equivalent to Key (Right) < Key (Left).
85/5
function "<" (Left : Cursor; Right : Key_Type) return Boolean
   with Pre    => Left /= No_Element or else raise Constraint_Error,
        Global => in all;
86/2
Equivalent to Key (Left) < Right.
87/5
function ">" (Left : Cursor; Right : Key_Type) return Boolean
   with Pre    => Left /= No_Element or else raise Constraint_Error,
           Global => in all;
88/2
Equivalent to Right < Key (Left).
89/5
function "<" (Left : Key_Type; Right : Cursor) return Boolean
   with Pre    => Right /= No_Element or else raise Constraint_Error,
           Global => in all;
90/2
Equivalent to Left < Key (Right).
91/5
function ">" (Left : Key_Type; Right : Cursor) return Boolean
   with Pre    => Right /= No_Element or else raise Constraint_Error,
           Global => in all;
92/2
Equivalent to Key (Right) < Left.
93/5
procedure Reverse_Iterate
  (Container : in Map;
   Process   : not null access procedure (Position : in Cursor))
   with Allows_Exit;
94/3
Iterates over the nodes in Container as per procedure Iterate, with the difference that the nodes are traversed in predecessor order, starting with the last node.
94.1/5
function Iterate (Container : in Map)
   return Map_Iterator_Interfaces.Parallel_Reversible_Iterator'Class
   with Post => Tampering_With_Cursors_Prohibited (Container);
94.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 starting with the last node and moving the cursor according to the predecessor relation when used as a reverse 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.
94.3/5
function Iterate (Container : in Map; Start : in Cursor)
   return Map_Iterator_Interfaces.Reversible_Iterator'Class
   with Pre  => (Start /= No_Element
                   or else raise Constraint_Error) and then
                (Has_Element (Container, Start)
                   or else raise Program_Error),
        Post => Tampering_With_Cursors_Prohibited (Container);
94.4/5
Iterate returns a reversible 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 node designated by Start and moving the cursor according to the successor relation when used as a forward iterator, or moving the cursor according to the predecessor relation when used as a reverse 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

95/2
If N is the length of a map, then the worst-case time complexity of the Element, Insert, Include, Replace, Delete, Exclude, and Find operations that take a key parameter should be O((log N)**2) or better. The worst-case time complexity of the subprograms that take a cursor parameter should be O(1). 

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