Ada Reference Manual (Ada 2022)
A.18.9 The Generic Package Containers.Ordered_Sets
Static Semantics
The generic library package Containers.Ordered_Sets has the following declaration:
with Ada.Iterator_Interfaces;
generic
type Element_Type is private;
with function "<" (Left, Right : Element_Type) return Boolean is <>;
with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Ordered_Sets
with Preelaborate, Remote_Types,
Nonblocking, Global => in out synchronized is
generic
type Element_Type is private;
with function "<" (Left, Right : Element_Type) return Boolean is <>;
with function "=" (Left, Right : Element_Type) return Boolean is <>;
package Ada.Containers.Ordered_Sets
with Preelaborate, Remote_Types,
Nonblocking, Global => in out synchronized is
function Equivalent_Elements (Left, Right : Element_Type) return Boolean;
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;
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;
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;
with Nonblocking, Global => in all, Use_Formal => null;
function Has_Element (Container : Set; Position : Cursor)
return Boolean
with Nonblocking, Global => null, Use_Formal => null;
return Boolean
with Nonblocking, Global => null, Use_Formal => null;
package Set_Iterator_Interfaces is new
Ada.Iterator_Interfaces (Cursor, Has_Element);
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;
(Container : Set) return Boolean
with Nonblocking, Global => null, Use_Formal => null;
function Empty return Set
is (Empty_Set)
with Post =>
not Tampering_With_Cursors_Prohibited (Empty'Result) and then
Length (Empty'Result) = 0;
is (Empty_Set)
with Post =>
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);
with Post => Length (To_Set'Result) = 1 and then
not Tampering_with_Cursors_Prohibited (To_Set'Result);
function Length (Container : Set) return Count_Type
with Nonblocking, Global => null, Use_Formal => null;
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);
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 => Length (Container) = 0;
with Pre => not Tampering_With_Cursors_Prohibited (Container)
or else raise Program_Error,
Post => 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;
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;
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);
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;
(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);
(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);
(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;
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);
with Pre => not Tampering_With_Cursors_Prohibited (Target)
or else raise Program_Error,
Post => Length (Source) = Length (Target);
function Copy (Source : Set) return Set
with Post => Length (Copy'Result) = Length (Source) and then
not Tampering_With_Cursors_Prohibited (Copy'Result);
with Post => Length (Copy'Result) = Length (Source) and then
not Tampering_With_Cursors_Prohibited (Copy'Result);
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);
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));
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));
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;
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;
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);
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);
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;
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);
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;
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;
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 Delete_First (Container : in out Set)
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));
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));
procedure Delete_Last (Container : in out Set)
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));
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));
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);
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);
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);
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);
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);
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);
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);
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);
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;
Symmetric_Difference;
function Overlap (Left, Right : Set) return Boolean;
function Is_Subset (Subset : Set;
Of_Set : Set) return Boolean;
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);
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 First_Element (Container : Set)
return Element_Type
with Pre => (not Is_Empty (Container)
or else raise Constraint_Error);
return Element_Type
with Pre => (not Is_Empty (Container)
or else raise Constraint_Error);
function Last (Container : Set) 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);
with Nonblocking, Global => null, Use_Formal => null,
Post => (if not Is_Empty (Container) then
Has_Element (Container, Last'Result)
else Last'Result = No_Element);
function Last_Element (Container : Set)
return Element_Type
with Pre => (not Is_Empty (Container)
or else raise Constraint_Error);
return Element_Type
with Pre => (not Is_Empty (Container)
or else raise Constraint_Error);
function Next (Position : Cursor) return Cursor
with Nonblocking, Global => in all, Use_Formal => null,
Post => (if Position = No_Element then Next'Result = No_Element);
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));
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;
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));
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 Previous (Position : Cursor) return Cursor
with Nonblocking, Global => in all, Use_Formal => null,
Post => (if Position = No_Element then
Previous'Result = No_Element);
with Nonblocking, Global => in all, Use_Formal => null,
Post => (if Position = No_Element then
Previous'Result = No_Element);
function Previous (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
Previous'Result = No_Element
elsif Previous'Result = No_Element then
Position = First (Container)
else Has_Element (Container, Previous'Result));
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));
procedure Previous (Position : in out Cursor)
with Nonblocking, Global => in all,
Use_Formal => null;
with Nonblocking, Global => in all,
Use_Formal => null;
procedure Previous (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));
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));
Item : Element_Type) return Cursor
with Post => (if Find'Result /= No_Element
then Has_Element (Container, Find'Result));
function Floor (Container : Set;
Item : Element_Type) return Cursor
with Post => (if Floor'Result /= No_Element
then Has_Element (Container, Floor'Result));
Item : Element_Type) return Cursor
with Post => (if Floor'Result /= No_Element
then Has_Element (Container, Floor'Result));
function Ceiling (Container : Set;
Item : Element_Type) return Cursor
with Post => (if Ceiling'Result /= No_Element
then Has_Element (Container, Ceiling'Result));
Item : Element_Type) return Cursor
with Post => (if Ceiling'Result /= No_Element
then Has_Element (Container, Ceiling'Result));
function Contains (Container : Set;
Item : Element_Type) return Boolean;
Item : Element_Type) return Boolean;
This paragraph was deleted.
function "<" (Left, Right : Cursor) return Boolean
with Pre => (Left /= No_Element and then Right /= No_Element)
or else raise Constraint_Error,
Global => in all;
with Pre => (Left /= No_Element and then Right /= No_Element)
or else raise Constraint_Error,
Global => in all;
function ">" (Left, Right : Cursor) return Boolean
with Pre => (Left /= No_Element and then Right /= No_Element)
or else raise Constraint_Error,
Global => in all;
with Pre => (Left /= No_Element and then Right /= No_Element)
or else raise Constraint_Error,
Global => in all;
function "<" (Left : Cursor; Right : Element_Type) return Boolean
with Pre => Left /= No_Element or else raise Constraint_Error,
Global => in all;
with Pre => Left /= No_Element or else raise Constraint_Error,
Global => in all;
function ">" (Left : Cursor; Right : Element_Type) return Boolean
with Pre => Left /= No_Element or else raise Constraint_Error,
Global => in all;
with Pre => Left /= No_Element or else raise Constraint_Error,
Global => in all;
function "<" (Left : Element_Type; Right : Cursor) return Boolean
with Pre => Right /= No_Element or else raise Constraint_Error,
Global => in all;
with Pre => Right /= No_Element or else raise Constraint_Error,
Global => in all;
function ">" (Left : Element_Type; Right : Cursor) return Boolean
with Pre => Right /= No_Element or else raise Constraint_Error,
Global => in all;
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;
(Container : in Set;
Process : not null access procedure (Position : in Cursor))
with Allows_Exit;
procedure Reverse_Iterate
(Container : in Set;
Process : not null access procedure (Position : in Cursor))
with Allows_Exit;
(Container : in Set;
Process : not null access procedure (Position : in Cursor))
with Allows_Exit;
function Iterate (Container : in Set)
return Set_Iterator_Interfaces.Parallel_Reversible_Iterator'Class
with Post => Tampering_With_Cursors_Prohibited (Container);
return Set_Iterator_Interfaces.Parallel_Reversible_Iterator'Class
with Post => Tampering_With_Cursors_Prohibited (Container);
function Iterate (Container : in Set; Start : in Cursor)
return Set_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);
return Set_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);
generic
type Key_Type (<>) is private;
with function Key (Element : Element_Type) return Key_Type;
with function "<" (Left, Right : Key_Type)
return Boolean is <>;
package Generic_Keys
with Nonblocking, Global => null is
type Key_Type (<>) is private;
with function Key (Element : Element_Type) return Key_Type;
with function "<" (Left, Right : Key_Type)
return Boolean is <>;
package Generic_Keys
with Nonblocking, Global => null is
function Equivalent_Keys (Left, Right : Key_Type)
return Boolean;
return Boolean;
function Key (Position : Cursor) return Key_Type
with Pre => Position /= No_Element or else raise Constraint_Error,
Global => in all;
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);
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;
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;
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);
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;
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));
Key : Key_Type) return Cursor
with Post => (if Find'Result /= No_Element
then Has_Element (Container, Find'Result));
function Floor (Container : Set;
Key : Key_Type) return Cursor
with Post => (if Floor'Result /= No_Element
then Has_Element (Container, Floor'Result));
Key : Key_Type) return Cursor
with Post => (if Floor'Result /= No_Element
then Has_Element (Container, Floor'Result));
function Ceiling (Container : Set;
Key : Key_Type) return Cursor
with Post => (if Ceiling'Result /= No_Element
then Has_Element (Container, Ceiling'Result));
Key : Key_Type) return Cursor
with Post => (if Ceiling'Result /= No_Element
then Has_Element (Container, Ceiling'Result));
function Contains (Container : Set;
Key : Key_Type) return Boolean;
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);
(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);
(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);;
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);;
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);;
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 Ordered_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;
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;
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;
with Nonblocking, Global => in all, Use_Formal => null;
package Set_Iterator_Interfaces is new
Ada.Iterator_Interfaces (Cursor, Has_Element);
Ada.Iterator_Interfaces (Cursor, Has_Element);
procedure Assign (Target : in out Ordered_Sets.Set;
Source : in Set)
with Post => Length (Source) = Length (Target);
Source : in Set)
with Post => Length (Source) = Length (Target);
function Copy (Source : Ordered_Sets.Set) return Set
with Post => Length (Copy'Result) = Length (Source);
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);
(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.
-- are declared here.
private
... -- not specified by the language
end Stable;
private
... -- not specified by the language
end Ada.Containers.Ordered_Sets;
Two elements E1 and E2 are equivalent if both E1 < E2 and E2 < E1 return False, using the generic formal "<" operator for elements. Function Equivalent_Elements returns True if Left and Right are equivalent, and False otherwise.
The actual function for the generic formal function "<" on Element_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.
If the actual function for the generic formal function "=" returns True for any pair of nonequivalent elements, then the behavior of the container function "=" 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 "<" or "=" give different results, the behavior of this package is unspecified.
The first element of a nonempty set is the one which is less than all the other elements in the set. The last element of a nonempty set is the one which is greater than all the other elements in the set. The successor of an element is the smallest element that is larger than the given element. The predecessor of an element is the largest element that is smaller than the given element. All comparisons are done using the generic formal "<" operator for elements.
function Copy (Source : Set) return Set
with Post => Length (Copy'Result) = Length (Source) and then
not Tampering_With_Cursors_Prohibited (Copy'Result);
with Post => Length (Copy'Result) = Length (Source) and then
not Tampering_With_Cursors_Prohibited (Copy'Result);
Returns a set whose elements are initialized from the corresponding elements of Source.
procedure Delete_First (Container : in out Set)
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));
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));
If Container is empty, Delete_First has no effect. Otherwise, the element designated by First (Container) is removed from Container. Delete_First tampers with the cursors of Container.
procedure Delete_Last (Container : in out Set)
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));
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));
If Container is empty, Delete_Last has no effect. Otherwise, the element designated by Last (Container) is removed from Container. Delete_Last tampers with the cursors of Container.
function First_Element (Container : Set) return Element_Type
with Pre => (not Is_Empty (Container)
or else raise Constraint_Error);
with Pre => (not Is_Empty (Container)
or else raise Constraint_Error);
Equivalent to Element (First (Container)).
function Last (Container : Set) 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);
with Nonblocking, Global => null, Use_Formal => null,
Post => (if not Is_Empty (Container) then
Has_Element (Container, Last'Result)
else Last'Result = No_Element);
Returns a cursor that designates the last element in Container. If Container is empty, returns No_Element.
function Last_Element (Container : Set) return Element_Type
with Pre => (not Is_Empty (Container)
or else raise Constraint_Error);
with Pre => (not Is_Empty (Container)
or else raise Constraint_Error);
Equivalent to Element (Last (Container)).
function Previous (Position : Cursor) return Cursor
with Nonblocking, Global => in all, Use_Formal => null,
Post => (if Position = No_Element then
Previous'Result = No_Element);
with Nonblocking, Global => in all, Use_Formal => null,
Post => (if Position = No_Element then
Previous'Result = No_Element);
If Position equals No_Element, then Previous returns No_Element. Otherwise, Previous returns a cursor designating the predecessor element of the one designated by Position. If Position designates the first element, then Previous returns No_Element.
function Previous (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
Previous'Result = No_Element
elsif Previous'Result = No_Element then
Position = First (Container)
else Has_Element (Container, Previous'Result));
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));
Returns a cursor designating the predecessor of the node designated by Position in Container, if any.
procedure Previous (Position : in out Cursor)
with Nonblocking, Global => in all, Use_Formal => null;
with Nonblocking, Global => in all, Use_Formal => null;
Equivalent to Position := Previous (Position).
procedure Previous (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));
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));
Equivalent to Position := Previous (Container, Position).
function Floor (Container : Set;
Item : Element_Type) return Cursor
with Post => (if Floor'Result /= No_Element
then Has_Element (Container, Floor'Result));
Item : Element_Type) return Cursor
with Post => (if Floor'Result /= No_Element
then Has_Element (Container, Floor'Result));
Floor searches for the last element which is not greater than Item. If such an element is found, a cursor that designates it is returned. Otherwise, No_Element is returned.
function Ceiling (Container : Set;
Item : Element_Type) return Cursor
with Post => (if Ceiling'Result /= No_Element
then Has_Element (Container, Ceiling'Result));
Item : Element_Type) return Cursor
with Post => (if Ceiling'Result /= No_Element
then Has_Element (Container, Ceiling'Result));
Ceiling searches for the first element which is not less than Item. If such an element is found, a cursor that designates it is returned. Otherwise, No_Element is returned.
function "<" (Left, Right : Cursor) return Boolean
with Pre => (Left /= No_Element and then Right /= No_Element)
or else raise Constraint_Error,
Global => in all;
with Pre => (Left /= No_Element and then Right /= No_Element)
or else raise Constraint_Error,
Global => in all;
Equivalent to Element (Left) < Element (Right).
function ">" (Left, Right : Cursor) return Boolean
with Pre => (Left /= No_Element and then Right /= No_Element)
or else raise Constraint_Error,
Global => in all;
with Pre => (Left /= No_Element and then Right /= No_Element)
or else raise Constraint_Error,
Global => in all;
Equivalent to Element (Right) < Element (Left).
function "<" (Left : Cursor; Right : Element_Type) return Boolean
with Pre => Left /= No_Element or else raise Constraint_Error,
Global => in all;
with Pre => Left /= No_Element or else raise Constraint_Error,
Global => in all;
Equivalent to Element (Left) < Right.
function ">" (Left : Cursor; Right : Element_Type) return Boolean
with Pre => Left /= No_Element or else raise Constraint_Error,
Global => in all;
with Pre => Left /= No_Element or else raise Constraint_Error,
Global => in all;
Equivalent to Right < Element (Left).
function "<" (Left : Element_Type; Right : Cursor) return Boolean
with Pre => Right /= No_Element or else raise Constraint_Error,
Global => in all;
with Pre => Right /= No_Element or else raise Constraint_Error,
Global => in all;
Equivalent to Left < Element (Right).
function ">" (Left : Element_Type; Right : Cursor) return Boolean
with Pre => Right /= No_Element or else raise Constraint_Error,
Global => in all;
with Pre => Right /= No_Element or else raise Constraint_Error,
Global => in all;
Equivalent to Element (Right) < Left.
procedure Reverse_Iterate
(Container : in Set;
Process : not null access procedure (Position : in Cursor))
with Allows_Exit;
(Container : in Set;
Process : not null access procedure (Position : in Cursor))
with Allows_Exit;
Iterates over the elements in Container as per procedure Iterate, with the difference that the elements are traversed in predecessor order, starting with the last element.
function Iterate (Container : in Set)
return Set_Iterator_Interfaces.Parallel_Reversible_Iterator'Class
with Post => Tampering_With_Cursors_Prohibited (Container);
return Set_Iterator_Interfaces.Parallel_Reversible_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 starting with the last element 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.
function Iterate (Container : in Set; Start : in Cursor)
return Set_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);
return Set_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);
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 element in Container, starting with the element 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.
For any two elements E1 and E2, the boolean values (E1 < E2) and (Key(E1) < Key(E2)) are expected to be equal. If the actuals for Key or Generic_Keys."<" behave in some other manner, the behavior of this package is unspecified. Which subprograms of this package call Key and Generic_Keys."<", and how many times the functions are called, is unspecified.
In addition to the semantics described in A.18.7, the subprograms in package Generic_Keys named Floor and Ceiling, are equivalent to the corresponding subprograms in the parent package, with the difference that the Key subprogram parameter is compared to elements in the container using the Key and "<" generic formal functions. The function named Equivalent_Keys in package Generic_Keys returns True if both Left < Right and Right < Left return False using the generic formal "<" operator, and returns True otherwise.
Implementation Advice
If N is the length of a set, then the worst-case time complexity of the Insert, Include, Replace, Delete, Exclude, and Find operations that take an element 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).