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-2013, 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
;
58 type Element_Type
is private;
60 with function "<" (Left
, Right
: Element_Type
) return Boolean is <>;
61 with function "=" (Left
, Right
: Element_Type
) return Boolean is <>;
63 package Ada
.Containers
.Formal_Ordered_Sets
is
66 function Equivalent_Elements
(Left
, Right
: Element_Type
) return Boolean;
68 type Set
(Capacity
: Count_Type
) is private;
69 pragma Preelaborable_Initialization
(Set
);
71 type Cursor
is private;
72 pragma Preelaborable_Initialization
(Cursor
);
74 Empty_Set
: constant Set
;
76 No_Element
: constant Cursor
;
78 function "=" (Left
, Right
: Set
) return Boolean;
80 function Equivalent_Sets
(Left
, Right
: Set
) return Boolean;
82 function To_Set
(New_Item
: Element_Type
) return Set
;
84 function Length
(Container
: Set
) return Count_Type
;
86 function Is_Empty
(Container
: Set
) return Boolean;
88 procedure Clear
(Container
: in out Set
);
90 procedure Assign
(Target
: in out Set
; Source
: Set
) with
91 Pre
=> Target
.Capacity
>= Length
(Source
);
93 function Copy
(Source
: Set
; Capacity
: Count_Type
:= 0) return Set
with
94 Pre
=> Capacity
>= Source
.Capacity
;
98 Position
: Cursor
) return Element_Type
100 Pre
=> Has_Element
(Container
, Position
);
102 procedure Replace_Element
103 (Container
: in out Set
;
105 New_Item
: Element_Type
)
107 Pre
=> Has_Element
(Container
, Position
);
109 procedure Move
(Target
: in out Set
; Source
: in out Set
) with
110 Pre
=> Target
.Capacity
>= Length
(Source
);
113 (Container
: in out Set
;
114 New_Item
: Element_Type
;
115 Position
: out Cursor
;
116 Inserted
: out Boolean)
118 Pre
=> Length
(Container
) < Container
.Capacity
;
121 (Container
: in out Set
;
122 New_Item
: Element_Type
)
124 Pre
=> Length
(Container
) < Container
.Capacity
125 and then (not Contains
(Container
, New_Item
));
128 (Container
: in out Set
;
129 New_Item
: Element_Type
)
131 Pre
=> Length
(Container
) < Container
.Capacity
;
134 (Container
: in out Set
;
135 New_Item
: Element_Type
)
137 Pre
=> Contains
(Container
, New_Item
);
140 (Container
: in out Set
;
141 Item
: Element_Type
);
144 (Container
: in out Set
;
147 Pre
=> Contains
(Container
, Item
);
150 (Container
: in out Set
;
151 Position
: in out Cursor
)
153 Pre
=> Has_Element
(Container
, Position
);
155 procedure Delete_First
(Container
: in out Set
);
157 procedure Delete_Last
(Container
: in out Set
);
159 procedure Union
(Target
: in out Set
; Source
: Set
) with
160 Pre
=> Length
(Target
) + Length
(Source
) -
161 Length
(Intersection
(Target
, Source
)) <= Target
.Capacity
;
163 function Union
(Left
, Right
: Set
) return Set
;
165 function "or" (Left
, Right
: Set
) return Set
renames Union
;
167 procedure Intersection
(Target
: in out Set
; Source
: Set
);
169 function Intersection
(Left
, Right
: Set
) return Set
;
171 function "and" (Left
, Right
: Set
) return Set
renames Intersection
;
173 procedure Difference
(Target
: in out Set
; Source
: Set
);
175 function Difference
(Left
, Right
: Set
) return Set
;
177 function "-" (Left
, Right
: Set
) return Set
renames Difference
;
179 procedure Symmetric_Difference
(Target
: in out Set
; Source
: Set
);
181 function Symmetric_Difference
(Left
, Right
: Set
) return Set
;
183 function "xor" (Left
, Right
: Set
) return Set
renames Symmetric_Difference
;
185 function Overlap
(Left
, Right
: Set
) return Boolean;
187 function Is_Subset
(Subset
: Set
; Of_Set
: Set
) return Boolean;
189 function First
(Container
: Set
) return Cursor
;
191 function First_Element
(Container
: Set
) return Element_Type
with
192 Pre
=> not Is_Empty
(Container
);
194 function Last
(Container
: Set
) return Cursor
;
196 function Last_Element
(Container
: Set
) return Element_Type
with
197 Pre
=> not Is_Empty
(Container
);
199 function Next
(Container
: Set
; Position
: Cursor
) return Cursor
with
200 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
202 procedure Next
(Container
: Set
; Position
: in out Cursor
) with
203 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
205 function Previous
(Container
: Set
; Position
: Cursor
) return Cursor
with
206 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
208 procedure Previous
(Container
: Set
; Position
: in out Cursor
) with
209 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
211 function Find
(Container
: Set
; Item
: Element_Type
) return Cursor
;
213 function Floor
(Container
: Set
; Item
: Element_Type
) return Cursor
;
215 function Ceiling
(Container
: Set
; Item
: Element_Type
) return Cursor
;
217 function Contains
(Container
: Set
; Item
: Element_Type
) return Boolean;
219 function Has_Element
(Container
: Set
; Position
: Cursor
) return Boolean;
222 type Key_Type
(<>) is private;
224 with function Key
(Element
: Element_Type
) return Key_Type
;
226 with function "<" (Left
, Right
: Key_Type
) return Boolean is <>;
228 package Generic_Keys
is
230 function Equivalent_Keys
(Left
, Right
: Key_Type
) return Boolean;
232 function Key
(Container
: Set
; Position
: Cursor
) return Key_Type
;
234 function Element
(Container
: Set
; Key
: Key_Type
) return Element_Type
;
237 (Container
: in out Set
;
239 New_Item
: Element_Type
);
241 procedure Exclude
(Container
: in out Set
; Key
: Key_Type
);
243 procedure Delete
(Container
: in out Set
; Key
: Key_Type
);
245 function Find
(Container
: Set
; Key
: Key_Type
) return Cursor
;
247 function Floor
(Container
: Set
; Key
: Key_Type
) return Cursor
;
249 function Ceiling
(Container
: Set
; Key
: Key_Type
) return Cursor
;
251 function Contains
(Container
: Set
; Key
: Key_Type
) return Boolean;
255 function Strict_Equal
(Left
, Right
: Set
) return Boolean;
256 -- Strict_Equal returns True if the containers are physically equal, i.e.
257 -- they are structurally equal (function "=" returns True) and that they
258 -- have the same set of cursors.
260 function Left
(Container
: Set
; Position
: Cursor
) return Set
with
261 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
262 function Right
(Container
: Set
; Position
: Cursor
) return Set
with
263 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
264 -- Left returns a container containing all elements preceding Position
265 -- (excluded) in Container. Right returns a container containing all
266 -- elements following Position (included) in Container. These two new
267 -- functions can be used to express invariant properties in loops which
268 -- iterate over containers. Left returns the part of the container already
269 -- scanned and Right the part not scanned yet.
273 pragma Inline
(Next
);
274 pragma Inline
(Previous
);
276 type Node_Type
is record
277 Has_Element
: Boolean := False;
278 Parent
: Count_Type
:= 0;
279 Left
: Count_Type
:= 0;
280 Right
: Count_Type
:= 0;
281 Color
: Red_Black_Trees
.Color_Type
;
282 Element
: Element_Type
;
285 package Tree_Types
is
286 new Red_Black_Trees
.Generic_Bounded_Tree_Types
(Node_Type
);
288 type Set
(Capacity
: Count_Type
) is
289 new Tree_Types
.Tree_Type
(Capacity
) with null record;
293 type Cursor
is record
297 No_Element
: constant Cursor
:= (Node
=> 0);
299 Empty_Set
: constant Set
:= (Capacity
=> 0, others => <>);
301 end Ada
.Containers
.Formal_Ordered_Sets
;