1 ------------------------------------------------------------------------------
3 -- GNAT LIBRARY COMPONENTS --
5 -- A D A . C O N T A I N E R S . F O R M A L _ H A S H E D _ S E T S --
9 -- Copyright (C) 2004-2011, Free Software Foundation, Inc. --
11 -- This specification is derived from the Ada Reference Manual for use with --
12 -- GNAT. The copyright notice above, and the license provisions that follow --
13 -- apply solely to the contents of the part following the private keyword. --
15 -- GNAT is free software; you can redistribute it and/or modify it under --
16 -- terms of the GNU General Public License as published by the Free Soft- --
17 -- ware Foundation; either version 3, or (at your option) any later ver- --
18 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
19 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
20 -- or FITNESS FOR A PARTICULAR PURPOSE. --
22 -- As a special exception under Section 7 of GPL version 3, you are granted --
23 -- additional permissions described in the GCC Runtime Library Exception, --
24 -- version 3.1, as published by the Free Software Foundation. --
26 -- You should have received a copy of the GNU General Public License and --
27 -- a copy of the GCC Runtime Library Exception along with this program; --
28 -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
29 -- <http://www.gnu.org/licenses/>. --
30 ------------------------------------------------------------------------------
32 -- This spec is derived from package Ada.Containers.Bounded_Hashed_Sets in the
33 -- Ada 2012 RM. The modifications are to facilitate formal proofs by making it
34 -- easier to express properties.
36 -- The modifications are:
38 -- A parameter for the container is added to every function reading the
39 -- content of a container: Element, Next, Query_Element, Has_Element, Key,
40 -- Iterate, Equivalent_Elements. This change is motivated by the need to
41 -- have cursors which are valid on different containers (typically a
42 -- container C and its previous version C'Old) for expressing properties,
43 -- which is not possible if cursors encapsulate an access to the underlying
46 -- There are three new functions:
48 -- function Strict_Equal (Left, Right : Set) return Boolean;
49 -- function Left (Container : Set; Position : Cursor) return Set;
50 -- function Right (Container : Set; Position : Cursor) return Set;
52 -- See detailed specifications for these subprograms
54 private with Ada
.Containers
.Hash_Tables
;
55 private with Ada
.Streams
;
58 type Element_Type
is private;
60 with function Hash
(Element
: Element_Type
) return Hash_Type
;
62 with function Equivalent_Elements
(Left
, Right
: Element_Type
)
65 with function "=" (Left
, Right
: Element_Type
) return Boolean is <>;
67 package Ada
.Containers
.Formal_Hashed_Sets
is
70 type Set
(Capacity
: Count_Type
; Modulus
: Hash_Type
) is tagged private;
71 -- why is this commented out ???
72 -- pragma Preelaborable_Initialization (Set);
74 type Cursor
is private;
75 pragma Preelaborable_Initialization
(Cursor
);
77 Empty_Set
: constant Set
;
79 No_Element
: constant Cursor
;
81 function "=" (Left
, Right
: Set
) return Boolean;
83 function Equivalent_Sets
(Left
, Right
: Set
) return Boolean;
85 function To_Set
(New_Item
: Element_Type
) return Set
;
87 function Capacity
(Container
: Set
) return Count_Type
;
89 procedure Reserve_Capacity
90 (Container
: in out Set
;
91 Capacity
: Count_Type
);
93 function Length
(Container
: Set
) return Count_Type
;
95 function Is_Empty
(Container
: Set
) return Boolean;
97 procedure Clear
(Container
: in out Set
);
99 procedure Assign
(Target
: in out Set
; Source
: Set
);
101 function Copy
(Source
: Set
;
102 Capacity
: Count_Type
:= 0) return Set
;
104 function Element
(Container
: Set
; Position
: Cursor
) return Element_Type
;
106 procedure Replace_Element
107 (Container
: in out Set
;
109 New_Item
: Element_Type
);
111 procedure Query_Element
112 (Container
: in out Set
;
114 Process
: not null access procedure (Element
: Element_Type
));
116 procedure Move
(Target
: in out Set
; Source
: in out Set
);
119 (Container
: in out Set
;
120 New_Item
: Element_Type
;
121 Position
: out Cursor
;
122 Inserted
: out Boolean);
124 procedure Insert
(Container
: in out Set
; New_Item
: Element_Type
);
126 procedure Include
(Container
: in out Set
; New_Item
: Element_Type
);
128 procedure Replace
(Container
: in out Set
; New_Item
: Element_Type
);
130 procedure Exclude
(Container
: in out Set
; Item
: Element_Type
);
132 procedure Delete
(Container
: in out Set
; Item
: Element_Type
);
134 procedure Delete
(Container
: in out Set
; Position
: in out Cursor
);
136 procedure Union
(Target
: in out Set
; Source
: Set
);
138 function Union
(Left
, Right
: Set
) return Set
;
140 function "or" (Left
, Right
: Set
) return Set
renames Union
;
142 procedure Intersection
(Target
: in out Set
; Source
: Set
);
144 function Intersection
(Left
, Right
: Set
) return Set
;
146 function "and" (Left
, Right
: Set
) return Set
renames Intersection
;
148 procedure Difference
(Target
: in out Set
; Source
: Set
);
150 function Difference
(Left
, Right
: Set
) return Set
;
152 function "-" (Left
, Right
: Set
) return Set
renames Difference
;
154 procedure Symmetric_Difference
(Target
: in out Set
; Source
: Set
);
156 function Symmetric_Difference
(Left
, Right
: Set
) return Set
;
158 function "xor" (Left
, Right
: Set
) return Set
159 renames Symmetric_Difference
;
161 function Overlap
(Left
, Right
: Set
) return Boolean;
163 function Is_Subset
(Subset
: Set
; Of_Set
: Set
) return Boolean;
165 function First
(Container
: Set
) return Cursor
;
167 function Next
(Container
: Set
; Position
: Cursor
) return Cursor
;
169 procedure Next
(Container
: Set
; Position
: in out Cursor
);
173 Item
: Element_Type
) return Cursor
;
175 function Contains
(Container
: Set
; Item
: Element_Type
) return Boolean;
177 function Has_Element
(Container
: Set
; Position
: Cursor
) return Boolean;
179 function Equivalent_Elements
(Left
: Set
; CLeft
: Cursor
;
180 Right
: Set
; CRight
: Cursor
) return Boolean;
182 function Equivalent_Elements
183 (Left
: Set
; CLeft
: Cursor
;
184 Right
: Element_Type
) return Boolean;
186 function Equivalent_Elements
187 (Left
: Element_Type
;
188 Right
: Set
; CRight
: Cursor
) return Boolean;
193 not null access procedure (Container
: Set
; Position
: Cursor
));
195 function Default_Modulus
(Capacity
: Count_Type
) return Hash_Type
;
198 type Key_Type
(<>) is private;
200 with function Key
(Element
: Element_Type
) return Key_Type
;
202 with function Hash
(Key
: Key_Type
) return Hash_Type
;
204 with function Equivalent_Keys
(Left
, Right
: Key_Type
) return Boolean;
206 package Generic_Keys
is
208 function Key
(Container
: Set
; Position
: Cursor
) return Key_Type
;
210 function Element
(Container
: Set
; Key
: Key_Type
) return Element_Type
;
213 (Container
: in out Set
;
215 New_Item
: Element_Type
);
217 procedure Exclude
(Container
: in out Set
; Key
: Key_Type
);
219 procedure Delete
(Container
: in out Set
; Key
: Key_Type
);
221 function Find
(Container
: Set
; Key
: Key_Type
) return Cursor
;
223 function Contains
(Container
: Set
; Key
: Key_Type
) return Boolean;
225 procedure Update_Element_Preserving_Key
226 (Container
: in out Set
;
228 Process
: not null access
229 procedure (Element
: in out Element_Type
));
233 function Strict_Equal
(Left
, Right
: Set
) return Boolean;
234 -- Strict_Equal returns True if the containers are physically equal, i.e.
235 -- they are structurally equal (function "=" returns True) and that they
236 -- have the same set of cursors.
238 function Left
(Container
: Set
; Position
: Cursor
) return Set
;
239 function Right
(Container
: Set
; Position
: Cursor
) return Set
;
240 -- Left returns a container containing all elements preceding Position
241 -- (excluded) in Container. Right returns a container containing all
242 -- elements following Position (included) in Container. These two new
243 -- functions can be used to express invariant properties in loops which
244 -- iterate over containers. Left returns the part of the container already
245 -- scanned and Right the part not scanned yet.
249 pragma Inline
(Next
);
253 Element
: Element_Type
;
255 Has_Element
: Boolean := False;
258 package HT_Types
is new
259 Ada
.Containers
.Hash_Tables
.Generic_Bounded_Hash_Table_Types
(Node_Type
);
261 type Set
(Capacity
: Count_Type
; Modulus
: Hash_Type
) is
262 new HT_Types
.Hash_Table_Type
(Capacity
, Modulus
) with null record;
267 type Cursor
is record
272 (Stream
: not null access Root_Stream_Type
'Class;
275 for Cursor
'Write use Write
;
278 (Stream
: not null access Root_Stream_Type
'Class;
281 for Cursor
'Read use Read
;
283 No_Element
: constant Cursor
:= (Node
=> 0);
286 (Stream
: not null access Root_Stream_Type
'Class;
289 for Set
'Write use Write
;
292 (Stream
: not null access Root_Stream_Type
'Class;
293 Container
: out Set
);
295 for Set
'Read use Read
;
297 Empty_Set
: constant Set
:= (Capacity
=> 0, Modulus
=> 0, others => <>);
299 end Ada
.Containers
.Formal_Hashed_Sets
;