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 _ O R D E R 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_Ordered_Sets in
33 -- the Ada 2012 RM. The modifications are to facilitate formal proofs by
34 -- making it 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: Key, Element, Next, Query_Element, Previous,
40 -- Has_Element, Iterate, Reverse_Iterate. This change is motivated by the
41 -- need to have cursors which are valid on different containers (typically
42 -- a container C and its previous version C'Old) for expressing properties,
43 -- which is not possible if cursors encapsulate an access to the underlying
44 -- container. The operators "<" and ">" that could not be modified that way
47 -- There are three new functions:
49 -- function Strict_Equal (Left, Right : Set) return Boolean;
50 -- function Left (Container : Set; Position : Cursor) return Set;
51 -- function Right (Container : Set; Position : Cursor) return Set;
53 -- See detailed specifications for these subprograms
55 private with Ada
.Containers
.Red_Black_Trees
;
56 private with Ada
.Streams
;
59 type Element_Type
is private;
61 with function "<" (Left
, Right
: Element_Type
) return Boolean is <>;
62 with function "=" (Left
, Right
: Element_Type
) return Boolean is <>;
64 package Ada
.Containers
.Formal_Ordered_Sets
is
67 function Equivalent_Elements
(Left
, Right
: Element_Type
) return Boolean;
69 type Set
(Capacity
: Count_Type
) is tagged private;
70 -- why is this commented out ???
71 -- pragma Preelaborable_Initialization (Set);
73 type Cursor
is private;
74 pragma Preelaborable_Initialization
(Cursor
);
76 Empty_Set
: constant Set
;
78 No_Element
: constant Cursor
;
80 function "=" (Left
, Right
: Set
) return Boolean;
82 function Equivalent_Sets
(Left
, Right
: Set
) return Boolean;
84 function To_Set
(New_Item
: Element_Type
) return Set
;
86 function Length
(Container
: Set
) return Count_Type
;
88 function Is_Empty
(Container
: Set
) return Boolean;
90 procedure Clear
(Container
: in out Set
);
92 procedure Assign
(Target
: in out Set
; Source
: Set
);
94 function Copy
(Source
: Set
; Capacity
: Count_Type
:= 0) return Set
;
96 function Element
(Container
: Set
; Position
: Cursor
) return Element_Type
;
98 procedure Replace_Element
99 (Container
: in out Set
;
101 New_Item
: Element_Type
);
103 procedure Query_Element
104 (Container
: in out Set
;
106 Process
: not null access procedure (Element
: Element_Type
));
108 procedure Move
(Target
: in out Set
; Source
: in out Set
);
111 (Container
: in out Set
;
112 New_Item
: Element_Type
;
113 Position
: out Cursor
;
114 Inserted
: out Boolean);
117 (Container
: in out Set
;
118 New_Item
: Element_Type
);
121 (Container
: in out Set
;
122 New_Item
: Element_Type
);
125 (Container
: in out Set
;
126 New_Item
: Element_Type
);
129 (Container
: in out Set
;
130 Item
: Element_Type
);
133 (Container
: in out Set
;
134 Item
: Element_Type
);
137 (Container
: in out Set
;
138 Position
: in out Cursor
);
140 procedure Delete_First
(Container
: in out Set
);
142 procedure Delete_Last
(Container
: in out Set
);
144 procedure Union
(Target
: in out Set
; Source
: Set
);
146 function Union
(Left
, Right
: Set
) return Set
;
148 function "or" (Left
, Right
: Set
) return Set
renames Union
;
150 procedure Intersection
(Target
: in out Set
; Source
: Set
);
152 function Intersection
(Left
, Right
: Set
) return Set
;
154 function "and" (Left
, Right
: Set
) return Set
renames Intersection
;
156 procedure Difference
(Target
: in out Set
; Source
: Set
);
158 function Difference
(Left
, Right
: Set
) return Set
;
160 function "-" (Left
, Right
: Set
) return Set
renames Difference
;
162 procedure Symmetric_Difference
(Target
: in out Set
; Source
: Set
);
164 function Symmetric_Difference
(Left
, Right
: Set
) return Set
;
166 function "xor" (Left
, Right
: Set
) return Set
renames Symmetric_Difference
;
168 function Overlap
(Left
, Right
: Set
) return Boolean;
170 function Is_Subset
(Subset
: Set
; Of_Set
: Set
) return Boolean;
172 function First
(Container
: Set
) return Cursor
;
174 function First_Element
(Container
: Set
) return Element_Type
;
176 function Last
(Container
: Set
) return Cursor
;
178 function Last_Element
(Container
: Set
) return Element_Type
;
180 function Next
(Container
: Set
; Position
: Cursor
) return Cursor
;
182 procedure Next
(Container
: Set
; Position
: in out Cursor
);
184 function Previous
(Container
: Set
; Position
: Cursor
) return Cursor
;
186 procedure Previous
(Container
: Set
; Position
: in out Cursor
);
188 function Find
(Container
: Set
; Item
: Element_Type
) return Cursor
;
190 function Floor
(Container
: Set
; Item
: Element_Type
) return Cursor
;
192 function Ceiling
(Container
: Set
; Item
: Element_Type
) return Cursor
;
194 function Contains
(Container
: Set
; Item
: Element_Type
) return Boolean;
196 function Has_Element
(Container
: Set
; Position
: Cursor
) return Boolean;
201 not null access procedure (Container
: Set
; Position
: Cursor
));
203 procedure Reverse_Iterate
205 Process
: not null access
206 procedure (Container
: Set
; Position
: Cursor
));
209 type Key_Type
(<>) is private;
211 with function Key
(Element
: Element_Type
) return Key_Type
;
213 with function "<" (Left
, Right
: Key_Type
) return Boolean is <>;
215 package Generic_Keys
is
217 function Equivalent_Keys
(Left
, Right
: Key_Type
) return Boolean;
219 function Key
(Container
: Set
; Position
: Cursor
) return Key_Type
;
221 function Element
(Container
: Set
; Key
: Key_Type
) return Element_Type
;
224 (Container
: in out Set
;
226 New_Item
: Element_Type
);
228 procedure Exclude
(Container
: in out Set
; Key
: Key_Type
);
230 procedure Delete
(Container
: in out Set
; Key
: Key_Type
);
232 function Find
(Container
: Set
; Key
: Key_Type
) return Cursor
;
234 function Floor
(Container
: Set
; Key
: Key_Type
) return Cursor
;
236 function Ceiling
(Container
: Set
; Key
: Key_Type
) return Cursor
;
238 function Contains
(Container
: Set
; Key
: Key_Type
) return Boolean;
240 procedure Update_Element_Preserving_Key
241 (Container
: in out Set
;
243 Process
: not null access
244 procedure (Element
: in out Element_Type
));
248 function Strict_Equal
(Left
, Right
: Set
) return Boolean;
249 -- Strict_Equal returns True if the containers are physically equal, i.e.
250 -- they are structurally equal (function "=" returns True) and that they
251 -- have the same set of cursors.
253 function Left
(Container
: Set
; Position
: Cursor
) return Set
;
254 function Right
(Container
: Set
; Position
: Cursor
) return Set
;
255 -- Left returns a container containing all elements preceding Position
256 -- (excluded) in Container. Right returns a container containing all
257 -- elements following Position (included) in Container. These two new
258 -- functions can be used to express invariant properties in loops which
259 -- iterate over containers. Left returns the part of the container already
260 -- scanned and Right the part not scanned yet.
264 pragma Inline
(Next
);
265 pragma Inline
(Previous
);
267 type Node_Type
is record
268 Has_Element
: Boolean := False;
269 Parent
: Count_Type
:= 0;
270 Left
: Count_Type
:= 0;
271 Right
: Count_Type
:= 0;
272 Color
: Red_Black_Trees
.Color_Type
;
273 Element
: Element_Type
;
276 package Tree_Types
is
277 new Red_Black_Trees
.Generic_Bounded_Tree_Types
(Node_Type
);
279 type Set
(Capacity
: Count_Type
) is
280 new Tree_Types
.Tree_Type
(Capacity
) with null record;
285 type Set_Access
is access all Set
;
286 for Set_Access
'Storage_Size use 0;
288 type Cursor
is record
293 (Stream
: not null access Root_Stream_Type
'Class;
296 for Cursor
'Write use Write
;
299 (Stream
: not null access Root_Stream_Type
'Class;
302 for Cursor
'Read use Read
;
304 No_Element
: constant Cursor
:= (Node
=> 0);
307 (Stream
: not null access Root_Stream_Type
'Class;
310 for Set
'Write use Write
;
313 (Stream
: not null access Root_Stream_Type
'Class;
314 Container
: out Set
);
316 for Set
'Read use Read
;
318 Empty_Set
: constant Set
:= (Capacity
=> 0, others => <>);
320 end Ada
.Containers
.Formal_Ordered_Sets
;