|
111
|
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 -- --
|
|
145
|
9 -- Copyright (C) 2004-2019, Free Software Foundation, Inc. --
|
|
111
|
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 -- 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. --
|
|
|
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 with Ada.Containers.Functional_Maps;
|
|
|
49 with Ada.Containers.Functional_Sets;
|
|
|
50 with Ada.Containers.Functional_Vectors;
|
|
|
51 private with Ada.Containers.Hash_Tables;
|
|
|
52
|
|
|
53 generic
|
|
|
54 type Element_Type is private;
|
|
|
55
|
|
|
56 with function Hash (Element : Element_Type) return Hash_Type;
|
|
|
57
|
|
|
58 with function Equivalent_Elements
|
|
|
59 (Left : Element_Type;
|
|
|
60 Right : Element_Type) return Boolean is "=";
|
|
|
61
|
|
|
62 package Ada.Containers.Formal_Hashed_Sets with
|
|
|
63 SPARK_Mode
|
|
|
64 is
|
|
|
65 pragma Annotate (CodePeer, Skip_Analysis);
|
|
|
66
|
|
|
67 type Set (Capacity : Count_Type; Modulus : Hash_Type) is private with
|
|
|
68 Iterable => (First => First,
|
|
|
69 Next => Next,
|
|
|
70 Has_Element => Has_Element,
|
|
|
71 Element => Element),
|
|
|
72 Default_Initial_Condition => Is_Empty (Set);
|
|
|
73 pragma Preelaborable_Initialization (Set);
|
|
|
74
|
|
|
75 type Cursor is record
|
|
|
76 Node : Count_Type;
|
|
|
77 end record;
|
|
|
78
|
|
|
79 No_Element : constant Cursor := (Node => 0);
|
|
|
80
|
|
|
81 function Length (Container : Set) return Count_Type with
|
|
|
82 Global => null,
|
|
|
83 Post => Length'Result <= Container.Capacity;
|
|
|
84
|
|
|
85 pragma Unevaluated_Use_Of_Old (Allow);
|
|
|
86
|
|
|
87 package Formal_Model with Ghost is
|
|
|
88 subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
|
|
|
89
|
|
|
90 package M is new Ada.Containers.Functional_Sets
|
|
|
91 (Element_Type => Element_Type,
|
|
|
92 Equivalent_Elements => Equivalent_Elements);
|
|
|
93
|
|
|
94 function "="
|
|
|
95 (Left : M.Set;
|
|
|
96 Right : M.Set) return Boolean renames M."=";
|
|
|
97
|
|
|
98 function "<="
|
|
|
99 (Left : M.Set;
|
|
|
100 Right : M.Set) return Boolean renames M."<=";
|
|
|
101
|
|
|
102 package E is new Ada.Containers.Functional_Vectors
|
|
|
103 (Element_Type => Element_Type,
|
|
|
104 Index_Type => Positive_Count_Type);
|
|
|
105
|
|
|
106 function "="
|
|
|
107 (Left : E.Sequence;
|
|
|
108 Right : E.Sequence) return Boolean renames E."=";
|
|
|
109
|
|
|
110 function "<"
|
|
|
111 (Left : E.Sequence;
|
|
|
112 Right : E.Sequence) return Boolean renames E."<";
|
|
|
113
|
|
|
114 function "<="
|
|
|
115 (Left : E.Sequence;
|
|
|
116 Right : E.Sequence) return Boolean renames E."<=";
|
|
|
117
|
|
|
118 function Find
|
|
|
119 (Container : E.Sequence;
|
|
|
120 Item : Element_Type) return Count_Type
|
|
|
121 -- Search for Item in Container
|
|
|
122
|
|
|
123 with
|
|
|
124 Global => null,
|
|
|
125 Post =>
|
|
|
126 (if Find'Result > 0 then
|
|
|
127 Find'Result <= E.Length (Container)
|
|
|
128 and Equivalent_Elements
|
|
|
129 (Item, E.Get (Container, Find'Result)));
|
|
|
130
|
|
|
131 function E_Elements_Included
|
|
|
132 (Left : E.Sequence;
|
|
|
133 Right : E.Sequence) return Boolean
|
|
|
134 -- The elements of Left are contained in Right
|
|
|
135
|
|
|
136 with
|
|
|
137 Global => null,
|
|
|
138 Post =>
|
|
|
139 E_Elements_Included'Result =
|
|
|
140 (for all I in 1 .. E.Length (Left) =>
|
|
|
141 Find (Right, E.Get (Left, I)) > 0
|
|
|
142 and then E.Get (Right, Find (Right, E.Get (Left, I))) =
|
|
|
143 E.Get (Left, I));
|
|
|
144 pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
|
|
|
145
|
|
|
146 function E_Elements_Included
|
|
|
147 (Left : E.Sequence;
|
|
|
148 Model : M.Set;
|
|
|
149 Right : E.Sequence) return Boolean
|
|
|
150 -- The elements of Container contained in Model are in Right
|
|
|
151
|
|
|
152 with
|
|
|
153 Global => null,
|
|
|
154 Post =>
|
|
|
155 E_Elements_Included'Result =
|
|
|
156 (for all I in 1 .. E.Length (Left) =>
|
|
|
157 (if M.Contains (Model, E.Get (Left, I)) then
|
|
|
158 Find (Right, E.Get (Left, I)) > 0
|
|
|
159 and then E.Get (Right, Find (Right, E.Get (Left, I))) =
|
|
|
160 E.Get (Left, I)));
|
|
|
161 pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
|
|
|
162
|
|
|
163 function E_Elements_Included
|
|
|
164 (Container : E.Sequence;
|
|
|
165 Model : M.Set;
|
|
|
166 Left : E.Sequence;
|
|
|
167 Right : E.Sequence) return Boolean
|
|
|
168 -- The elements of Container contained in Model are in Left and others
|
|
|
169 -- are in Right.
|
|
|
170
|
|
|
171 with
|
|
|
172 Global => null,
|
|
|
173 Post =>
|
|
|
174 E_Elements_Included'Result =
|
|
|
175 (for all I in 1 .. E.Length (Container) =>
|
|
|
176 (if M.Contains (Model, E.Get (Container, I)) then
|
|
|
177 Find (Left, E.Get (Container, I)) > 0
|
|
|
178 and then E.Get (Left, Find (Left, E.Get (Container, I))) =
|
|
|
179 E.Get (Container, I)
|
|
|
180 else
|
|
|
181 Find (Right, E.Get (Container, I)) > 0
|
|
|
182 and then E.Get
|
|
|
183 (Right, Find (Right, E.Get (Container, I))) =
|
|
|
184 E.Get (Container, I)));
|
|
|
185 pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
|
|
|
186
|
|
|
187 package P is new Ada.Containers.Functional_Maps
|
|
|
188 (Key_Type => Cursor,
|
|
|
189 Element_Type => Positive_Count_Type,
|
|
|
190 Equivalent_Keys => "=",
|
|
|
191 Enable_Handling_Of_Equivalence => False);
|
|
|
192
|
|
|
193 function "="
|
|
|
194 (Left : P.Map;
|
|
|
195 Right : P.Map) return Boolean renames P."=";
|
|
|
196
|
|
|
197 function "<="
|
|
|
198 (Left : P.Map;
|
|
|
199 Right : P.Map) return Boolean renames P."<=";
|
|
|
200
|
|
|
201 function Mapping_Preserved
|
|
|
202 (E_Left : E.Sequence;
|
|
|
203 E_Right : E.Sequence;
|
|
|
204 P_Left : P.Map;
|
|
|
205 P_Right : P.Map) return Boolean
|
|
|
206 with
|
|
|
207 Ghost,
|
|
|
208 Global => null,
|
|
|
209 Post =>
|
|
|
210 (if Mapping_Preserved'Result then
|
|
|
211
|
|
|
212 -- Right contains all the cursors of Left
|
|
|
213
|
|
|
214 P.Keys_Included (P_Left, P_Right)
|
|
|
215
|
|
|
216 -- Right contains all the elements of Left
|
|
|
217
|
|
|
218 and E_Elements_Included (E_Left, E_Right)
|
|
|
219
|
|
|
220 -- Mappings from cursors to elements induced by E_Left, P_Left
|
|
|
221 -- and E_Right, P_Right are the same.
|
|
|
222
|
|
|
223 and (for all C of P_Left =>
|
|
|
224 E.Get (E_Left, P.Get (P_Left, C)) =
|
|
|
225 E.Get (E_Right, P.Get (P_Right, C))));
|
|
|
226
|
|
|
227 function Mapping_Preserved_Except
|
|
|
228 (E_Left : E.Sequence;
|
|
|
229 E_Right : E.Sequence;
|
|
|
230 P_Left : P.Map;
|
|
|
231 P_Right : P.Map;
|
|
|
232 Position : Cursor) return Boolean
|
|
|
233 with
|
|
|
234 Ghost,
|
|
|
235 Global => null,
|
|
|
236 Post =>
|
|
|
237 (if Mapping_Preserved_Except'Result then
|
|
|
238
|
|
|
239 -- Right contains all the cursors of Left
|
|
|
240
|
|
|
241 P.Keys_Included (P_Left, P_Right)
|
|
|
242
|
|
|
243 -- Mappings from cursors to elements induced by E_Left, P_Left
|
|
|
244 -- and E_Right, P_Right are the same except for Position.
|
|
|
245
|
|
|
246 and (for all C of P_Left =>
|
|
|
247 (if C /= Position then
|
|
|
248 E.Get (E_Left, P.Get (P_Left, C)) =
|
|
|
249 E.Get (E_Right, P.Get (P_Right, C)))));
|
|
|
250
|
|
|
251 function Model (Container : Set) return M.Set with
|
|
|
252 -- The high-level model of a set is a set of elements. Neither cursors
|
|
|
253 -- nor order of elements are represented in this model. Elements are
|
|
|
254 -- modeled up to equivalence.
|
|
|
255
|
|
|
256 Ghost,
|
|
|
257 Global => null,
|
|
|
258 Post => M.Length (Model'Result) = Length (Container);
|
|
|
259
|
|
|
260 function Elements (Container : Set) return E.Sequence with
|
|
|
261 -- The Elements sequence represents the underlying list structure of
|
|
|
262 -- sets that is used for iteration. It stores the actual values of
|
|
|
263 -- elements in the set. It does not model cursors.
|
|
|
264
|
|
|
265 Ghost,
|
|
|
266 Global => null,
|
|
|
267 Post =>
|
|
|
268 E.Length (Elements'Result) = Length (Container)
|
|
|
269
|
|
|
270 -- It only contains keys contained in Model
|
|
|
271
|
|
|
272 and (for all Item of Elements'Result =>
|
|
|
273 M.Contains (Model (Container), Item))
|
|
|
274
|
|
|
275 -- It contains all the elements contained in Model
|
|
|
276
|
|
|
277 and (for all Item of Model (Container) =>
|
|
|
278 (Find (Elements'Result, Item) > 0
|
|
|
279 and then Equivalent_Elements
|
|
|
280 (E.Get (Elements'Result,
|
|
|
281 Find (Elements'Result, Item)),
|
|
|
282 Item)))
|
|
|
283
|
|
|
284 -- It has no duplicate
|
|
|
285
|
|
|
286 and (for all I in 1 .. Length (Container) =>
|
|
|
287 Find (Elements'Result, E.Get (Elements'Result, I)) = I)
|
|
|
288
|
|
|
289 and (for all I in 1 .. Length (Container) =>
|
|
|
290 (for all J in 1 .. Length (Container) =>
|
|
|
291 (if Equivalent_Elements
|
|
|
292 (E.Get (Elements'Result, I),
|
|
|
293 E.Get (Elements'Result, J))
|
|
|
294 then I = J)));
|
|
|
295 pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Elements);
|
|
|
296
|
|
|
297 function Positions (Container : Set) return P.Map with
|
|
|
298 -- The Positions map is used to model cursors. It only contains valid
|
|
|
299 -- cursors and maps them to their position in the container.
|
|
|
300
|
|
|
301 Ghost,
|
|
|
302 Global => null,
|
|
|
303 Post =>
|
|
|
304 not P.Has_Key (Positions'Result, No_Element)
|
|
|
305
|
|
|
306 -- Positions of cursors are smaller than the container's length
|
|
|
307
|
|
|
308 and then
|
|
|
309 (for all I of Positions'Result =>
|
|
|
310 P.Get (Positions'Result, I) in 1 .. Length (Container)
|
|
|
311
|
|
|
312 -- No two cursors have the same position. Note that we do not
|
|
|
313 -- state that there is a cursor in the map for each position, as
|
|
|
314 -- it is rarely needed.
|
|
|
315
|
|
|
316 and then
|
|
|
317 (for all J of Positions'Result =>
|
|
|
318 (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
|
|
|
319 then I = J)));
|
|
|
320
|
|
|
321 procedure Lift_Abstraction_Level (Container : Set) with
|
|
|
322 -- Lift_Abstraction_Level is a ghost procedure that does nothing but
|
|
|
323 -- assume that we can access the same elements by iterating over
|
|
|
324 -- positions or cursors.
|
|
|
325 -- This information is not generally useful except when switching from
|
|
|
326 -- a low-level, cursor-aware view of a container, to a high-level,
|
|
|
327 -- position-based view.
|
|
|
328
|
|
|
329 Ghost,
|
|
|
330 Global => null,
|
|
|
331 Post =>
|
|
|
332 (for all Item of Elements (Container) =>
|
|
|
333 (for some I of Positions (Container) =>
|
|
|
334 E.Get (Elements (Container), P.Get (Positions (Container), I)) =
|
|
|
335 Item));
|
|
|
336
|
|
|
337 function Contains
|
|
|
338 (C : M.Set;
|
|
|
339 K : Element_Type) return Boolean renames M.Contains;
|
|
|
340 -- To improve readability of contracts, we rename the function used to
|
|
|
341 -- search for an element in the model to Contains.
|
|
|
342
|
|
|
343 end Formal_Model;
|
|
|
344 use Formal_Model;
|
|
|
345
|
|
|
346 Empty_Set : constant Set;
|
|
|
347
|
|
|
348 function "=" (Left, Right : Set) return Boolean with
|
|
|
349 Global => null,
|
|
|
350 Post =>
|
|
|
351 "="'Result =
|
|
|
352 (Length (Left) = Length (Right)
|
|
|
353 and E_Elements_Included (Elements (Left), Elements (Right)))
|
|
|
354 and
|
|
|
355 "="'Result =
|
|
|
356 (E_Elements_Included (Elements (Left), Elements (Right))
|
|
|
357 and E_Elements_Included (Elements (Right), Elements (Left)));
|
|
145
|
358 -- For each element in Left, set equality attempts to find the equal
|
|
|
359 -- element in Right; if a search fails, then set equality immediately
|
|
|
360 -- returns False. The search works by calling Hash to find the bucket in
|
|
|
361 -- the Right set that corresponds to the Left element. If the bucket is
|
|
|
362 -- non-empty, the search calls the generic formal element equality operator
|
|
|
363 -- to compare the element (in Left) to the element of each node in the
|
|
|
364 -- bucket (in Right); the search terminates when a matching node in the
|
|
|
365 -- bucket is found, or the nodes in the bucket are exhausted. (Note that
|
|
|
366 -- element equality is called here, not Equivalent_Elements. Set equality
|
|
|
367 -- is the only operation in which element equality is used. Compare set
|
|
|
368 -- equality to Equivalent_Sets, which does call Equivalent_Elements.)
|
|
111
|
369
|
|
|
370 function Equivalent_Sets (Left, Right : Set) return Boolean with
|
|
|
371 Global => null,
|
|
|
372 Post => Equivalent_Sets'Result = (Model (Left) = Model (Right));
|
|
145
|
373 -- Similar to set equality, with the difference that the element in Left is
|
|
|
374 -- compared to the elements in Right using the generic formal
|
|
|
375 -- Equivalent_Elements operation instead of element equality.
|
|
111
|
376
|
|
|
377 function To_Set (New_Item : Element_Type) return Set with
|
|
|
378 Global => null,
|
|
|
379 Post =>
|
|
|
380 M.Is_Singleton (Model (To_Set'Result), New_Item)
|
|
|
381 and Length (To_Set'Result) = 1
|
|
|
382 and E.Get (Elements (To_Set'Result), 1) = New_Item;
|
|
145
|
383 -- Constructs a singleton set comprising New_Element. To_Set calls Hash to
|
|
|
384 -- determine the bucket for New_Item.
|
|
111
|
385
|
|
|
386 function Capacity (Container : Set) return Count_Type with
|
|
|
387 Global => null,
|
|
|
388 Post => Capacity'Result = Container.Capacity;
|
|
145
|
389 -- Returns the current capacity of the set. Capacity is the maximum length
|
|
|
390 -- before which rehashing in guaranteed not to occur.
|
|
111
|
391
|
|
|
392 procedure Reserve_Capacity
|
|
|
393 (Container : in out Set;
|
|
|
394 Capacity : Count_Type)
|
|
|
395 with
|
|
|
396 Global => null,
|
|
|
397 Pre => Capacity <= Container.Capacity,
|
|
|
398 Post =>
|
|
|
399 Model (Container) = Model (Container)'Old
|
|
|
400 and Length (Container)'Old = Length (Container)
|
|
|
401
|
|
|
402 -- Actual elements are preserved
|
|
|
403
|
|
|
404 and E_Elements_Included
|
|
|
405 (Elements (Container), Elements (Container)'Old)
|
|
|
406 and E_Elements_Included
|
|
|
407 (Elements (Container)'Old, Elements (Container));
|
|
145
|
408 -- If the value of the Capacity actual parameter is less or equal to
|
|
|
409 -- Container.Capacity, then the operation has no effect. Otherwise it
|
|
|
410 -- raises Capacity_Error (as no expansion of capacity is possible for a
|
|
|
411 -- bounded form).
|
|
111
|
412
|
|
|
413 function Is_Empty (Container : Set) return Boolean with
|
|
|
414 Global => null,
|
|
|
415 Post => Is_Empty'Result = (Length (Container) = 0);
|
|
145
|
416 -- Equivalent to Length (Container) = 0
|
|
111
|
417
|
|
|
418 procedure Clear (Container : in out Set) with
|
|
|
419 Global => null,
|
|
|
420 Post => Length (Container) = 0 and M.Is_Empty (Model (Container));
|
|
145
|
421 -- Removes all of the items from the set. This will deallocate all memory
|
|
|
422 -- associated with this set.
|
|
111
|
423
|
|
|
424 procedure Assign (Target : in out Set; Source : Set) with
|
|
|
425 Global => null,
|
|
|
426 Pre => Target.Capacity >= Length (Source),
|
|
|
427 Post =>
|
|
|
428 Model (Target) = Model (Source)
|
|
|
429 and Length (Target) = Length (Source)
|
|
|
430
|
|
|
431 -- Actual elements are preserved
|
|
|
432
|
|
|
433 and E_Elements_Included (Elements (Target), Elements (Source))
|
|
|
434 and E_Elements_Included (Elements (Source), Elements (Target));
|
|
145
|
435 -- If Target denotes the same object as Source, then the operation has no
|
|
|
436 -- effect. If the Target capacity is less than the Source length, then
|
|
|
437 -- Assign raises Capacity_Error. Otherwise, Assign clears Target and then
|
|
|
438 -- copies the (active) elements from Source to Target.
|
|
111
|
439
|
|
|
440 function Copy
|
|
|
441 (Source : Set;
|
|
|
442 Capacity : Count_Type := 0) return Set
|
|
|
443 with
|
|
|
444 Global => null,
|
|
|
445 Pre => Capacity = 0 or else Capacity >= Source.Capacity,
|
|
|
446 Post =>
|
|
|
447 Model (Copy'Result) = Model (Source)
|
|
|
448 and Elements (Copy'Result) = Elements (Source)
|
|
|
449 and Positions (Copy'Result) = Positions (Source)
|
|
|
450 and (if Capacity = 0 then
|
|
|
451 Copy'Result.Capacity = Source.Capacity
|
|
|
452 else
|
|
|
453 Copy'Result.Capacity = Capacity);
|
|
145
|
454 -- Constructs a new set object whose elements correspond to Source. If the
|
|
|
455 -- Capacity parameter is 0, then the capacity of the result is the same as
|
|
|
456 -- the length of Source. If the Capacity parameter is equal or greater than
|
|
|
457 -- the length of Source, then the capacity of the result is the specified
|
|
|
458 -- value. Otherwise, Copy raises Capacity_Error. If the Modulus parameter
|
|
|
459 -- is 0, then the modulus of the result is the value returned by a call to
|
|
|
460 -- Default_Modulus with the capacity parameter determined as above;
|
|
|
461 -- otherwise the modulus of the result is the specified value.
|
|
111
|
462
|
|
|
463 function Element
|
|
|
464 (Container : Set;
|
|
|
465 Position : Cursor) return Element_Type
|
|
|
466 with
|
|
|
467 Global => null,
|
|
|
468 Pre => Has_Element (Container, Position),
|
|
|
469 Post =>
|
|
|
470 Element'Result =
|
|
|
471 E.Get (Elements (Container), P.Get (Positions (Container), Position));
|
|
|
472 pragma Annotate (GNATprove, Inline_For_Proof, Element);
|
|
|
473
|
|
|
474 procedure Replace_Element
|
|
|
475 (Container : in out Set;
|
|
|
476 Position : Cursor;
|
|
|
477 New_Item : Element_Type)
|
|
|
478 with
|
|
|
479 Global => null,
|
|
|
480 Pre => Has_Element (Container, Position),
|
|
|
481 Post =>
|
|
|
482 Length (Container) = Length (Container)'Old
|
|
|
483
|
|
|
484 -- Position now maps to New_Item
|
|
|
485
|
|
|
486 and Element (Container, Position) = New_Item
|
|
|
487
|
|
|
488 -- New_Item is contained in Container
|
|
|
489
|
|
|
490 and Contains (Model (Container), New_Item)
|
|
|
491
|
|
|
492 -- Other elements are preserved
|
|
|
493
|
|
|
494 and M.Included_Except
|
|
|
495 (Model (Container)'Old,
|
|
|
496 Model (Container),
|
|
|
497 Element (Container, Position)'Old)
|
|
|
498 and M.Included_Except
|
|
|
499 (Model (Container),
|
|
|
500 Model (Container)'Old,
|
|
|
501 New_Item)
|
|
|
502
|
|
|
503 -- Mapping from cursors to elements is preserved
|
|
|
504
|
|
|
505 and Mapping_Preserved_Except
|
|
|
506 (E_Left => Elements (Container)'Old,
|
|
|
507 E_Right => Elements (Container),
|
|
|
508 P_Left => Positions (Container)'Old,
|
|
|
509 P_Right => Positions (Container),
|
|
|
510 Position => Position)
|
|
|
511 and Positions (Container) = Positions (Container)'Old;
|
|
|
512
|
|
|
513 procedure Move (Target : in out Set; Source : in out Set) with
|
|
|
514 Global => null,
|
|
|
515 Pre => Target.Capacity >= Length (Source),
|
|
|
516 Post =>
|
|
|
517 Length (Source) = 0
|
|
|
518 and Model (Target) = Model (Source)'Old
|
|
|
519 and Length (Target) = Length (Source)'Old
|
|
|
520
|
|
|
521 -- Actual elements are preserved
|
|
|
522
|
|
|
523 and E_Elements_Included (Elements (Target), Elements (Source)'Old)
|
|
|
524 and E_Elements_Included (Elements (Source)'Old, Elements (Target));
|
|
145
|
525 -- Clears Target (if it's not empty), and then moves (not copies) the
|
|
|
526 -- buckets array and nodes from Source to Target.
|
|
111
|
527
|
|
|
528 procedure Insert
|
|
|
529 (Container : in out Set;
|
|
|
530 New_Item : Element_Type;
|
|
|
531 Position : out Cursor;
|
|
|
532 Inserted : out Boolean)
|
|
|
533 with
|
|
|
534 Global => null,
|
|
|
535 Pre =>
|
|
|
536 Length (Container) < Container.Capacity
|
|
|
537 or Contains (Container, New_Item),
|
|
|
538 Post =>
|
|
|
539 Contains (Container, New_Item)
|
|
|
540 and Has_Element (Container, Position)
|
|
|
541 and Equivalent_Elements (Element (Container, Position), New_Item),
|
|
|
542 Contract_Cases =>
|
|
|
543
|
|
|
544 -- If New_Item is already in Container, it is not modified and Inserted
|
|
|
545 -- is set to False.
|
|
|
546
|
|
|
547 (Contains (Container, New_Item) =>
|
|
|
548 not Inserted
|
|
|
549 and Model (Container) = Model (Container)'Old
|
|
|
550 and Elements (Container) = Elements (Container)'Old
|
|
|
551 and Positions (Container) = Positions (Container)'Old,
|
|
|
552
|
|
|
553 -- Otherwise, New_Item is inserted in Container and Inserted is set to
|
|
|
554 -- True.
|
|
|
555
|
|
|
556 others =>
|
|
|
557 Inserted
|
|
|
558 and Length (Container) = Length (Container)'Old + 1
|
|
|
559
|
|
|
560 -- Position now maps to New_Item
|
|
|
561
|
|
|
562 and Element (Container, Position) = New_Item
|
|
|
563
|
|
|
564 -- Other elements are preserved
|
|
|
565
|
|
|
566 and Model (Container)'Old <= Model (Container)
|
|
|
567 and M.Included_Except
|
|
|
568 (Model (Container),
|
|
|
569 Model (Container)'Old,
|
|
|
570 New_Item)
|
|
|
571
|
|
|
572 -- Mapping from cursors to elements is preserved
|
|
|
573
|
|
|
574 and Mapping_Preserved
|
|
|
575 (E_Left => Elements (Container)'Old,
|
|
|
576 E_Right => Elements (Container),
|
|
|
577 P_Left => Positions (Container)'Old,
|
|
|
578 P_Right => Positions (Container))
|
|
|
579 and P.Keys_Included_Except
|
|
|
580 (Positions (Container),
|
|
|
581 Positions (Container)'Old,
|
|
|
582 Position));
|
|
145
|
583 -- Conditionally inserts New_Item into the set. If New_Item is already in
|
|
|
584 -- the set, then Inserted returns False and Position designates the node
|
|
|
585 -- containing the existing element (which is not modified). If New_Item is
|
|
|
586 -- not already in the set, then Inserted returns True and Position
|
|
|
587 -- designates the newly-inserted node containing New_Item. The search for
|
|
|
588 -- an existing element works as follows. Hash is called to determine
|
|
|
589 -- New_Item's bucket; if the bucket is non-empty, then Equivalent_Elements
|
|
|
590 -- is called to compare New_Item to the element of each node in that
|
|
|
591 -- bucket. If the bucket is empty, or there were no equivalent elements in
|
|
|
592 -- the bucket, the search "fails" and the New_Item is inserted in the set
|
|
|
593 -- (and Inserted returns True); otherwise, the search "succeeds" (and
|
|
|
594 -- Inserted returns False).
|
|
111
|
595
|
|
|
596 procedure Insert (Container : in out Set; New_Item : Element_Type) with
|
|
|
597 Global => null,
|
|
|
598 Pre => Length (Container) < Container.Capacity
|
|
|
599 and then (not Contains (Container, New_Item)),
|
|
|
600 Post =>
|
|
|
601 Length (Container) = Length (Container)'Old + 1
|
|
|
602 and Contains (Container, New_Item)
|
|
|
603 and Element (Container, Find (Container, New_Item)) = New_Item
|
|
|
604
|
|
|
605 -- Other elements are preserved
|
|
|
606
|
|
|
607 and Model (Container)'Old <= Model (Container)
|
|
|
608 and M.Included_Except
|
|
|
609 (Model (Container),
|
|
|
610 Model (Container)'Old,
|
|
|
611 New_Item)
|
|
|
612
|
|
|
613 -- Mapping from cursors to elements is preserved
|
|
|
614
|
|
|
615 and Mapping_Preserved
|
|
|
616 (E_Left => Elements (Container)'Old,
|
|
|
617 E_Right => Elements (Container),
|
|
|
618 P_Left => Positions (Container)'Old,
|
|
|
619 P_Right => Positions (Container))
|
|
|
620 and P.Keys_Included_Except
|
|
|
621 (Positions (Container),
|
|
|
622 Positions (Container)'Old,
|
|
|
623 Find (Container, New_Item));
|
|
145
|
624 -- Attempts to insert New_Item into the set, performing the usual insertion
|
|
|
625 -- search (which involves calling both Hash and Equivalent_Elements); if
|
|
|
626 -- the search succeeds (New_Item is equivalent to an element already in the
|
|
|
627 -- set, and so was not inserted), then this operation raises
|
|
|
628 -- Constraint_Error. (This version of Insert is similar to Replace, but
|
|
|
629 -- having the opposite exception behavior. It is intended for use when you
|
|
|
630 -- want to assert that the item is not already in the set.)
|
|
111
|
631
|
|
|
632 procedure Include (Container : in out Set; New_Item : Element_Type) with
|
|
|
633 Global => null,
|
|
|
634 Pre =>
|
|
|
635 Length (Container) < Container.Capacity
|
|
|
636 or Contains (Container, New_Item),
|
|
|
637 Post =>
|
|
|
638 Contains (Container, New_Item)
|
|
|
639 and Element (Container, Find (Container, New_Item)) = New_Item,
|
|
|
640 Contract_Cases =>
|
|
|
641
|
|
|
642 -- If an element equivalent to New_Item is already in Container, it is
|
|
|
643 -- replaced by New_Item.
|
|
|
644
|
|
|
645 (Contains (Container, New_Item) =>
|
|
|
646
|
|
|
647 -- Elements are preserved modulo equivalence
|
|
|
648
|
|
|
649 Model (Container) = Model (Container)'Old
|
|
|
650
|
|
|
651 -- Cursors are preserved
|
|
|
652
|
|
|
653 and Positions (Container) = Positions (Container)'Old
|
|
|
654
|
|
|
655 -- The actual value of other elements is preserved
|
|
|
656
|
|
|
657 and E.Equal_Except
|
|
|
658 (Elements (Container)'Old,
|
|
|
659 Elements (Container),
|
|
|
660 P.Get (Positions (Container), Find (Container, New_Item))),
|
|
|
661
|
|
|
662 -- Otherwise, New_Item is inserted in Container
|
|
|
663
|
|
|
664 others =>
|
|
|
665 Length (Container) = Length (Container)'Old + 1
|
|
|
666
|
|
|
667 -- Other elements are preserved
|
|
|
668
|
|
|
669 and Model (Container)'Old <= Model (Container)
|
|
|
670 and M.Included_Except
|
|
|
671 (Model (Container),
|
|
|
672 Model (Container)'Old,
|
|
|
673 New_Item)
|
|
|
674
|
|
|
675 -- Mapping from cursors to elements is preserved
|
|
|
676
|
|
|
677 and Mapping_Preserved
|
|
|
678 (E_Left => Elements (Container)'Old,
|
|
|
679 E_Right => Elements (Container),
|
|
|
680 P_Left => Positions (Container)'Old,
|
|
|
681 P_Right => Positions (Container))
|
|
|
682 and P.Keys_Included_Except
|
|
|
683 (Positions (Container),
|
|
|
684 Positions (Container)'Old,
|
|
|
685 Find (Container, New_Item)));
|
|
145
|
686 -- Attempts to insert New_Item into the set. If an element equivalent to
|
|
|
687 -- New_Item is already in the set (the insertion search succeeded, and
|
|
|
688 -- hence New_Item was not inserted), then the value of New_Item is assigned
|
|
|
689 -- to the existing element. (This insertion operation only raises an
|
|
|
690 -- exception if cursor tampering occurs. It is intended for use when you
|
|
|
691 -- want to insert the item in the set, and you don't care whether an
|
|
|
692 -- equivalent element is already present.)
|
|
111
|
693
|
|
|
694 procedure Replace (Container : in out Set; New_Item : Element_Type) with
|
|
|
695 Global => null,
|
|
|
696 Pre => Contains (Container, New_Item),
|
|
|
697 Post =>
|
|
|
698
|
|
|
699 -- Elements are preserved modulo equivalence
|
|
|
700
|
|
|
701 Model (Container) = Model (Container)'Old
|
|
|
702 and Contains (Container, New_Item)
|
|
|
703
|
|
|
704 -- Cursors are preserved
|
|
|
705
|
|
|
706 and Positions (Container) = Positions (Container)'Old
|
|
|
707
|
|
|
708 -- The element equivalent to New_Item in Container is replaced by
|
|
|
709 -- New_Item.
|
|
|
710
|
|
|
711 and Element (Container, Find (Container, New_Item)) = New_Item
|
|
|
712 and E.Equal_Except
|
|
|
713 (Elements (Container)'Old,
|
|
|
714 Elements (Container),
|
|
|
715 P.Get (Positions (Container), Find (Container, New_Item)));
|
|
145
|
716 -- Searches for New_Item in the set; if the search fails (because an
|
|
|
717 -- equivalent element was not in the set), then it raises
|
|
|
718 -- Constraint_Error. Otherwise, the existing element is assigned the value
|
|
|
719 -- New_Item. (This is similar to Insert, but with the opposite exception
|
|
|
720 -- behavior. It is intended for use when you want to assert that the item
|
|
|
721 -- is already in the set.)
|
|
111
|
722
|
|
|
723 procedure Exclude (Container : in out Set; Item : Element_Type) with
|
|
|
724 Global => null,
|
|
|
725 Post => not Contains (Container, Item),
|
|
|
726 Contract_Cases =>
|
|
|
727
|
|
|
728 -- If Item is not in Container, nothing is changed
|
|
|
729
|
|
|
730 (not Contains (Container, Item) =>
|
|
|
731 Model (Container) = Model (Container)'Old
|
|
|
732 and Elements (Container) = Elements (Container)'Old
|
|
|
733 and Positions (Container) = Positions (Container)'Old,
|
|
|
734
|
|
|
735 -- Otherwise, Item is removed from Container
|
|
|
736
|
|
|
737 others =>
|
|
|
738 Length (Container) = Length (Container)'Old - 1
|
|
|
739
|
|
|
740 -- Other elements are preserved
|
|
|
741
|
|
|
742 and Model (Container) <= Model (Container)'Old
|
|
|
743 and M.Included_Except
|
|
|
744 (Model (Container)'Old,
|
|
|
745 Model (Container),
|
|
|
746 Item)
|
|
|
747
|
|
|
748 -- Mapping from cursors to elements is preserved
|
|
|
749
|
|
|
750 and Mapping_Preserved
|
|
|
751 (E_Left => Elements (Container),
|
|
|
752 E_Right => Elements (Container)'Old,
|
|
|
753 P_Left => Positions (Container),
|
|
|
754 P_Right => Positions (Container)'Old)
|
|
|
755 and P.Keys_Included_Except
|
|
|
756 (Positions (Container)'Old,
|
|
|
757 Positions (Container),
|
|
|
758 Find (Container, Item)'Old));
|
|
145
|
759 -- Searches for Item in the set, and if found, removes its node from the
|
|
|
760 -- set and then deallocates it. The search works as follows. The operation
|
|
|
761 -- calls Hash to determine the item's bucket; if the bucket is not empty,
|
|
|
762 -- it calls Equivalent_Elements to compare Item to the element of each node
|
|
|
763 -- in the bucket. (This is the deletion analog of Include. It is intended
|
|
|
764 -- for use when you want to remove the item from the set, but don't care
|
|
|
765 -- whether the item is already in the set.)
|
|
111
|
766
|
|
|
767 procedure Delete (Container : in out Set; Item : Element_Type) with
|
|
|
768 Global => null,
|
|
|
769 Pre => Contains (Container, Item),
|
|
|
770 Post =>
|
|
|
771 Length (Container) = Length (Container)'Old - 1
|
|
|
772
|
|
|
773 -- Item is no longer in Container
|
|
|
774
|
|
|
775 and not Contains (Container, Item)
|
|
|
776
|
|
|
777 -- Other elements are preserved
|
|
|
778
|
|
|
779 and Model (Container) <= Model (Container)'Old
|
|
|
780 and M.Included_Except
|
|
|
781 (Model (Container)'Old,
|
|
|
782 Model (Container),
|
|
|
783 Item)
|
|
|
784
|
|
|
785 -- Mapping from cursors to elements is preserved
|
|
|
786
|
|
|
787 and Mapping_Preserved
|
|
|
788 (E_Left => Elements (Container),
|
|
|
789 E_Right => Elements (Container)'Old,
|
|
|
790 P_Left => Positions (Container),
|
|
|
791 P_Right => Positions (Container)'Old)
|
|
|
792 and P.Keys_Included_Except
|
|
|
793 (Positions (Container)'Old,
|
|
|
794 Positions (Container),
|
|
|
795 Find (Container, Item)'Old);
|
|
145
|
796 -- Searches for Item in the set (which involves calling both Hash and
|
|
|
797 -- Equivalent_Elements). If the search fails, then the operation raises
|
|
|
798 -- Constraint_Error. Otherwise it removes the node from the set and then
|
|
|
799 -- deallocates it. (This is the deletion analog of non-conditional
|
|
|
800 -- Insert. It is intended for use when you want to assert that the item is
|
|
|
801 -- already in the set.)
|
|
111
|
802
|
|
|
803 procedure Delete (Container : in out Set; Position : in out Cursor) with
|
|
|
804 Global => null,
|
|
|
805 Pre => Has_Element (Container, Position),
|
|
|
806 Post =>
|
|
|
807 Position = No_Element
|
|
|
808 and Length (Container) = Length (Container)'Old - 1
|
|
|
809
|
|
|
810 -- The element at position Position is no longer in Container
|
|
|
811
|
|
|
812 and not Contains (Container, Element (Container, Position)'Old)
|
|
|
813 and not P.Has_Key (Positions (Container), Position'Old)
|
|
|
814
|
|
|
815 -- Other elements are preserved
|
|
|
816
|
|
|
817 and Model (Container) <= Model (Container)'Old
|
|
|
818 and M.Included_Except
|
|
|
819 (Model (Container)'Old,
|
|
|
820 Model (Container),
|
|
|
821 Element (Container, Position)'Old)
|
|
|
822
|
|
|
823 -- Mapping from cursors to elements is preserved
|
|
|
824
|
|
|
825 and Mapping_Preserved
|
|
|
826 (E_Left => Elements (Container),
|
|
|
827 E_Right => Elements (Container)'Old,
|
|
|
828 P_Left => Positions (Container),
|
|
|
829 P_Right => Positions (Container)'Old)
|
|
|
830 and P.Keys_Included_Except
|
|
|
831 (Positions (Container)'Old,
|
|
|
832 Positions (Container),
|
|
|
833 Position'Old);
|
|
145
|
834 -- Removes the node designated by Position from the set, and then
|
|
|
835 -- deallocates the node. The operation calls Hash to determine the bucket,
|
|
|
836 -- and then compares Position to each node in the bucket until there's a
|
|
|
837 -- match (it does not call Equivalent_Elements).
|
|
111
|
838
|
|
|
839 procedure Union (Target : in out Set; Source : Set) with
|
|
|
840 Global => null,
|
|
|
841 Pre =>
|
|
|
842 Length (Source) - Length (Target and Source) <=
|
|
|
843 Target.Capacity - Length (Target),
|
|
|
844 Post =>
|
|
|
845 Length (Target) = Length (Target)'Old
|
|
|
846 - M.Num_Overlaps (Model (Target)'Old, Model (Source))
|
|
|
847 + Length (Source)
|
|
|
848
|
|
|
849 -- Elements already in Target are still in Target
|
|
|
850
|
|
|
851 and Model (Target)'Old <= Model (Target)
|
|
|
852
|
|
|
853 -- Elements of Source are included in Target
|
|
|
854
|
|
|
855 and Model (Source) <= Model (Target)
|
|
|
856
|
|
|
857 -- Elements of Target come from either Source or Target
|
|
|
858
|
|
|
859 and M.Included_In_Union
|
|
|
860 (Model (Target), Model (Source), Model (Target)'Old)
|
|
|
861
|
|
|
862 -- Actual value of elements come from either Left or Right
|
|
|
863
|
|
|
864 and E_Elements_Included
|
|
|
865 (Elements (Target),
|
|
|
866 Model (Target)'Old,
|
|
|
867 Elements (Target)'Old,
|
|
|
868 Elements (Source))
|
|
|
869
|
|
|
870 and E_Elements_Included
|
|
|
871 (Elements (Target)'Old, Model (Target)'Old, Elements (Target))
|
|
|
872
|
|
|
873 and E_Elements_Included
|
|
|
874 (Elements (Source),
|
|
|
875 Model (Target)'Old,
|
|
|
876 Elements (Source),
|
|
|
877 Elements (Target))
|
|
|
878
|
|
|
879 -- Mapping from cursors of Target to elements is preserved
|
|
|
880
|
|
|
881 and Mapping_Preserved
|
|
|
882 (E_Left => Elements (Target)'Old,
|
|
|
883 E_Right => Elements (Target),
|
|
|
884 P_Left => Positions (Target)'Old,
|
|
|
885 P_Right => Positions (Target));
|
|
145
|
886 -- Iterates over the Source set, and conditionally inserts each element
|
|
|
887 -- into Target.
|
|
111
|
888
|
|
|
889 function Union (Left, Right : Set) return Set with
|
|
|
890 Global => null,
|
|
|
891 Pre => Length (Left) <= Count_Type'Last - Length (Right),
|
|
|
892 Post =>
|
|
|
893 Length (Union'Result) = Length (Left)
|
|
|
894 - M.Num_Overlaps (Model (Left), Model (Right))
|
|
|
895 + Length (Right)
|
|
|
896
|
|
|
897 -- Elements of Left and Right are in the result of Union
|
|
|
898
|
|
|
899 and Model (Left) <= Model (Union'Result)
|
|
|
900 and Model (Right) <= Model (Union'Result)
|
|
|
901
|
|
|
902 -- Elements of the result of union come from either Left or Right
|
|
|
903
|
|
|
904 and
|
|
|
905 M.Included_In_Union
|
|
|
906 (Model (Union'Result), Model (Left), Model (Right))
|
|
|
907
|
|
|
908 -- Actual value of elements come from either Left or Right
|
|
|
909
|
|
|
910 and E_Elements_Included
|
|
|
911 (Elements (Union'Result),
|
|
|
912 Model (Left),
|
|
|
913 Elements (Left),
|
|
|
914 Elements (Right))
|
|
|
915
|
|
|
916 and E_Elements_Included
|
|
|
917 (Elements (Left), Model (Left), Elements (Union'Result))
|
|
|
918
|
|
|
919 and E_Elements_Included
|
|
|
920 (Elements (Right),
|
|
|
921 Model (Left),
|
|
|
922 Elements (Right),
|
|
|
923 Elements (Union'Result));
|
|
145
|
924 -- The operation first copies the Left set to the result, and then iterates
|
|
|
925 -- over the Right set to conditionally insert each element into the result.
|
|
111
|
926
|
|
|
927 function "or" (Left, Right : Set) return Set renames Union;
|
|
|
928
|
|
|
929 procedure Intersection (Target : in out Set; Source : Set) with
|
|
|
930 Global => null,
|
|
|
931 Post =>
|
|
|
932 Length (Target) =
|
|
|
933 M.Num_Overlaps (Model (Target)'Old, Model (Source))
|
|
|
934
|
|
|
935 -- Elements of Target were already in Target
|
|
|
936
|
|
|
937 and Model (Target) <= Model (Target)'Old
|
|
|
938
|
|
|
939 -- Elements of Target are in Source
|
|
|
940
|
|
|
941 and Model (Target) <= Model (Source)
|
|
|
942
|
|
|
943 -- Elements both in Source and Target are in the intersection
|
|
|
944
|
|
|
945 and M.Includes_Intersection
|
|
|
946 (Model (Target), Model (Source), Model (Target)'Old)
|
|
|
947
|
|
|
948 -- Actual value of elements of Target is preserved
|
|
|
949
|
|
|
950 and E_Elements_Included (Elements (Target), Elements (Target)'Old)
|
|
|
951 and E_Elements_Included
|
|
|
952 (Elements (Target)'Old, Model (Source), Elements (Target))
|
|
|
953
|
|
|
954 -- Mapping from cursors of Target to elements is preserved
|
|
|
955
|
|
|
956 and Mapping_Preserved
|
|
|
957 (E_Left => Elements (Target),
|
|
|
958 E_Right => Elements (Target)'Old,
|
|
|
959 P_Left => Positions (Target),
|
|
|
960 P_Right => Positions (Target)'Old);
|
|
145
|
961 -- Iterates over the Target set (calling First and Next), calling Find to
|
|
|
962 -- determine whether the element is in Source. If an equivalent element is
|
|
|
963 -- not found in Source, the element is deleted from Target.
|
|
111
|
964
|
|
|
965 function Intersection (Left, Right : Set) return Set with
|
|
|
966 Global => null,
|
|
|
967 Post =>
|
|
|
968 Length (Intersection'Result) =
|
|
|
969 M.Num_Overlaps (Model (Left), Model (Right))
|
|
|
970
|
|
|
971 -- Elements in the result of Intersection are in Left and Right
|
|
|
972
|
|
|
973 and Model (Intersection'Result) <= Model (Left)
|
|
|
974 and Model (Intersection'Result) <= Model (Right)
|
|
|
975
|
|
|
976 -- Elements both in Left and Right are in the result of Intersection
|
|
|
977
|
|
|
978 and M.Includes_Intersection
|
|
|
979 (Model (Intersection'Result), Model (Left), Model (Right))
|
|
|
980
|
|
|
981 -- Actual value of elements come from Left
|
|
|
982
|
|
|
983 and E_Elements_Included
|
|
|
984 (Elements (Intersection'Result), Elements (Left))
|
|
|
985
|
|
|
986 and E_Elements_Included
|
|
|
987 (Elements (Left), Model (Right),
|
|
|
988 Elements (Intersection'Result));
|
|
145
|
989 -- Iterates over the Left set, calling Find to determine whether the
|
|
|
990 -- element is in Right. If an equivalent element is found, it is inserted
|
|
|
991 -- into the result set.
|
|
111
|
992
|
|
|
993 function "and" (Left, Right : Set) return Set renames Intersection;
|
|
|
994
|
|
|
995 procedure Difference (Target : in out Set; Source : Set) with
|
|
|
996 Global => null,
|
|
|
997 Post =>
|
|
|
998 Length (Target) = Length (Target)'Old -
|
|
|
999 M.Num_Overlaps (Model (Target)'Old, Model (Source))
|
|
|
1000
|
|
|
1001 -- Elements of Target were already in Target
|
|
|
1002
|
|
|
1003 and Model (Target) <= Model (Target)'Old
|
|
|
1004
|
|
|
1005 -- Elements of Target are not in Source
|
|
|
1006
|
|
|
1007 and M.No_Overlap (Model (Target), Model (Source))
|
|
|
1008
|
|
|
1009 -- Elements in Target but not in Source are in the difference
|
|
|
1010
|
|
|
1011 and M.Included_In_Union
|
|
|
1012 (Model (Target)'Old, Model (Target), Model (Source))
|
|
|
1013
|
|
|
1014 -- Actual value of elements of Target is preserved
|
|
|
1015
|
|
|
1016 and E_Elements_Included (Elements (Target), Elements (Target)'Old)
|
|
|
1017 and E_Elements_Included
|
|
|
1018 (Elements (Target)'Old, Model (Target), Elements (Target))
|
|
|
1019
|
|
|
1020 -- Mapping from cursors of Target to elements is preserved
|
|
|
1021
|
|
|
1022 and Mapping_Preserved
|
|
|
1023 (E_Left => Elements (Target),
|
|
|
1024 E_Right => Elements (Target)'Old,
|
|
|
1025 P_Left => Positions (Target),
|
|
|
1026 P_Right => Positions (Target)'Old);
|
|
145
|
1027 -- Iterates over the Source (calling First and Next), calling Find to
|
|
|
1028 -- determine whether the element is in Target. If an equivalent element is
|
|
|
1029 -- found, it is deleted from Target.
|
|
111
|
1030
|
|
|
1031 function Difference (Left, Right : Set) return Set with
|
|
|
1032 Global => null,
|
|
|
1033 Post =>
|
|
|
1034 Length (Difference'Result) = Length (Left) -
|
|
|
1035 M.Num_Overlaps (Model (Left), Model (Right))
|
|
|
1036
|
|
|
1037 -- Elements of the result of Difference are in Left
|
|
|
1038
|
|
|
1039 and Model (Difference'Result) <= Model (Left)
|
|
|
1040
|
|
|
1041 -- Elements of the result of Difference are in Right
|
|
|
1042
|
|
|
1043 and M.No_Overlap (Model (Difference'Result), Model (Right))
|
|
|
1044
|
|
|
1045 -- Elements in Left but not in Right are in the difference
|
|
|
1046
|
|
|
1047 and M.Included_In_Union
|
|
|
1048 (Model (Left), Model (Difference'Result), Model (Right))
|
|
|
1049
|
|
|
1050 -- Actual value of elements come from Left
|
|
|
1051
|
|
|
1052 and E_Elements_Included
|
|
|
1053 (Elements (Difference'Result), Elements (Left))
|
|
|
1054
|
|
|
1055 and E_Elements_Included
|
|
|
1056 (Elements (Left),
|
|
|
1057 Model (Difference'Result),
|
|
|
1058 Elements (Difference'Result));
|
|
145
|
1059 -- Iterates over the Left set, calling Find to determine whether the
|
|
|
1060 -- element is in the Right set. If an equivalent element is not found, the
|
|
|
1061 -- element is inserted into the result set.
|
|
111
|
1062
|
|
|
1063 function "-" (Left, Right : Set) return Set renames Difference;
|
|
|
1064
|
|
|
1065 procedure Symmetric_Difference (Target : in out Set; Source : Set) with
|
|
|
1066 Global => null,
|
|
|
1067 Pre =>
|
|
|
1068 Length (Source) - Length (Target and Source) <=
|
|
|
1069 Target.Capacity - Length (Target) + Length (Target and Source),
|
|
|
1070 Post =>
|
|
|
1071 Length (Target) = Length (Target)'Old -
|
|
|
1072 2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) +
|
|
|
1073 Length (Source)
|
|
|
1074
|
|
|
1075 -- Elements of the difference were not both in Source and in Target
|
|
|
1076
|
|
|
1077 and M.Not_In_Both (Model (Target), Model (Target)'Old, Model (Source))
|
|
|
1078
|
|
|
1079 -- Elements in Target but not in Source are in the difference
|
|
|
1080
|
|
|
1081 and M.Included_In_Union
|
|
|
1082 (Model (Target)'Old, Model (Target), Model (Source))
|
|
|
1083
|
|
|
1084 -- Elements in Source but not in Target are in the difference
|
|
|
1085
|
|
|
1086 and M.Included_In_Union
|
|
|
1087 (Model (Source), Model (Target), Model (Target)'Old)
|
|
|
1088
|
|
|
1089 -- Actual value of elements come from either Left or Right
|
|
|
1090
|
|
|
1091 and E_Elements_Included
|
|
|
1092 (Elements (Target),
|
|
|
1093 Model (Target)'Old,
|
|
|
1094 Elements (Target)'Old,
|
|
|
1095 Elements (Source))
|
|
|
1096
|
|
|
1097 and E_Elements_Included
|
|
|
1098 (Elements (Target)'Old, Model (Target), Elements (Target))
|
|
|
1099
|
|
|
1100 and E_Elements_Included
|
|
|
1101 (Elements (Source), Model (Target), Elements (Target));
|
|
145
|
1102 -- The operation iterates over the Source set, searching for the element
|
|
|
1103 -- in Target (calling Hash and Equivalent_Elements). If an equivalent
|
|
|
1104 -- element is found, it is removed from Target; otherwise it is inserted
|
|
|
1105 -- into Target.
|
|
111
|
1106
|
|
|
1107 function Symmetric_Difference (Left, Right : Set) return Set with
|
|
|
1108 Global => null,
|
|
|
1109 Pre => Length (Left) <= Count_Type'Last - Length (Right),
|
|
|
1110 Post =>
|
|
|
1111 Length (Symmetric_Difference'Result) = Length (Left) -
|
|
|
1112 2 * M.Num_Overlaps (Model (Left), Model (Right)) +
|
|
|
1113 Length (Right)
|
|
|
1114
|
|
|
1115 -- Elements of the difference were not both in Left and Right
|
|
|
1116
|
|
|
1117 and M.Not_In_Both
|
|
|
1118 (Model (Symmetric_Difference'Result),
|
|
|
1119 Model (Left),
|
|
|
1120 Model (Right))
|
|
|
1121
|
|
|
1122 -- Elements in Left but not in Right are in the difference
|
|
|
1123
|
|
|
1124 and M.Included_In_Union
|
|
|
1125 (Model (Left),
|
|
|
1126 Model (Symmetric_Difference'Result),
|
|
|
1127 Model (Right))
|
|
|
1128
|
|
|
1129 -- Elements in Right but not in Left are in the difference
|
|
|
1130
|
|
|
1131 and M.Included_In_Union
|
|
|
1132 (Model (Right),
|
|
|
1133 Model (Symmetric_Difference'Result),
|
|
|
1134 Model (Left))
|
|
|
1135
|
|
|
1136 -- Actual value of elements come from either Left or Right
|
|
|
1137
|
|
|
1138 and E_Elements_Included
|
|
|
1139 (Elements (Symmetric_Difference'Result),
|
|
|
1140 Model (Left),
|
|
|
1141 Elements (Left),
|
|
|
1142 Elements (Right))
|
|
|
1143
|
|
|
1144 and E_Elements_Included
|
|
|
1145 (Elements (Left),
|
|
|
1146 Model (Symmetric_Difference'Result),
|
|
|
1147 Elements (Symmetric_Difference'Result))
|
|
|
1148
|
|
|
1149 and E_Elements_Included
|
|
|
1150 (Elements (Right),
|
|
|
1151 Model (Symmetric_Difference'Result),
|
|
|
1152 Elements (Symmetric_Difference'Result));
|
|
145
|
1153 -- The operation first iterates over the Left set. It calls Find to
|
|
|
1154 -- determine whether the element is in the Right set. If no equivalent
|
|
|
1155 -- element is found, the element from Left is inserted into the result. The
|
|
|
1156 -- operation then iterates over the Right set, to determine whether the
|
|
|
1157 -- element is in the Left set. If no equivalent element is found, the Right
|
|
|
1158 -- element is inserted into the result.
|
|
111
|
1159
|
|
|
1160 function "xor" (Left, Right : Set) return Set
|
|
|
1161 renames Symmetric_Difference;
|
|
|
1162
|
|
|
1163 function Overlap (Left, Right : Set) return Boolean with
|
|
|
1164 Global => null,
|
|
|
1165 Post =>
|
|
|
1166 Overlap'Result = not (M.No_Overlap (Model (Left), Model (Right)));
|
|
145
|
1167 -- Iterates over the Left set (calling First and Next), calling Find to
|
|
|
1168 -- determine whether the element is in the Right set. If an equivalent
|
|
|
1169 -- element is found, the operation immediately returns True. The operation
|
|
|
1170 -- returns False if the iteration over Left terminates without finding any
|
|
|
1171 -- equivalent element in Right.
|
|
111
|
1172
|
|
|
1173 function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with
|
|
|
1174 Global => null,
|
|
|
1175 Post => Is_Subset'Result = (Model (Subset) <= Model (Of_Set));
|
|
145
|
1176 -- Iterates over Subset (calling First and Next), calling Find to determine
|
|
|
1177 -- whether the element is in Of_Set. If no equivalent element is found in
|
|
|
1178 -- Of_Set, the operation immediately returns False. The operation returns
|
|
|
1179 -- True if the iteration over Subset terminates without finding an element
|
|
|
1180 -- not in Of_Set (that is, every element in Subset is equivalent to an
|
|
|
1181 -- element in Of_Set).
|
|
111
|
1182
|
|
|
1183 function First (Container : Set) return Cursor with
|
|
|
1184 Global => null,
|
|
|
1185 Contract_Cases =>
|
|
|
1186 (Length (Container) = 0 =>
|
|
|
1187 First'Result = No_Element,
|
|
|
1188
|
|
|
1189 others =>
|
|
|
1190 Has_Element (Container, First'Result)
|
|
|
1191 and P.Get (Positions (Container), First'Result) = 1);
|
|
145
|
1192 -- Returns a cursor that designates the first non-empty bucket, by
|
|
|
1193 -- searching from the beginning of the buckets array.
|
|
111
|
1194
|
|
|
1195 function Next (Container : Set; Position : Cursor) return Cursor with
|
|
|
1196 Global => null,
|
|
|
1197 Pre =>
|
|
|
1198 Has_Element (Container, Position) or else Position = No_Element,
|
|
|
1199 Contract_Cases =>
|
|
|
1200 (Position = No_Element
|
|
|
1201 or else P.Get (Positions (Container), Position) = Length (Container)
|
|
|
1202 =>
|
|
|
1203 Next'Result = No_Element,
|
|
|
1204
|
|
|
1205 others =>
|
|
|
1206 Has_Element (Container, Next'Result)
|
|
|
1207 and then P.Get (Positions (Container), Next'Result) =
|
|
|
1208 P.Get (Positions (Container), Position) + 1);
|
|
145
|
1209 -- Returns a cursor that designates the node that follows the current one
|
|
|
1210 -- designated by Position. If Position designates the last node in its
|
|
|
1211 -- bucket, the operation calls Hash to compute the index of this bucket,
|
|
|
1212 -- and searches the buckets array for the first non-empty bucket, starting
|
|
|
1213 -- from that index; otherwise, it simply follows the link to the next node
|
|
|
1214 -- in the same bucket.
|
|
111
|
1215
|
|
|
1216 procedure Next (Container : Set; Position : in out Cursor) with
|
|
|
1217 Global => null,
|
|
|
1218 Pre =>
|
|
|
1219 Has_Element (Container, Position) or else Position = No_Element,
|
|
|
1220 Contract_Cases =>
|
|
|
1221 (Position = No_Element
|
|
|
1222 or else P.Get (Positions (Container), Position) = Length (Container)
|
|
|
1223 =>
|
|
|
1224 Position = No_Element,
|
|
|
1225
|
|
|
1226 others =>
|
|
|
1227 Has_Element (Container, Position)
|
|
|
1228 and then P.Get (Positions (Container), Position) =
|
|
|
1229 P.Get (Positions (Container), Position'Old) + 1);
|
|
145
|
1230 -- Equivalent to Position := Next (Position)
|
|
111
|
1231
|
|
|
1232 function Find
|
|
|
1233 (Container : Set;
|
|
|
1234 Item : Element_Type) return Cursor
|
|
|
1235 with
|
|
|
1236 Global => null,
|
|
|
1237 Contract_Cases =>
|
|
|
1238
|
|
|
1239 -- If Item is not contained in Container, Find returns No_Element
|
|
|
1240
|
|
|
1241 (not Contains (Model (Container), Item) =>
|
|
|
1242 Find'Result = No_Element,
|
|
|
1243
|
|
|
1244 -- Otherwise, Find returns a valid cursor in Container
|
|
|
1245
|
|
|
1246 others =>
|
|
|
1247 P.Has_Key (Positions (Container), Find'Result)
|
|
|
1248 and P.Get (Positions (Container), Find'Result) =
|
|
|
1249 Find (Elements (Container), Item)
|
|
|
1250
|
|
|
1251 -- The element designated by the result of Find is Item
|
|
|
1252
|
|
|
1253 and Equivalent_Elements
|
|
|
1254 (Element (Container, Find'Result), Item));
|
|
145
|
1255 -- Searches for Item in the set. Find calls Hash to determine the item's
|
|
|
1256 -- bucket; if the bucket is not empty, it calls Equivalent_Elements to
|
|
|
1257 -- compare Item to each element in the bucket. If the search succeeds, Find
|
|
|
1258 -- returns a cursor designating the node containing the equivalent element;
|
|
|
1259 -- otherwise, it returns No_Element.
|
|
111
|
1260
|
|
|
1261 function Contains (Container : Set; Item : Element_Type) return Boolean with
|
|
|
1262 Global => null,
|
|
|
1263 Post => Contains'Result = Contains (Model (Container), Item);
|
|
|
1264 pragma Annotate (GNATprove, Inline_For_Proof, Contains);
|
|
|
1265
|
|
|
1266 function Has_Element (Container : Set; Position : Cursor) return Boolean
|
|
|
1267 with
|
|
|
1268 Global => null,
|
|
|
1269 Post =>
|
|
|
1270 Has_Element'Result = P.Has_Key (Positions (Container), Position);
|
|
|
1271 pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
|
|
|
1272
|
|
|
1273 function Default_Modulus (Capacity : Count_Type) return Hash_Type with
|
|
|
1274 Global => null;
|
|
|
1275
|
|
|
1276 generic
|
|
|
1277 type Key_Type (<>) is private;
|
|
|
1278
|
|
|
1279 with function Key (Element : Element_Type) return Key_Type;
|
|
|
1280
|
|
|
1281 with function Hash (Key : Key_Type) return Hash_Type;
|
|
|
1282
|
|
|
1283 with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
|
|
|
1284
|
|
|
1285 package Generic_Keys with SPARK_Mode is
|
|
|
1286
|
|
|
1287 package Formal_Model with Ghost is
|
|
|
1288
|
|
|
1289 function M_Included_Except
|
|
|
1290 (Left : M.Set;
|
|
|
1291 Right : M.Set;
|
|
|
1292 Key : Key_Type) return Boolean
|
|
|
1293 with
|
|
|
1294 Global => null,
|
|
|
1295 Post =>
|
|
|
1296 M_Included_Except'Result =
|
|
|
1297 (for all E of Left =>
|
|
|
1298 Contains (Right, E)
|
|
|
1299 or Equivalent_Keys (Generic_Keys.Key (E), Key));
|
|
|
1300
|
|
|
1301 end Formal_Model;
|
|
|
1302 use Formal_Model;
|
|
|
1303
|
|
|
1304 function Key (Container : Set; Position : Cursor) return Key_Type with
|
|
|
1305 Global => null,
|
|
|
1306 Post => Key'Result = Key (Element (Container, Position));
|
|
|
1307 pragma Annotate (GNATprove, Inline_For_Proof, Key);
|
|
|
1308
|
|
|
1309 function Element (Container : Set; Key : Key_Type) return Element_Type
|
|
|
1310 with
|
|
|
1311 Global => null,
|
|
|
1312 Pre => Contains (Container, Key),
|
|
|
1313 Post =>
|
|
|
1314 Element'Result = Element (Container, Find (Container, Key));
|
|
|
1315 pragma Annotate (GNATprove, Inline_For_Proof, Element);
|
|
|
1316
|
|
|
1317 procedure Replace
|
|
|
1318 (Container : in out Set;
|
|
|
1319 Key : Key_Type;
|
|
|
1320 New_Item : Element_Type)
|
|
|
1321 with
|
|
|
1322 Global => null,
|
|
|
1323 Pre => Contains (Container, Key),
|
|
|
1324 Post =>
|
|
|
1325 Length (Container) = Length (Container)'Old
|
|
|
1326
|
|
|
1327 -- Key now maps to New_Item
|
|
|
1328
|
|
|
1329 and Element (Container, Key) = New_Item
|
|
|
1330
|
|
|
1331 -- New_Item is contained in Container
|
|
|
1332
|
|
|
1333 and Contains (Model (Container), New_Item)
|
|
|
1334
|
|
|
1335 -- Other elements are preserved
|
|
|
1336
|
|
|
1337 and M_Included_Except
|
|
|
1338 (Model (Container)'Old,
|
|
|
1339 Model (Container),
|
|
|
1340 Key)
|
|
|
1341 and M.Included_Except
|
|
|
1342 (Model (Container),
|
|
|
1343 Model (Container)'Old,
|
|
|
1344 New_Item)
|
|
|
1345
|
|
|
1346 -- Mapping from cursors to elements is preserved
|
|
|
1347
|
|
|
1348 and Mapping_Preserved_Except
|
|
|
1349 (E_Left => Elements (Container)'Old,
|
|
|
1350 E_Right => Elements (Container),
|
|
|
1351 P_Left => Positions (Container)'Old,
|
|
|
1352 P_Right => Positions (Container),
|
|
|
1353 Position => Find (Container, Key))
|
|
|
1354 and Positions (Container) = Positions (Container)'Old;
|
|
|
1355
|
|
|
1356 procedure Exclude (Container : in out Set; Key : Key_Type) with
|
|
|
1357 Global => null,
|
|
|
1358 Post => not Contains (Container, Key),
|
|
|
1359 Contract_Cases =>
|
|
|
1360
|
|
|
1361 -- If Key is not in Container, nothing is changed
|
|
|
1362
|
|
|
1363 (not Contains (Container, Key) =>
|
|
|
1364 Model (Container) = Model (Container)'Old
|
|
|
1365 and Elements (Container) = Elements (Container)'Old
|
|
|
1366 and Positions (Container) = Positions (Container)'Old,
|
|
|
1367
|
|
|
1368 -- Otherwise, Key is removed from Container
|
|
|
1369
|
|
|
1370 others =>
|
|
|
1371 Length (Container) = Length (Container)'Old - 1
|
|
|
1372
|
|
|
1373 -- Other elements are preserved
|
|
|
1374
|
|
|
1375 and Model (Container) <= Model (Container)'Old
|
|
|
1376 and M_Included_Except
|
|
|
1377 (Model (Container)'Old,
|
|
|
1378 Model (Container),
|
|
|
1379 Key)
|
|
|
1380
|
|
|
1381 -- Mapping from cursors to elements is preserved
|
|
|
1382
|
|
|
1383 and Mapping_Preserved
|
|
|
1384 (E_Left => Elements (Container),
|
|
|
1385 E_Right => Elements (Container)'Old,
|
|
|
1386 P_Left => Positions (Container),
|
|
|
1387 P_Right => Positions (Container)'Old)
|
|
|
1388 and P.Keys_Included_Except
|
|
|
1389 (Positions (Container)'Old,
|
|
|
1390 Positions (Container),
|
|
|
1391 Find (Container, Key)'Old));
|
|
|
1392
|
|
|
1393 procedure Delete (Container : in out Set; Key : Key_Type) with
|
|
|
1394 Global => null,
|
|
|
1395 Pre => Contains (Container, Key),
|
|
|
1396 Post =>
|
|
|
1397 Length (Container) = Length (Container)'Old - 1
|
|
|
1398
|
|
|
1399 -- Key is no longer in Container
|
|
|
1400
|
|
|
1401 and not Contains (Container, Key)
|
|
|
1402
|
|
|
1403 -- Other elements are preserved
|
|
|
1404
|
|
|
1405 and Model (Container) <= Model (Container)'Old
|
|
|
1406 and M_Included_Except
|
|
|
1407 (Model (Container)'Old,
|
|
|
1408 Model (Container),
|
|
|
1409 Key)
|
|
|
1410
|
|
|
1411 -- Mapping from cursors to elements is preserved
|
|
|
1412
|
|
|
1413 and Mapping_Preserved
|
|
|
1414 (E_Left => Elements (Container),
|
|
|
1415 E_Right => Elements (Container)'Old,
|
|
|
1416 P_Left => Positions (Container),
|
|
|
1417 P_Right => Positions (Container)'Old)
|
|
|
1418 and P.Keys_Included_Except
|
|
|
1419 (Positions (Container)'Old,
|
|
|
1420 Positions (Container),
|
|
|
1421 Find (Container, Key)'Old);
|
|
|
1422
|
|
|
1423 function Find (Container : Set; Key : Key_Type) return Cursor with
|
|
|
1424 Global => null,
|
|
|
1425 Contract_Cases =>
|
|
|
1426
|
|
|
1427 -- If Key is not contained in Container, Find returns No_Element
|
|
|
1428
|
|
|
1429 ((for all E of Model (Container) =>
|
|
|
1430 not Equivalent_Keys (Key, Generic_Keys.Key (E))) =>
|
|
|
1431 Find'Result = No_Element,
|
|
|
1432
|
|
|
1433 -- Otherwise, Find returns a valid cursor in Container
|
|
|
1434
|
|
|
1435 others =>
|
|
|
1436 P.Has_Key (Positions (Container), Find'Result)
|
|
|
1437
|
|
|
1438 -- The key designated by the result of Find is Key
|
|
|
1439
|
|
|
1440 and Equivalent_Keys
|
|
|
1441 (Generic_Keys.Key (Container, Find'Result), Key));
|
|
|
1442
|
|
|
1443 function Contains (Container : Set; Key : Key_Type) return Boolean with
|
|
|
1444 Global => null,
|
|
|
1445 Post =>
|
|
|
1446 Contains'Result =
|
|
|
1447 (for some E of Model (Container) =>
|
|
|
1448 Equivalent_Keys (Key, Generic_Keys.Key (E)));
|
|
|
1449
|
|
|
1450 end Generic_Keys;
|
|
|
1451
|
|
|
1452 private
|
|
|
1453 pragma SPARK_Mode (Off);
|
|
|
1454
|
|
|
1455 pragma Inline (Next);
|
|
|
1456
|
|
|
1457 type Node_Type is
|
|
|
1458 record
|
|
|
1459 Element : Element_Type;
|
|
|
1460 Next : Count_Type;
|
|
|
1461 Has_Element : Boolean := False;
|
|
|
1462 end record;
|
|
|
1463
|
|
|
1464 package HT_Types is new
|
|
|
1465 Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type);
|
|
|
1466
|
|
|
1467 type Set (Capacity : Count_Type; Modulus : Hash_Type) is
|
|
|
1468 new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
|
|
|
1469
|
|
|
1470 use HT_Types;
|
|
|
1471
|
|
|
1472 Empty_Set : constant Set := (Capacity => 0, Modulus => 0, others => <>);
|
|
|
1473
|
|
|
1474 end Ada.Containers.Formal_Hashed_Sets;
|
