Mercurial > hg > CbC > CbC_gcc

comparison gcc/ada/libgnat/a-cfhase.ads @ 111:04ced10e8804

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
gcc 7
author kono
date Fri, 27 Oct 2017 22:46:09 +0900
parents
children 84e7813d76e9
comparison
equal deleted inserted replaced
68:561a7518be6b 111:04ced10e8804
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT LIBRARY COMPONENTS --
4 -- --
5 -- A D A . C O N T A I N E R S . F O R M A L _ H A S H E D _ S E T S --
6 -- --
7 -- S p e c --
8 -- --
9 -- Copyright (C) 2004-2017, Free Software Foundation, Inc. --
10 -- --
11 -- This specification is derived from the Ada Reference Manual for use with --
12 -- GNAT. The copyright notice above, and the license provisions that follow --
13 -- apply solely to the contents of the part following the private keyword. --
14 -- --
15 -- GNAT is free software; you can redistribute it and/or modify it under --
16 -- terms of the GNU General Public License as published by the Free Soft- --
17 -- ware Foundation; either version 3, or (at your option) any later ver- --
18 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
19 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
20 -- or FITNESS FOR A PARTICULAR PURPOSE. --
21 -- --
22 -- 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;