|
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 -- --
|
|
131
|
9 -- Copyright (C) 2004-2018, 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)));
|
|
|
358
|
|
|
359 function Equivalent_Sets (Left, Right : Set) return Boolean with
|
|
|
360 Global => null,
|
|
|
361 Post => Equivalent_Sets'Result = (Model (Left) = Model (Right));
|
|
|
362
|
|
|
363 function To_Set (New_Item : Element_Type) return Set with
|
|
|
364 Global => null,
|
|
|
365 Post =>
|
|
|
366 M.Is_Singleton (Model (To_Set'Result), New_Item)
|
|
|
367 and Length (To_Set'Result) = 1
|
|
|
368 and E.Get (Elements (To_Set'Result), 1) = New_Item;
|
|
|
369
|
|
|
370 function Capacity (Container : Set) return Count_Type with
|
|
|
371 Global => null,
|
|
|
372 Post => Capacity'Result = Container.Capacity;
|
|
|
373
|
|
|
374 procedure Reserve_Capacity
|
|
|
375 (Container : in out Set;
|
|
|
376 Capacity : Count_Type)
|
|
|
377 with
|
|
|
378 Global => null,
|
|
|
379 Pre => Capacity <= Container.Capacity,
|
|
|
380 Post =>
|
|
|
381 Model (Container) = Model (Container)'Old
|
|
|
382 and Length (Container)'Old = Length (Container)
|
|
|
383
|
|
|
384 -- Actual elements are preserved
|
|
|
385
|
|
|
386 and E_Elements_Included
|
|
|
387 (Elements (Container), Elements (Container)'Old)
|
|
|
388 and E_Elements_Included
|
|
|
389 (Elements (Container)'Old, Elements (Container));
|
|
|
390
|
|
|
391 function Is_Empty (Container : Set) return Boolean with
|
|
|
392 Global => null,
|
|
|
393 Post => Is_Empty'Result = (Length (Container) = 0);
|
|
|
394
|
|
|
395 procedure Clear (Container : in out Set) with
|
|
|
396 Global => null,
|
|
|
397 Post => Length (Container) = 0 and M.Is_Empty (Model (Container));
|
|
|
398
|
|
|
399 procedure Assign (Target : in out Set; Source : Set) with
|
|
|
400 Global => null,
|
|
|
401 Pre => Target.Capacity >= Length (Source),
|
|
|
402 Post =>
|
|
|
403 Model (Target) = Model (Source)
|
|
|
404 and Length (Target) = Length (Source)
|
|
|
405
|
|
|
406 -- Actual elements are preserved
|
|
|
407
|
|
|
408 and E_Elements_Included (Elements (Target), Elements (Source))
|
|
|
409 and E_Elements_Included (Elements (Source), Elements (Target));
|
|
|
410
|
|
|
411 function Copy
|
|
|
412 (Source : Set;
|
|
|
413 Capacity : Count_Type := 0) return Set
|
|
|
414 with
|
|
|
415 Global => null,
|
|
|
416 Pre => Capacity = 0 or else Capacity >= Source.Capacity,
|
|
|
417 Post =>
|
|
|
418 Model (Copy'Result) = Model (Source)
|
|
|
419 and Elements (Copy'Result) = Elements (Source)
|
|
|
420 and Positions (Copy'Result) = Positions (Source)
|
|
|
421 and (if Capacity = 0 then
|
|
|
422 Copy'Result.Capacity = Source.Capacity
|
|
|
423 else
|
|
|
424 Copy'Result.Capacity = Capacity);
|
|
|
425
|
|
|
426 function Element
|
|
|
427 (Container : Set;
|
|
|
428 Position : Cursor) return Element_Type
|
|
|
429 with
|
|
|
430 Global => null,
|
|
|
431 Pre => Has_Element (Container, Position),
|
|
|
432 Post =>
|
|
|
433 Element'Result =
|
|
|
434 E.Get (Elements (Container), P.Get (Positions (Container), Position));
|
|
|
435 pragma Annotate (GNATprove, Inline_For_Proof, Element);
|
|
|
436
|
|
|
437 procedure Replace_Element
|
|
|
438 (Container : in out Set;
|
|
|
439 Position : Cursor;
|
|
|
440 New_Item : Element_Type)
|
|
|
441 with
|
|
|
442 Global => null,
|
|
|
443 Pre => Has_Element (Container, Position),
|
|
|
444 Post =>
|
|
|
445 Length (Container) = Length (Container)'Old
|
|
|
446
|
|
|
447 -- Position now maps to New_Item
|
|
|
448
|
|
|
449 and Element (Container, Position) = New_Item
|
|
|
450
|
|
|
451 -- New_Item is contained in Container
|
|
|
452
|
|
|
453 and Contains (Model (Container), New_Item)
|
|
|
454
|
|
|
455 -- Other elements are preserved
|
|
|
456
|
|
|
457 and M.Included_Except
|
|
|
458 (Model (Container)'Old,
|
|
|
459 Model (Container),
|
|
|
460 Element (Container, Position)'Old)
|
|
|
461 and M.Included_Except
|
|
|
462 (Model (Container),
|
|
|
463 Model (Container)'Old,
|
|
|
464 New_Item)
|
|
|
465
|
|
|
466 -- Mapping from cursors to elements is preserved
|
|
|
467
|
|
|
468 and Mapping_Preserved_Except
|
|
|
469 (E_Left => Elements (Container)'Old,
|
|
|
470 E_Right => Elements (Container),
|
|
|
471 P_Left => Positions (Container)'Old,
|
|
|
472 P_Right => Positions (Container),
|
|
|
473 Position => Position)
|
|
|
474 and Positions (Container) = Positions (Container)'Old;
|
|
|
475
|
|
|
476 procedure Move (Target : in out Set; Source : in out Set) with
|
|
|
477 Global => null,
|
|
|
478 Pre => Target.Capacity >= Length (Source),
|
|
|
479 Post =>
|
|
|
480 Length (Source) = 0
|
|
|
481 and Model (Target) = Model (Source)'Old
|
|
|
482 and Length (Target) = Length (Source)'Old
|
|
|
483
|
|
|
484 -- Actual elements are preserved
|
|
|
485
|
|
|
486 and E_Elements_Included (Elements (Target), Elements (Source)'Old)
|
|
|
487 and E_Elements_Included (Elements (Source)'Old, Elements (Target));
|
|
|
488
|
|
|
489 procedure Insert
|
|
|
490 (Container : in out Set;
|
|
|
491 New_Item : Element_Type;
|
|
|
492 Position : out Cursor;
|
|
|
493 Inserted : out Boolean)
|
|
|
494 with
|
|
|
495 Global => null,
|
|
|
496 Pre =>
|
|
|
497 Length (Container) < Container.Capacity
|
|
|
498 or Contains (Container, New_Item),
|
|
|
499 Post =>
|
|
|
500 Contains (Container, New_Item)
|
|
|
501 and Has_Element (Container, Position)
|
|
|
502 and Equivalent_Elements (Element (Container, Position), New_Item),
|
|
|
503 Contract_Cases =>
|
|
|
504
|
|
|
505 -- If New_Item is already in Container, it is not modified and Inserted
|
|
|
506 -- is set to False.
|
|
|
507
|
|
|
508 (Contains (Container, New_Item) =>
|
|
|
509 not Inserted
|
|
|
510 and Model (Container) = Model (Container)'Old
|
|
|
511 and Elements (Container) = Elements (Container)'Old
|
|
|
512 and Positions (Container) = Positions (Container)'Old,
|
|
|
513
|
|
|
514 -- Otherwise, New_Item is inserted in Container and Inserted is set to
|
|
|
515 -- True.
|
|
|
516
|
|
|
517 others =>
|
|
|
518 Inserted
|
|
|
519 and Length (Container) = Length (Container)'Old + 1
|
|
|
520
|
|
|
521 -- Position now maps to New_Item
|
|
|
522
|
|
|
523 and Element (Container, Position) = New_Item
|
|
|
524
|
|
|
525 -- Other elements are preserved
|
|
|
526
|
|
|
527 and Model (Container)'Old <= Model (Container)
|
|
|
528 and M.Included_Except
|
|
|
529 (Model (Container),
|
|
|
530 Model (Container)'Old,
|
|
|
531 New_Item)
|
|
|
532
|
|
|
533 -- Mapping from cursors to elements is preserved
|
|
|
534
|
|
|
535 and Mapping_Preserved
|
|
|
536 (E_Left => Elements (Container)'Old,
|
|
|
537 E_Right => Elements (Container),
|
|
|
538 P_Left => Positions (Container)'Old,
|
|
|
539 P_Right => Positions (Container))
|
|
|
540 and P.Keys_Included_Except
|
|
|
541 (Positions (Container),
|
|
|
542 Positions (Container)'Old,
|
|
|
543 Position));
|
|
|
544
|
|
|
545 procedure Insert (Container : in out Set; New_Item : Element_Type) with
|
|
|
546 Global => null,
|
|
|
547 Pre => Length (Container) < Container.Capacity
|
|
|
548 and then (not Contains (Container, New_Item)),
|
|
|
549 Post =>
|
|
|
550 Length (Container) = Length (Container)'Old + 1
|
|
|
551 and Contains (Container, New_Item)
|
|
|
552 and Element (Container, Find (Container, New_Item)) = New_Item
|
|
|
553
|
|
|
554 -- Other elements are preserved
|
|
|
555
|
|
|
556 and Model (Container)'Old <= Model (Container)
|
|
|
557 and M.Included_Except
|
|
|
558 (Model (Container),
|
|
|
559 Model (Container)'Old,
|
|
|
560 New_Item)
|
|
|
561
|
|
|
562 -- Mapping from cursors to elements is preserved
|
|
|
563
|
|
|
564 and Mapping_Preserved
|
|
|
565 (E_Left => Elements (Container)'Old,
|
|
|
566 E_Right => Elements (Container),
|
|
|
567 P_Left => Positions (Container)'Old,
|
|
|
568 P_Right => Positions (Container))
|
|
|
569 and P.Keys_Included_Except
|
|
|
570 (Positions (Container),
|
|
|
571 Positions (Container)'Old,
|
|
|
572 Find (Container, New_Item));
|
|
|
573
|
|
|
574 procedure Include (Container : in out Set; New_Item : Element_Type) with
|
|
|
575 Global => null,
|
|
|
576 Pre =>
|
|
|
577 Length (Container) < Container.Capacity
|
|
|
578 or Contains (Container, New_Item),
|
|
|
579 Post =>
|
|
|
580 Contains (Container, New_Item)
|
|
|
581 and Element (Container, Find (Container, New_Item)) = New_Item,
|
|
|
582 Contract_Cases =>
|
|
|
583
|
|
|
584 -- If an element equivalent to New_Item is already in Container, it is
|
|
|
585 -- replaced by New_Item.
|
|
|
586
|
|
|
587 (Contains (Container, New_Item) =>
|
|
|
588
|
|
|
589 -- Elements are preserved modulo equivalence
|
|
|
590
|
|
|
591 Model (Container) = Model (Container)'Old
|
|
|
592
|
|
|
593 -- Cursors are preserved
|
|
|
594
|
|
|
595 and Positions (Container) = Positions (Container)'Old
|
|
|
596
|
|
|
597 -- The actual value of other elements is preserved
|
|
|
598
|
|
|
599 and E.Equal_Except
|
|
|
600 (Elements (Container)'Old,
|
|
|
601 Elements (Container),
|
|
|
602 P.Get (Positions (Container), Find (Container, New_Item))),
|
|
|
603
|
|
|
604 -- Otherwise, New_Item is inserted in Container
|
|
|
605
|
|
|
606 others =>
|
|
|
607 Length (Container) = Length (Container)'Old + 1
|
|
|
608
|
|
|
609 -- Other elements are preserved
|
|
|
610
|
|
|
611 and Model (Container)'Old <= Model (Container)
|
|
|
612 and M.Included_Except
|
|
|
613 (Model (Container),
|
|
|
614 Model (Container)'Old,
|
|
|
615 New_Item)
|
|
|
616
|
|
|
617 -- Mapping from cursors to elements is preserved
|
|
|
618
|
|
|
619 and Mapping_Preserved
|
|
|
620 (E_Left => Elements (Container)'Old,
|
|
|
621 E_Right => Elements (Container),
|
|
|
622 P_Left => Positions (Container)'Old,
|
|
|
623 P_Right => Positions (Container))
|
|
|
624 and P.Keys_Included_Except
|
|
|
625 (Positions (Container),
|
|
|
626 Positions (Container)'Old,
|
|
|
627 Find (Container, New_Item)));
|
|
|
628
|
|
|
629 procedure Replace (Container : in out Set; New_Item : Element_Type) with
|
|
|
630 Global => null,
|
|
|
631 Pre => Contains (Container, New_Item),
|
|
|
632 Post =>
|
|
|
633
|
|
|
634 -- Elements are preserved modulo equivalence
|
|
|
635
|
|
|
636 Model (Container) = Model (Container)'Old
|
|
|
637 and Contains (Container, New_Item)
|
|
|
638
|
|
|
639 -- Cursors are preserved
|
|
|
640
|
|
|
641 and Positions (Container) = Positions (Container)'Old
|
|
|
642
|
|
|
643 -- The element equivalent to New_Item in Container is replaced by
|
|
|
644 -- New_Item.
|
|
|
645
|
|
|
646 and Element (Container, Find (Container, New_Item)) = New_Item
|
|
|
647 and E.Equal_Except
|
|
|
648 (Elements (Container)'Old,
|
|
|
649 Elements (Container),
|
|
|
650 P.Get (Positions (Container), Find (Container, New_Item)));
|
|
|
651
|
|
|
652 procedure Exclude (Container : in out Set; Item : Element_Type) with
|
|
|
653 Global => null,
|
|
|
654 Post => not Contains (Container, Item),
|
|
|
655 Contract_Cases =>
|
|
|
656
|
|
|
657 -- If Item is not in Container, nothing is changed
|
|
|
658
|
|
|
659 (not Contains (Container, Item) =>
|
|
|
660 Model (Container) = Model (Container)'Old
|
|
|
661 and Elements (Container) = Elements (Container)'Old
|
|
|
662 and Positions (Container) = Positions (Container)'Old,
|
|
|
663
|
|
|
664 -- Otherwise, Item is removed from Container
|
|
|
665
|
|
|
666 others =>
|
|
|
667 Length (Container) = Length (Container)'Old - 1
|
|
|
668
|
|
|
669 -- Other elements are preserved
|
|
|
670
|
|
|
671 and Model (Container) <= Model (Container)'Old
|
|
|
672 and M.Included_Except
|
|
|
673 (Model (Container)'Old,
|
|
|
674 Model (Container),
|
|
|
675 Item)
|
|
|
676
|
|
|
677 -- Mapping from cursors to elements is preserved
|
|
|
678
|
|
|
679 and Mapping_Preserved
|
|
|
680 (E_Left => Elements (Container),
|
|
|
681 E_Right => Elements (Container)'Old,
|
|
|
682 P_Left => Positions (Container),
|
|
|
683 P_Right => Positions (Container)'Old)
|
|
|
684 and P.Keys_Included_Except
|
|
|
685 (Positions (Container)'Old,
|
|
|
686 Positions (Container),
|
|
|
687 Find (Container, Item)'Old));
|
|
|
688
|
|
|
689 procedure Delete (Container : in out Set; Item : Element_Type) with
|
|
|
690 Global => null,
|
|
|
691 Pre => Contains (Container, Item),
|
|
|
692 Post =>
|
|
|
693 Length (Container) = Length (Container)'Old - 1
|
|
|
694
|
|
|
695 -- Item is no longer in Container
|
|
|
696
|
|
|
697 and not Contains (Container, Item)
|
|
|
698
|
|
|
699 -- Other elements are preserved
|
|
|
700
|
|
|
701 and Model (Container) <= Model (Container)'Old
|
|
|
702 and M.Included_Except
|
|
|
703 (Model (Container)'Old,
|
|
|
704 Model (Container),
|
|
|
705 Item)
|
|
|
706
|
|
|
707 -- Mapping from cursors to elements is preserved
|
|
|
708
|
|
|
709 and Mapping_Preserved
|
|
|
710 (E_Left => Elements (Container),
|
|
|
711 E_Right => Elements (Container)'Old,
|
|
|
712 P_Left => Positions (Container),
|
|
|
713 P_Right => Positions (Container)'Old)
|
|
|
714 and P.Keys_Included_Except
|
|
|
715 (Positions (Container)'Old,
|
|
|
716 Positions (Container),
|
|
|
717 Find (Container, Item)'Old);
|
|
|
718
|
|
|
719 procedure Delete (Container : in out Set; Position : in out Cursor) with
|
|
|
720 Global => null,
|
|
|
721 Pre => Has_Element (Container, Position),
|
|
|
722 Post =>
|
|
|
723 Position = No_Element
|
|
|
724 and Length (Container) = Length (Container)'Old - 1
|
|
|
725
|
|
|
726 -- The element at position Position is no longer in Container
|
|
|
727
|
|
|
728 and not Contains (Container, Element (Container, Position)'Old)
|
|
|
729 and not P.Has_Key (Positions (Container), Position'Old)
|
|
|
730
|
|
|
731 -- Other elements are preserved
|
|
|
732
|
|
|
733 and Model (Container) <= Model (Container)'Old
|
|
|
734 and M.Included_Except
|
|
|
735 (Model (Container)'Old,
|
|
|
736 Model (Container),
|
|
|
737 Element (Container, Position)'Old)
|
|
|
738
|
|
|
739 -- Mapping from cursors to elements is preserved
|
|
|
740
|
|
|
741 and Mapping_Preserved
|
|
|
742 (E_Left => Elements (Container),
|
|
|
743 E_Right => Elements (Container)'Old,
|
|
|
744 P_Left => Positions (Container),
|
|
|
745 P_Right => Positions (Container)'Old)
|
|
|
746 and P.Keys_Included_Except
|
|
|
747 (Positions (Container)'Old,
|
|
|
748 Positions (Container),
|
|
|
749 Position'Old);
|
|
|
750
|
|
|
751 procedure Union (Target : in out Set; Source : Set) with
|
|
|
752 Global => null,
|
|
|
753 Pre =>
|
|
|
754 Length (Source) - Length (Target and Source) <=
|
|
|
755 Target.Capacity - Length (Target),
|
|
|
756 Post =>
|
|
|
757 Length (Target) = Length (Target)'Old
|
|
|
758 - M.Num_Overlaps (Model (Target)'Old, Model (Source))
|
|
|
759 + Length (Source)
|
|
|
760
|
|
|
761 -- Elements already in Target are still in Target
|
|
|
762
|
|
|
763 and Model (Target)'Old <= Model (Target)
|
|
|
764
|
|
|
765 -- Elements of Source are included in Target
|
|
|
766
|
|
|
767 and Model (Source) <= Model (Target)
|
|
|
768
|
|
|
769 -- Elements of Target come from either Source or Target
|
|
|
770
|
|
|
771 and M.Included_In_Union
|
|
|
772 (Model (Target), Model (Source), Model (Target)'Old)
|
|
|
773
|
|
|
774 -- Actual value of elements come from either Left or Right
|
|
|
775
|
|
|
776 and E_Elements_Included
|
|
|
777 (Elements (Target),
|
|
|
778 Model (Target)'Old,
|
|
|
779 Elements (Target)'Old,
|
|
|
780 Elements (Source))
|
|
|
781
|
|
|
782 and E_Elements_Included
|
|
|
783 (Elements (Target)'Old, Model (Target)'Old, Elements (Target))
|
|
|
784
|
|
|
785 and E_Elements_Included
|
|
|
786 (Elements (Source),
|
|
|
787 Model (Target)'Old,
|
|
|
788 Elements (Source),
|
|
|
789 Elements (Target))
|
|
|
790
|
|
|
791 -- Mapping from cursors of Target to elements is preserved
|
|
|
792
|
|
|
793 and Mapping_Preserved
|
|
|
794 (E_Left => Elements (Target)'Old,
|
|
|
795 E_Right => Elements (Target),
|
|
|
796 P_Left => Positions (Target)'Old,
|
|
|
797 P_Right => Positions (Target));
|
|
|
798
|
|
|
799 function Union (Left, Right : Set) return Set with
|
|
|
800 Global => null,
|
|
|
801 Pre => Length (Left) <= Count_Type'Last - Length (Right),
|
|
|
802 Post =>
|
|
|
803 Length (Union'Result) = Length (Left)
|
|
|
804 - M.Num_Overlaps (Model (Left), Model (Right))
|
|
|
805 + Length (Right)
|
|
|
806
|
|
|
807 -- Elements of Left and Right are in the result of Union
|
|
|
808
|
|
|
809 and Model (Left) <= Model (Union'Result)
|
|
|
810 and Model (Right) <= Model (Union'Result)
|
|
|
811
|
|
|
812 -- Elements of the result of union come from either Left or Right
|
|
|
813
|
|
|
814 and
|
|
|
815 M.Included_In_Union
|
|
|
816 (Model (Union'Result), Model (Left), Model (Right))
|
|
|
817
|
|
|
818 -- Actual value of elements come from either Left or Right
|
|
|
819
|
|
|
820 and E_Elements_Included
|
|
|
821 (Elements (Union'Result),
|
|
|
822 Model (Left),
|
|
|
823 Elements (Left),
|
|
|
824 Elements (Right))
|
|
|
825
|
|
|
826 and E_Elements_Included
|
|
|
827 (Elements (Left), Model (Left), Elements (Union'Result))
|
|
|
828
|
|
|
829 and E_Elements_Included
|
|
|
830 (Elements (Right),
|
|
|
831 Model (Left),
|
|
|
832 Elements (Right),
|
|
|
833 Elements (Union'Result));
|
|
|
834
|
|
|
835 function "or" (Left, Right : Set) return Set renames Union;
|
|
|
836
|
|
|
837 procedure Intersection (Target : in out Set; Source : Set) with
|
|
|
838 Global => null,
|
|
|
839 Post =>
|
|
|
840 Length (Target) =
|
|
|
841 M.Num_Overlaps (Model (Target)'Old, Model (Source))
|
|
|
842
|
|
|
843 -- Elements of Target were already in Target
|
|
|
844
|
|
|
845 and Model (Target) <= Model (Target)'Old
|
|
|
846
|
|
|
847 -- Elements of Target are in Source
|
|
|
848
|
|
|
849 and Model (Target) <= Model (Source)
|
|
|
850
|
|
|
851 -- Elements both in Source and Target are in the intersection
|
|
|
852
|
|
|
853 and M.Includes_Intersection
|
|
|
854 (Model (Target), Model (Source), Model (Target)'Old)
|
|
|
855
|
|
|
856 -- Actual value of elements of Target is preserved
|
|
|
857
|
|
|
858 and E_Elements_Included (Elements (Target), Elements (Target)'Old)
|
|
|
859 and E_Elements_Included
|
|
|
860 (Elements (Target)'Old, Model (Source), Elements (Target))
|
|
|
861
|
|
|
862 -- Mapping from cursors of Target to elements is preserved
|
|
|
863
|
|
|
864 and Mapping_Preserved
|
|
|
865 (E_Left => Elements (Target),
|
|
|
866 E_Right => Elements (Target)'Old,
|
|
|
867 P_Left => Positions (Target),
|
|
|
868 P_Right => Positions (Target)'Old);
|
|
|
869
|
|
|
870 function Intersection (Left, Right : Set) return Set with
|
|
|
871 Global => null,
|
|
|
872 Post =>
|
|
|
873 Length (Intersection'Result) =
|
|
|
874 M.Num_Overlaps (Model (Left), Model (Right))
|
|
|
875
|
|
|
876 -- Elements in the result of Intersection are in Left and Right
|
|
|
877
|
|
|
878 and Model (Intersection'Result) <= Model (Left)
|
|
|
879 and Model (Intersection'Result) <= Model (Right)
|
|
|
880
|
|
|
881 -- Elements both in Left and Right are in the result of Intersection
|
|
|
882
|
|
|
883 and M.Includes_Intersection
|
|
|
884 (Model (Intersection'Result), Model (Left), Model (Right))
|
|
|
885
|
|
|
886 -- Actual value of elements come from Left
|
|
|
887
|
|
|
888 and E_Elements_Included
|
|
|
889 (Elements (Intersection'Result), Elements (Left))
|
|
|
890
|
|
|
891 and E_Elements_Included
|
|
|
892 (Elements (Left), Model (Right),
|
|
|
893 Elements (Intersection'Result));
|
|
|
894
|
|
|
895 function "and" (Left, Right : Set) return Set renames Intersection;
|
|
|
896
|
|
|
897 procedure Difference (Target : in out Set; Source : Set) with
|
|
|
898 Global => null,
|
|
|
899 Post =>
|
|
|
900 Length (Target) = Length (Target)'Old -
|
|
|
901 M.Num_Overlaps (Model (Target)'Old, Model (Source))
|
|
|
902
|
|
|
903 -- Elements of Target were already in Target
|
|
|
904
|
|
|
905 and Model (Target) <= Model (Target)'Old
|
|
|
906
|
|
|
907 -- Elements of Target are not in Source
|
|
|
908
|
|
|
909 and M.No_Overlap (Model (Target), Model (Source))
|
|
|
910
|
|
|
911 -- Elements in Target but not in Source are in the difference
|
|
|
912
|
|
|
913 and M.Included_In_Union
|
|
|
914 (Model (Target)'Old, Model (Target), Model (Source))
|
|
|
915
|
|
|
916 -- Actual value of elements of Target is preserved
|
|
|
917
|
|
|
918 and E_Elements_Included (Elements (Target), Elements (Target)'Old)
|
|
|
919 and E_Elements_Included
|
|
|
920 (Elements (Target)'Old, Model (Target), Elements (Target))
|
|
|
921
|
|
|
922 -- Mapping from cursors of Target to elements is preserved
|
|
|
923
|
|
|
924 and Mapping_Preserved
|
|
|
925 (E_Left => Elements (Target),
|
|
|
926 E_Right => Elements (Target)'Old,
|
|
|
927 P_Left => Positions (Target),
|
|
|
928 P_Right => Positions (Target)'Old);
|
|
|
929
|
|
|
930 function Difference (Left, Right : Set) return Set with
|
|
|
931 Global => null,
|
|
|
932 Post =>
|
|
|
933 Length (Difference'Result) = Length (Left) -
|
|
|
934 M.Num_Overlaps (Model (Left), Model (Right))
|
|
|
935
|
|
|
936 -- Elements of the result of Difference are in Left
|
|
|
937
|
|
|
938 and Model (Difference'Result) <= Model (Left)
|
|
|
939
|
|
|
940 -- Elements of the result of Difference are in Right
|
|
|
941
|
|
|
942 and M.No_Overlap (Model (Difference'Result), Model (Right))
|
|
|
943
|
|
|
944 -- Elements in Left but not in Right are in the difference
|
|
|
945
|
|
|
946 and M.Included_In_Union
|
|
|
947 (Model (Left), Model (Difference'Result), Model (Right))
|
|
|
948
|
|
|
949 -- Actual value of elements come from Left
|
|
|
950
|
|
|
951 and E_Elements_Included
|
|
|
952 (Elements (Difference'Result), Elements (Left))
|
|
|
953
|
|
|
954 and E_Elements_Included
|
|
|
955 (Elements (Left),
|
|
|
956 Model (Difference'Result),
|
|
|
957 Elements (Difference'Result));
|
|
|
958
|
|
|
959 function "-" (Left, Right : Set) return Set renames Difference;
|
|
|
960
|
|
|
961 procedure Symmetric_Difference (Target : in out Set; Source : Set) with
|
|
|
962 Global => null,
|
|
|
963 Pre =>
|
|
|
964 Length (Source) - Length (Target and Source) <=
|
|
|
965 Target.Capacity - Length (Target) + Length (Target and Source),
|
|
|
966 Post =>
|
|
|
967 Length (Target) = Length (Target)'Old -
|
|
|
968 2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) +
|
|
|
969 Length (Source)
|
|
|
970
|
|
|
971 -- Elements of the difference were not both in Source and in Target
|
|
|
972
|
|
|
973 and M.Not_In_Both (Model (Target), Model (Target)'Old, Model (Source))
|
|
|
974
|
|
|
975 -- Elements in Target but not in Source are in the difference
|
|
|
976
|
|
|
977 and M.Included_In_Union
|
|
|
978 (Model (Target)'Old, Model (Target), Model (Source))
|
|
|
979
|
|
|
980 -- Elements in Source but not in Target are in the difference
|
|
|
981
|
|
|
982 and M.Included_In_Union
|
|
|
983 (Model (Source), Model (Target), Model (Target)'Old)
|
|
|
984
|
|
|
985 -- Actual value of elements come from either Left or Right
|
|
|
986
|
|
|
987 and E_Elements_Included
|
|
|
988 (Elements (Target),
|
|
|
989 Model (Target)'Old,
|
|
|
990 Elements (Target)'Old,
|
|
|
991 Elements (Source))
|
|
|
992
|
|
|
993 and E_Elements_Included
|
|
|
994 (Elements (Target)'Old, Model (Target), Elements (Target))
|
|
|
995
|
|
|
996 and E_Elements_Included
|
|
|
997 (Elements (Source), Model (Target), Elements (Target));
|
|
|
998
|
|
|
999 function Symmetric_Difference (Left, Right : Set) return Set with
|
|
|
1000 Global => null,
|
|
|
1001 Pre => Length (Left) <= Count_Type'Last - Length (Right),
|
|
|
1002 Post =>
|
|
|
1003 Length (Symmetric_Difference'Result) = Length (Left) -
|
|
|
1004 2 * M.Num_Overlaps (Model (Left), Model (Right)) +
|
|
|
1005 Length (Right)
|
|
|
1006
|
|
|
1007 -- Elements of the difference were not both in Left and Right
|
|
|
1008
|
|
|
1009 and M.Not_In_Both
|
|
|
1010 (Model (Symmetric_Difference'Result),
|
|
|
1011 Model (Left),
|
|
|
1012 Model (Right))
|
|
|
1013
|
|
|
1014 -- Elements in Left but not in Right are in the difference
|
|
|
1015
|
|
|
1016 and M.Included_In_Union
|
|
|
1017 (Model (Left),
|
|
|
1018 Model (Symmetric_Difference'Result),
|
|
|
1019 Model (Right))
|
|
|
1020
|
|
|
1021 -- Elements in Right but not in Left are in the difference
|
|
|
1022
|
|
|
1023 and M.Included_In_Union
|
|
|
1024 (Model (Right),
|
|
|
1025 Model (Symmetric_Difference'Result),
|
|
|
1026 Model (Left))
|
|
|
1027
|
|
|
1028 -- Actual value of elements come from either Left or Right
|
|
|
1029
|
|
|
1030 and E_Elements_Included
|
|
|
1031 (Elements (Symmetric_Difference'Result),
|
|
|
1032 Model (Left),
|
|
|
1033 Elements (Left),
|
|
|
1034 Elements (Right))
|
|
|
1035
|
|
|
1036 and E_Elements_Included
|
|
|
1037 (Elements (Left),
|
|
|
1038 Model (Symmetric_Difference'Result),
|
|
|
1039 Elements (Symmetric_Difference'Result))
|
|
|
1040
|
|
|
1041 and E_Elements_Included
|
|
|
1042 (Elements (Right),
|
|
|
1043 Model (Symmetric_Difference'Result),
|
|
|
1044 Elements (Symmetric_Difference'Result));
|
|
|
1045
|
|
|
1046 function "xor" (Left, Right : Set) return Set
|
|
|
1047 renames Symmetric_Difference;
|
|
|
1048
|
|
|
1049 function Overlap (Left, Right : Set) return Boolean with
|
|
|
1050 Global => null,
|
|
|
1051 Post =>
|
|
|
1052 Overlap'Result = not (M.No_Overlap (Model (Left), Model (Right)));
|
|
|
1053
|
|
|
1054 function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with
|
|
|
1055 Global => null,
|
|
|
1056 Post => Is_Subset'Result = (Model (Subset) <= Model (Of_Set));
|
|
|
1057
|
|
|
1058 function First (Container : Set) return Cursor with
|
|
|
1059 Global => null,
|
|
|
1060 Contract_Cases =>
|
|
|
1061 (Length (Container) = 0 =>
|
|
|
1062 First'Result = No_Element,
|
|
|
1063
|
|
|
1064 others =>
|
|
|
1065 Has_Element (Container, First'Result)
|
|
|
1066 and P.Get (Positions (Container), First'Result) = 1);
|
|
|
1067
|
|
|
1068 function Next (Container : Set; Position : Cursor) return Cursor with
|
|
|
1069 Global => null,
|
|
|
1070 Pre =>
|
|
|
1071 Has_Element (Container, Position) or else Position = No_Element,
|
|
|
1072 Contract_Cases =>
|
|
|
1073 (Position = No_Element
|
|
|
1074 or else P.Get (Positions (Container), Position) = Length (Container)
|
|
|
1075 =>
|
|
|
1076 Next'Result = No_Element,
|
|
|
1077
|
|
|
1078 others =>
|
|
|
1079 Has_Element (Container, Next'Result)
|
|
|
1080 and then P.Get (Positions (Container), Next'Result) =
|
|
|
1081 P.Get (Positions (Container), Position) + 1);
|
|
|
1082
|
|
|
1083 procedure Next (Container : Set; Position : in out Cursor) with
|
|
|
1084 Global => null,
|
|
|
1085 Pre =>
|
|
|
1086 Has_Element (Container, Position) or else Position = No_Element,
|
|
|
1087 Contract_Cases =>
|
|
|
1088 (Position = No_Element
|
|
|
1089 or else P.Get (Positions (Container), Position) = Length (Container)
|
|
|
1090 =>
|
|
|
1091 Position = No_Element,
|
|
|
1092
|
|
|
1093 others =>
|
|
|
1094 Has_Element (Container, Position)
|
|
|
1095 and then P.Get (Positions (Container), Position) =
|
|
|
1096 P.Get (Positions (Container), Position'Old) + 1);
|
|
|
1097
|
|
|
1098 function Find
|
|
|
1099 (Container : Set;
|
|
|
1100 Item : Element_Type) return Cursor
|
|
|
1101 with
|
|
|
1102 Global => null,
|
|
|
1103 Contract_Cases =>
|
|
|
1104
|
|
|
1105 -- If Item is not contained in Container, Find returns No_Element
|
|
|
1106
|
|
|
1107 (not Contains (Model (Container), Item) =>
|
|
|
1108 Find'Result = No_Element,
|
|
|
1109
|
|
|
1110 -- Otherwise, Find returns a valid cursor in Container
|
|
|
1111
|
|
|
1112 others =>
|
|
|
1113 P.Has_Key (Positions (Container), Find'Result)
|
|
|
1114 and P.Get (Positions (Container), Find'Result) =
|
|
|
1115 Find (Elements (Container), Item)
|
|
|
1116
|
|
|
1117 -- The element designated by the result of Find is Item
|
|
|
1118
|
|
|
1119 and Equivalent_Elements
|
|
|
1120 (Element (Container, Find'Result), Item));
|
|
|
1121
|
|
|
1122 function Contains (Container : Set; Item : Element_Type) return Boolean with
|
|
|
1123 Global => null,
|
|
|
1124 Post => Contains'Result = Contains (Model (Container), Item);
|
|
|
1125 pragma Annotate (GNATprove, Inline_For_Proof, Contains);
|
|
|
1126
|
|
|
1127 function Has_Element (Container : Set; Position : Cursor) return Boolean
|
|
|
1128 with
|
|
|
1129 Global => null,
|
|
|
1130 Post =>
|
|
|
1131 Has_Element'Result = P.Has_Key (Positions (Container), Position);
|
|
|
1132 pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
|
|
|
1133
|
|
|
1134 function Default_Modulus (Capacity : Count_Type) return Hash_Type with
|
|
|
1135 Global => null;
|
|
|
1136
|
|
|
1137 generic
|
|
|
1138 type Key_Type (<>) is private;
|
|
|
1139
|
|
|
1140 with function Key (Element : Element_Type) return Key_Type;
|
|
|
1141
|
|
|
1142 with function Hash (Key : Key_Type) return Hash_Type;
|
|
|
1143
|
|
|
1144 with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
|
|
|
1145
|
|
|
1146 package Generic_Keys with SPARK_Mode is
|
|
|
1147
|
|
|
1148 package Formal_Model with Ghost is
|
|
|
1149
|
|
|
1150 function M_Included_Except
|
|
|
1151 (Left : M.Set;
|
|
|
1152 Right : M.Set;
|
|
|
1153 Key : Key_Type) return Boolean
|
|
|
1154 with
|
|
|
1155 Global => null,
|
|
|
1156 Post =>
|
|
|
1157 M_Included_Except'Result =
|
|
|
1158 (for all E of Left =>
|
|
|
1159 Contains (Right, E)
|
|
|
1160 or Equivalent_Keys (Generic_Keys.Key (E), Key));
|
|
|
1161
|
|
|
1162 end Formal_Model;
|
|
|
1163 use Formal_Model;
|
|
|
1164
|
|
|
1165 function Key (Container : Set; Position : Cursor) return Key_Type with
|
|
|
1166 Global => null,
|
|
|
1167 Post => Key'Result = Key (Element (Container, Position));
|
|
|
1168 pragma Annotate (GNATprove, Inline_For_Proof, Key);
|
|
|
1169
|
|
|
1170 function Element (Container : Set; Key : Key_Type) return Element_Type
|
|
|
1171 with
|
|
|
1172 Global => null,
|
|
|
1173 Pre => Contains (Container, Key),
|
|
|
1174 Post =>
|
|
|
1175 Element'Result = Element (Container, Find (Container, Key));
|
|
|
1176 pragma Annotate (GNATprove, Inline_For_Proof, Element);
|
|
|
1177
|
|
|
1178 procedure Replace
|
|
|
1179 (Container : in out Set;
|
|
|
1180 Key : Key_Type;
|
|
|
1181 New_Item : Element_Type)
|
|
|
1182 with
|
|
|
1183 Global => null,
|
|
|
1184 Pre => Contains (Container, Key),
|
|
|
1185 Post =>
|
|
|
1186 Length (Container) = Length (Container)'Old
|
|
|
1187
|
|
|
1188 -- Key now maps to New_Item
|
|
|
1189
|
|
|
1190 and Element (Container, Key) = New_Item
|
|
|
1191
|
|
|
1192 -- New_Item is contained in Container
|
|
|
1193
|
|
|
1194 and Contains (Model (Container), New_Item)
|
|
|
1195
|
|
|
1196 -- Other elements are preserved
|
|
|
1197
|
|
|
1198 and M_Included_Except
|
|
|
1199 (Model (Container)'Old,
|
|
|
1200 Model (Container),
|
|
|
1201 Key)
|
|
|
1202 and M.Included_Except
|
|
|
1203 (Model (Container),
|
|
|
1204 Model (Container)'Old,
|
|
|
1205 New_Item)
|
|
|
1206
|
|
|
1207 -- Mapping from cursors to elements is preserved
|
|
|
1208
|
|
|
1209 and Mapping_Preserved_Except
|
|
|
1210 (E_Left => Elements (Container)'Old,
|
|
|
1211 E_Right => Elements (Container),
|
|
|
1212 P_Left => Positions (Container)'Old,
|
|
|
1213 P_Right => Positions (Container),
|
|
|
1214 Position => Find (Container, Key))
|
|
|
1215 and Positions (Container) = Positions (Container)'Old;
|
|
|
1216
|
|
|
1217 procedure Exclude (Container : in out Set; Key : Key_Type) with
|
|
|
1218 Global => null,
|
|
|
1219 Post => not Contains (Container, Key),
|
|
|
1220 Contract_Cases =>
|
|
|
1221
|
|
|
1222 -- If Key is not in Container, nothing is changed
|
|
|
1223
|
|
|
1224 (not Contains (Container, Key) =>
|
|
|
1225 Model (Container) = Model (Container)'Old
|
|
|
1226 and Elements (Container) = Elements (Container)'Old
|
|
|
1227 and Positions (Container) = Positions (Container)'Old,
|
|
|
1228
|
|
|
1229 -- Otherwise, Key is removed from Container
|
|
|
1230
|
|
|
1231 others =>
|
|
|
1232 Length (Container) = Length (Container)'Old - 1
|
|
|
1233
|
|
|
1234 -- Other elements are preserved
|
|
|
1235
|
|
|
1236 and Model (Container) <= Model (Container)'Old
|
|
|
1237 and M_Included_Except
|
|
|
1238 (Model (Container)'Old,
|
|
|
1239 Model (Container),
|
|
|
1240 Key)
|
|
|
1241
|
|
|
1242 -- Mapping from cursors to elements is preserved
|
|
|
1243
|
|
|
1244 and Mapping_Preserved
|
|
|
1245 (E_Left => Elements (Container),
|
|
|
1246 E_Right => Elements (Container)'Old,
|
|
|
1247 P_Left => Positions (Container),
|
|
|
1248 P_Right => Positions (Container)'Old)
|
|
|
1249 and P.Keys_Included_Except
|
|
|
1250 (Positions (Container)'Old,
|
|
|
1251 Positions (Container),
|
|
|
1252 Find (Container, Key)'Old));
|
|
|
1253
|
|
|
1254 procedure Delete (Container : in out Set; Key : Key_Type) with
|
|
|
1255 Global => null,
|
|
|
1256 Pre => Contains (Container, Key),
|
|
|
1257 Post =>
|
|
|
1258 Length (Container) = Length (Container)'Old - 1
|
|
|
1259
|
|
|
1260 -- Key is no longer in Container
|
|
|
1261
|
|
|
1262 and not Contains (Container, Key)
|
|
|
1263
|
|
|
1264 -- Other elements are preserved
|
|
|
1265
|
|
|
1266 and Model (Container) <= Model (Container)'Old
|
|
|
1267 and M_Included_Except
|
|
|
1268 (Model (Container)'Old,
|
|
|
1269 Model (Container),
|
|
|
1270 Key)
|
|
|
1271
|
|
|
1272 -- Mapping from cursors to elements is preserved
|
|
|
1273
|
|
|
1274 and Mapping_Preserved
|
|
|
1275 (E_Left => Elements (Container),
|
|
|
1276 E_Right => Elements (Container)'Old,
|
|
|
1277 P_Left => Positions (Container),
|
|
|
1278 P_Right => Positions (Container)'Old)
|
|
|
1279 and P.Keys_Included_Except
|
|
|
1280 (Positions (Container)'Old,
|
|
|
1281 Positions (Container),
|
|
|
1282 Find (Container, Key)'Old);
|
|
|
1283
|
|
|
1284 function Find (Container : Set; Key : Key_Type) return Cursor with
|
|
|
1285 Global => null,
|
|
|
1286 Contract_Cases =>
|
|
|
1287
|
|
|
1288 -- If Key is not contained in Container, Find returns No_Element
|
|
|
1289
|
|
|
1290 ((for all E of Model (Container) =>
|
|
|
1291 not Equivalent_Keys (Key, Generic_Keys.Key (E))) =>
|
|
|
1292 Find'Result = No_Element,
|
|
|
1293
|
|
|
1294 -- Otherwise, Find returns a valid cursor in Container
|
|
|
1295
|
|
|
1296 others =>
|
|
|
1297 P.Has_Key (Positions (Container), Find'Result)
|
|
|
1298
|
|
|
1299 -- The key designated by the result of Find is Key
|
|
|
1300
|
|
|
1301 and Equivalent_Keys
|
|
|
1302 (Generic_Keys.Key (Container, Find'Result), Key));
|
|
|
1303
|
|
|
1304 function Contains (Container : Set; Key : Key_Type) return Boolean with
|
|
|
1305 Global => null,
|
|
|
1306 Post =>
|
|
|
1307 Contains'Result =
|
|
|
1308 (for some E of Model (Container) =>
|
|
|
1309 Equivalent_Keys (Key, Generic_Keys.Key (E)));
|
|
|
1310
|
|
|
1311 end Generic_Keys;
|
|
|
1312
|
|
|
1313 private
|
|
|
1314 pragma SPARK_Mode (Off);
|
|
|
1315
|
|
|
1316 pragma Inline (Next);
|
|
|
1317
|
|
|
1318 type Node_Type is
|
|
|
1319 record
|
|
|
1320 Element : Element_Type;
|
|
|
1321 Next : Count_Type;
|
|
|
1322 Has_Element : Boolean := False;
|
|
|
1323 end record;
|
|
|
1324
|
|
|
1325 package HT_Types is new
|
|
|
1326 Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type);
|
|
|
1327
|
|
|
1328 type Set (Capacity : Count_Type; Modulus : Hash_Type) is
|
|
|
1329 new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
|
|
|
1330
|
|
|
1331 use HT_Types;
|
|
|
1332
|
|
|
1333 Empty_Set : constant Set := (Capacity => 0, Modulus => 0, others => <>);
|
|
|
1334
|
|
|
1335 end Ada.Containers.Formal_Hashed_Sets;
|
