File : a-cfhase.ads
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT LIBRARY COMPONENTS --
4 -- --
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 --
6 -- --
7 -- S p e c --
8 -- --
9 -- Copyright (C) 2004-2015, Free Software Foundation, Inc. --
10 -- --
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. --
14 -- --
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. --
21 -- --
22 -- --
23 -- --
24 -- --
25 -- --
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 ------------------------------------------------------------------------------
31
32 -- This spec is derived from package Ada.Containers.Bounded_Hashed_Sets in the
33 -- Ada 2012 RM. The modifications are meant to facilitate formal proofs by
34 -- making it easier to express properties, and by making the specification of
35 -- this unit compatible with SPARK 2014. Note that the API of this unit may be
36 -- subject to incompatible changes as SPARK 2014 evolves.
37
38 -- The modifications are:
39
40 -- A parameter for the container is added to every function reading the
41 -- content of a container: Element, Next, Query_Element, Has_Element, Key,
42 -- Iterate, Equivalent_Elements. This change is motivated by the need to
43 -- have cursors which are valid on different containers (typically a
44 -- container C and its previous version C'Old) for expressing properties,
45 -- which is not possible if cursors encapsulate an access to the underlying
46 -- container.
47
48 -- There are three new functions:
49
50 -- function Strict_Equal (Left, Right : Set) return Boolean;
51 -- function First_To_Previous (Container : Set; Current : Cursor)
52 -- return Set;
53 -- function Current_To_Last (Container : Set; Current : Cursor)
54 -- return Set;
55
56 -- See detailed specifications for these subprograms
57
58 private with Ada.Containers.Hash_Tables;
59
60 generic
61 type Element_Type is private;
62
63 with function Hash (Element : Element_Type) return Hash_Type;
64
65 with function Equivalent_Elements (Left, Right : Element_Type)
66 return Boolean;
67
68 with function "=" (Left, Right : Element_Type) return Boolean is <>;
69
70 package Ada.Containers.Formal_Hashed_Sets with
71 Pure,
72 SPARK_Mode
73 is
74 pragma Annotate (GNATprove, External_Axiomatization);
75 pragma Annotate (CodePeer, Skip_Analysis);
76
77 type Set (Capacity : Count_Type; Modulus : Hash_Type) is private with
78 Iterable => (First => First,
79 Next => Next,
80 Has_Element => Has_Element,
81 Element => Element),
82 Default_Initial_Condition => Is_Empty (Set);
83 pragma Preelaborable_Initialization (Set);
84
85 type Cursor is private;
86 pragma Preelaborable_Initialization (Cursor);
87
88 Empty_Set : constant Set;
89
90 No_Element : constant Cursor;
91
92 function "=" (Left, Right : Set) return Boolean with
93 Global => null;
94
95 function Equivalent_Sets (Left, Right : Set) return Boolean with
96 Global => null;
97
98 function To_Set (New_Item : Element_Type) return Set with
99 Global => null;
100
101 function Capacity (Container : Set) return Count_Type with
102 Global => null;
103
104 procedure Reserve_Capacity
105 (Container : in out Set;
106 Capacity : Count_Type)
107 with
108 Global => null,
109 Pre => Capacity <= Container.Capacity;
110
111 function Length (Container : Set) return Count_Type with
112 Global => null;
113
114 function Is_Empty (Container : Set) return Boolean with
115 Global => null;
116
117 procedure Clear (Container : in out Set) with
118 Global => null;
119
120 procedure Assign (Target : in out Set; Source : Set) with
121 Global => null,
122 Pre => Target.Capacity >= Length (Source);
123
124 function Copy
125 (Source : Set;
126 Capacity : Count_Type := 0) return Set
127 with
128 Global => null,
129 Pre => Capacity = 0 or else Capacity >= Source.Capacity;
130
131 function Element
132 (Container : Set;
133 Position : Cursor) return Element_Type
134 with
135 Global => null,
136 Pre => Has_Element (Container, Position);
137
138 procedure Replace_Element
139 (Container : in out Set;
140 Position : Cursor;
141 New_Item : Element_Type)
142 with
143 Global => null,
144 Pre => Has_Element (Container, Position);
145
146 procedure Move (Target : in out Set; Source : in out Set) with
147 Global => null,
148 Pre => Target.Capacity >= Length (Source);
149
150 procedure Insert
151 (Container : in out Set;
152 New_Item : Element_Type;
153 Position : out Cursor;
154 Inserted : out Boolean)
155 with
156 Global => null,
157 Pre => Length (Container) < Container.Capacity;
158
159 procedure Insert (Container : in out Set; New_Item : Element_Type) with
160 Global => null,
161 Pre => Length (Container) < Container.Capacity
162 and then (not Contains (Container, New_Item));
163
164 procedure Include (Container : in out Set; New_Item : Element_Type) with
165 Global => null,
166 Pre => Length (Container) < Container.Capacity;
167
168 procedure Replace (Container : in out Set; New_Item : Element_Type) with
169 Global => null,
170 Pre => Contains (Container, New_Item);
171
172 procedure Exclude (Container : in out Set; Item : Element_Type) with
173 Global => null;
174
175 procedure Delete (Container : in out Set; Item : Element_Type) with
176 Global => null,
177 Pre => Contains (Container, Item);
178
179 procedure Delete (Container : in out Set; Position : in out Cursor) with
180 Global => null,
181 Pre => Has_Element (Container, Position);
182
183 procedure Union (Target : in out Set; Source : Set) with
184 Global => null,
185 Pre => Length (Target) + Length (Source) -
186 Length (Intersection (Target, Source)) <= Target.Capacity;
187
188 function Union (Left, Right : Set) return Set with
189 Global => null,
190 Pre => Length (Left) + Length (Right) -
191 Length (Intersection (Left, Right)) <= Count_Type'Last;
192
193 function "or" (Left, Right : Set) return Set renames Union;
194
195 procedure Intersection (Target : in out Set; Source : Set) with
196 Global => null;
197
198 function Intersection (Left, Right : Set) return Set with
199 Global => null;
200
201 function "and" (Left, Right : Set) return Set renames Intersection;
202
203 procedure Difference (Target : in out Set; Source : Set) with
204 Global => null;
205
206 function Difference (Left, Right : Set) return Set with
207 Global => null;
208
209 function "-" (Left, Right : Set) return Set renames Difference;
210
211 procedure Symmetric_Difference (Target : in out Set; Source : Set) with
212 Global => null,
213 Pre => Length (Target) + Length (Source) -
214 2 * Length (Intersection (Target, Source)) <= Target.Capacity;
215
216 function Symmetric_Difference (Left, Right : Set) return Set with
217 Global => null,
218 Pre => Length (Left) + Length (Right) -
219 2 * Length (Intersection (Left, Right)) <= Count_Type'Last;
220
221 function "xor" (Left, Right : Set) return Set
222 renames Symmetric_Difference;
223
224 function Overlap (Left, Right : Set) return Boolean with
225 Global => null;
226
227 function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with
228 Global => null;
229
230 function First (Container : Set) return Cursor with
231 Global => null;
232
233 function Next (Container : Set; Position : Cursor) return Cursor with
234 Global => null,
235 Pre => Has_Element (Container, Position) or else Position = No_Element;
236
237 procedure Next (Container : Set; Position : in out Cursor) with
238 Global => null,
239 Pre => Has_Element (Container, Position) or else Position = No_Element;
240
241 function Find
242 (Container : Set;
243 Item : Element_Type) return Cursor
244 with
245 Global => null;
246
247 function Contains (Container : Set; Item : Element_Type) return Boolean with
248 Global => null;
249
250 function Has_Element (Container : Set; Position : Cursor) return Boolean
251 with
252 Global => null;
253
254 function Equivalent_Elements (Left : Set; CLeft : Cursor;
255 Right : Set; CRight : Cursor) return Boolean
256 with
257 Global => null;
258
259 function Equivalent_Elements
260 (Left : Set; CLeft : Cursor;
261 Right : Element_Type) return Boolean
262 with
263 Global => null;
264
265 function Equivalent_Elements
266 (Left : Element_Type;
267 Right : Set; CRight : Cursor) return Boolean
268 with
269 Global => null;
270
271 function Default_Modulus (Capacity : Count_Type) return Hash_Type with
272 Global => null;
273
274 generic
275 type Key_Type (<>) is private;
276
277 with function Key (Element : Element_Type) return Key_Type;
278
279 with function Hash (Key : Key_Type) return Hash_Type;
280
281 with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
282
283 package Generic_Keys with SPARK_Mode is
284
285 function Key (Container : Set; Position : Cursor) return Key_Type with
286 Global => null;
287
288 function Element (Container : Set; Key : Key_Type) return Element_Type
289 with
290 Global => null;
291
292 procedure Replace
293 (Container : in out Set;
294 Key : Key_Type;
295 New_Item : Element_Type)
296 with
297 Global => null;
298
299 procedure Exclude (Container : in out Set; Key : Key_Type) with
300 Global => null;
301
302 procedure Delete (Container : in out Set; Key : Key_Type) with
303 Global => null;
304
305 function Find (Container : Set; Key : Key_Type) return Cursor with
306 Global => null;
307
308 function Contains (Container : Set; Key : Key_Type) return Boolean with
309 Global => null;
310
311 end Generic_Keys;
312
313 function Strict_Equal (Left, Right : Set) return Boolean with
314 Ghost,
315 Global => null;
316 -- Strict_Equal returns True if the containers are physically equal, i.e.
317 -- they are structurally equal (function "=" returns True) and that they
318 -- have the same set of cursors.
319
320 function First_To_Previous (Container : Set; Current : Cursor) return Set
321 with
322 Ghost,
323 Global => null,
324 Pre => Has_Element (Container, Current) or else Current = No_Element;
325
326 function Current_To_Last (Container : Set; Current : Cursor) return Set
327 with
328 Ghost,
329 Global => null,
330 Pre => Has_Element (Container, Current) or else Current = No_Element;
331 -- First_To_Previous returns a container containing all elements preceding
332 -- Current (excluded) in Container. Current_To_Last returns a container
333 -- containing all elements following Current (included) in Container.
334 -- These two new functions can be used to express invariant properties in
335 -- loops which iterate over containers. First_To_Previous returns the part
336 -- of the container already scanned and Current_To_Last the part not
337 -- scanned yet.
338
339 private
340 pragma SPARK_Mode (Off);
341
342 pragma Inline (Next);
343
344 type Node_Type is
345 record
346 Element : Element_Type;
347 Next : Count_Type;
348 Has_Element : Boolean := False;
349 end record;
350
351 package HT_Types is new
352 Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type);
353
354 type Set (Capacity : Count_Type; Modulus : Hash_Type) is
355 new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
356
357 use HT_Types;
358
359 type Cursor is record
360 Node : Count_Type;
361 end record;
362
363 No_Element : constant Cursor := (Node => 0);
364
365 Empty_Set : constant Set := (Capacity => 0, Modulus => 0, others => <>);
366
367 end Ada.Containers.Formal_Hashed_Sets;