Mercurial > hg > CbC > CbC_gcc

comparison gcc/ada/libgnat/a-cforse.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 _ O R D E R 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_Ordered_Sets in
33 -- the 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: Key, Element, Next, Query_Element, Previous,
42 -- Has_Element, Iterate, Reverse_Iterate. This change is motivated by the
43 -- need to have cursors which are valid on different containers (typically
44 -- a 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. The operators "<" and ">" that could not be modified that way
47 -- have been removed.
48
49 with Ada.Containers.Functional_Maps;
50 with Ada.Containers.Functional_Sets;
51 with Ada.Containers.Functional_Vectors;
52 private with Ada.Containers.Red_Black_Trees;
53
54 generic
55 type Element_Type is private;
56
57 with function "<" (Left, Right : Element_Type) return Boolean is <>;
58
59 package Ada.Containers.Formal_Ordered_Sets with
60 SPARK_Mode
61 is
62 pragma Annotate (CodePeer, Skip_Analysis);
63
64 function Equivalent_Elements (Left, Right : Element_Type) return Boolean
65 with
66 Global => null,
67 Post =>
68 Equivalent_Elements'Result =
69 (not (Left < Right) and not (Right < Left));
70 pragma Annotate (GNATprove, Inline_For_Proof, Equivalent_Elements);
71
72 type Set (Capacity : Count_Type) is private with
73 Iterable => (First => First,
74 Next => Next,
75 Has_Element => Has_Element,
76 Element => Element),
77 Default_Initial_Condition => Is_Empty (Set);
78 pragma Preelaborable_Initialization (Set);
79
80 type Cursor is record
81 Node : Count_Type;
82 end record;
83
84 No_Element : constant Cursor := (Node => 0);
85
86 function Length (Container : Set) return Count_Type with
87 Global => null,
88 Post => Length'Result <= Container.Capacity;
89
90 pragma Unevaluated_Use_Of_Old (Allow);
91
92 package Formal_Model with Ghost is
93 subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
94
95 package M is new Ada.Containers.Functional_Sets
96 (Element_Type => Element_Type,
97 Equivalent_Elements => Equivalent_Elements);
98
99 function "="
100 (Left : M.Set;
101 Right : M.Set) return Boolean renames M."=";
102
103 function "<="
104 (Left : M.Set;
105 Right : M.Set) return Boolean renames M."<=";
106
107 package E is new Ada.Containers.Functional_Vectors
108 (Element_Type => Element_Type,
109 Index_Type => Positive_Count_Type);
110
111 function "="
112 (Left : E.Sequence;
113 Right : E.Sequence) return Boolean renames E."=";
114
115 function "<"
116 (Left : E.Sequence;
117 Right : E.Sequence) return Boolean renames E."<";
118
119 function "<="
120 (Left : E.Sequence;
121 Right : E.Sequence) return Boolean renames E."<=";
122
123 function E_Bigger_Than_Range
124 (Container : E.Sequence;
125 Fst : Positive_Count_Type;
126 Lst : Count_Type;
127 Item : Element_Type) return Boolean
128 with
129 Global => null,
130 Pre => Lst <= E.Length (Container),
131 Post =>
132 E_Bigger_Than_Range'Result =
133 (for all I in Fst .. Lst => E.Get (Container, I) < Item);
134 pragma Annotate (GNATprove, Inline_For_Proof, E_Bigger_Than_Range);
135
136 function E_Smaller_Than_Range
137 (Container : E.Sequence;
138 Fst : Positive_Count_Type;
139 Lst : Count_Type;
140 Item : Element_Type) return Boolean
141 with
142 Global => null,
143 Pre => Lst <= E.Length (Container),
144 Post =>
145 E_Smaller_Than_Range'Result =
146 (for all I in Fst .. Lst => Item < E.Get (Container, I));
147 pragma Annotate (GNATprove, Inline_For_Proof, E_Smaller_Than_Range);
148
149 function E_Is_Find
150 (Container : E.Sequence;
151 Item : Element_Type;
152 Position : Count_Type) return Boolean
153 with
154 Global => null,
155 Pre => Position - 1 <= E.Length (Container),
156 Post =>
157 E_Is_Find'Result =
158
159 ((if Position > 0 then
160 E_Bigger_Than_Range (Container, 1, Position - 1, Item))
161
162 and (if Position < E.Length (Container) then
163 E_Smaller_Than_Range
164 (Container,
165 Position + 1,
166 E.Length (Container),
167 Item)));
168 pragma Annotate (GNATprove, Inline_For_Proof, E_Is_Find);
169
170 function Find
171 (Container : E.Sequence;
172 Item : Element_Type) return Count_Type
173 -- Search for Item in Container
174
175 with
176 Global => null,
177 Post =>
178 (if Find'Result > 0 then
179 Find'Result <= E.Length (Container)
180 and Equivalent_Elements (Item, E.Get (Container, Find'Result)));
181
182 function E_Elements_Included
183 (Left : E.Sequence;
184 Right : E.Sequence) return Boolean
185 -- The elements of Left are contained in Right
186
187 with
188 Global => null,
189 Post =>
190 E_Elements_Included'Result =
191 (for all I in 1 .. E.Length (Left) =>
192 Find (Right, E.Get (Left, I)) > 0
193 and then E.Get (Right, Find (Right, E.Get (Left, I))) =
194 E.Get (Left, I));
195 pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
196
197 function E_Elements_Included
198 (Left : E.Sequence;
199 Model : M.Set;
200 Right : E.Sequence) return Boolean
201 -- The elements of Container contained in Model are in Right
202
203 with
204 Global => null,
205 Post =>
206 E_Elements_Included'Result =
207 (for all I in 1 .. E.Length (Left) =>
208 (if M.Contains (Model, E.Get (Left, I)) then
209 Find (Right, E.Get (Left, I)) > 0
210 and then E.Get (Right, Find (Right, E.Get (Left, I))) =
211 E.Get (Left, I)));
212 pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
213
214 function E_Elements_Included
215 (Container : E.Sequence;
216 Model : M.Set;
217 Left : E.Sequence;
218 Right : E.Sequence) return Boolean
219 -- The elements of Container contained in Model are in Left and others
220 -- are in Right.
221
222 with
223 Global => null,
224 Post =>
225 E_Elements_Included'Result =
226 (for all I in 1 .. E.Length (Container) =>
227 (if M.Contains (Model, E.Get (Container, I)) then
228 Find (Left, E.Get (Container, I)) > 0
229 and then E.Get (Left, Find (Left, E.Get (Container, I))) =
230 E.Get (Container, I)
231 else
232 Find (Right, E.Get (Container, I)) > 0
233 and then E.Get (Right, Find (Right, E.Get (Container, I))) =
234 E.Get (Container, I)));
235 pragma Annotate (GNATprove, Inline_For_Proof, E_Elements_Included);
236
237 package P is new Ada.Containers.Functional_Maps
238 (Key_Type => Cursor,
239 Element_Type => Positive_Count_Type,
240 Equivalent_Keys => "=",
241 Enable_Handling_Of_Equivalence => False);
242
243 function "="
244 (Left : P.Map;
245 Right : P.Map) return Boolean renames P."=";
246
247 function "<="
248 (Left : P.Map;
249 Right : P.Map) return Boolean renames P."<=";
250
251 function P_Positions_Shifted
252 (Small : P.Map;
253 Big : P.Map;
254 Cut : Positive_Count_Type;
255 Count : Count_Type := 1) return Boolean
256 with
257 Global => null,
258 Post =>
259 P_Positions_Shifted'Result =
260
261 -- Big contains all cursors of Small
262
263 (P.Keys_Included (Small, Big)
264
265 -- Cursors located before Cut are not moved, cursors located
266 -- after are shifted by Count.
267
268 and (for all I of Small =>
269 (if P.Get (Small, I) < Cut then
270 P.Get (Big, I) = P.Get (Small, I)
271 else
272 P.Get (Big, I) - Count = P.Get (Small, I)))
273
274 -- New cursors of Big (if any) are between Cut and Cut - 1 +
275 -- Count.
276
277 and (for all I of Big =>
278 P.Has_Key (Small, I)
279 or P.Get (Big, I) - Count in Cut - Count .. Cut - 1));
280
281 function Mapping_Preserved
282 (E_Left : E.Sequence;
283 E_Right : E.Sequence;
284 P_Left : P.Map;
285 P_Right : P.Map) return Boolean
286 with
287 Ghost,
288 Global => null,
289 Post =>
290 (if Mapping_Preserved'Result then
291
292 -- Right contains all the cursors of Left
293
294 P.Keys_Included (P_Left, P_Right)
295
296 -- Right contains all the elements of Left
297
298 and E_Elements_Included (E_Left, E_Right)
299
300 -- Mappings from cursors to elements induced by E_Left, P_Left
301 -- and E_Right, P_Right are the same.
302
303 and (for all C of P_Left =>
304 E.Get (E_Left, P.Get (P_Left, C)) =
305 E.Get (E_Right, P.Get (P_Right, C))));
306
307 function Mapping_Preserved_Except
308 (E_Left : E.Sequence;
309 E_Right : E.Sequence;
310 P_Left : P.Map;
311 P_Right : P.Map;
312 Position : Cursor) return Boolean
313 with
314 Ghost,
315 Global => null,
316 Post =>
317 (if Mapping_Preserved_Except'Result then
318
319 -- Right contains all the cursors of Left
320
321 P.Keys_Included (P_Left, P_Right)
322
323 -- Mappings from cursors to elements induced by E_Left, P_Left
324 -- and E_Right, P_Right are the same except for Position.
325
326 and (for all C of P_Left =>
327 (if C /= Position then
328 E.Get (E_Left, P.Get (P_Left, C)) =
329 E.Get (E_Right, P.Get (P_Right, C)))));
330
331 function Model (Container : Set) return M.Set with
332 -- The high-level model of a set is a set of elements. Neither cursors
333 -- nor order of elements are represented in this model. Elements are
334 -- modeled up to equivalence.
335
336 Ghost,
337 Global => null,
338 Post => M.Length (Model'Result) = Length (Container);
339
340 function Elements (Container : Set) return E.Sequence with
341 -- The Elements sequence represents the underlying list structure of
342 -- sets that is used for iteration. It stores the actual values of
343 -- elements in the set. It does not model cursors.
344
345 Ghost,
346 Global => null,
347 Post =>
348 E.Length (Elements'Result) = Length (Container)
349
350 -- It only contains keys contained in Model
351
352 and (for all Item of Elements'Result =>
353 M.Contains (Model (Container), Item))
354
355 -- It contains all the elements contained in Model
356
357 and (for all Item of Model (Container) =>
358 (Find (Elements'Result, Item) > 0
359 and then Equivalent_Elements
360 (E.Get (Elements'Result, Find (Elements'Result, Item)),
361 Item)))
362
363 -- It is sorted in increasing order
364
365 and (for all I in 1 .. Length (Container) =>
366 Find (Elements'Result, E.Get (Elements'Result, I)) = I
367 and
368 E_Is_Find
369 (Elements'Result, E.Get (Elements'Result, I), I));
370 pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Elements);
371
372 function Positions (Container : Set) return P.Map with
373 -- The Positions map is used to model cursors. It only contains valid
374 -- cursors and maps them to their position in the container.
375
376 Ghost,
377 Global => null,
378 Post =>
379 not P.Has_Key (Positions'Result, No_Element)
380
381 -- Positions of cursors are smaller than the container's length
382
383 and then
384 (for all I of Positions'Result =>
385 P.Get (Positions'Result, I) in 1 .. Length (Container)
386
387 -- No two cursors have the same position. Note that we do not
388 -- state that there is a cursor in the map for each position, as
389 -- it is rarely needed.
390
391 and then
392 (for all J of Positions'Result =>
393 (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J)
394 then I = J)));
395
396 procedure Lift_Abstraction_Level (Container : Set) with
397 -- Lift_Abstraction_Level is a ghost procedure that does nothing but
398 -- assume that we can access the same elements by iterating over
399 -- positions or cursors.
400 -- This information is not generally useful except when switching from
401 -- a low-level, cursor-aware view of a container, to a high-level,
402 -- position-based view.
403
404 Ghost,
405 Global => null,
406 Post =>
407 (for all Item of Elements (Container) =>
408 (for some I of Positions (Container) =>
409 E.Get (Elements (Container), P.Get (Positions (Container), I)) =
410 Item));
411
412 function Contains
413 (C : M.Set;
414 K : Element_Type) return Boolean renames M.Contains;
415 -- To improve readability of contracts, we rename the function used to
416 -- search for an element in the model to Contains.
417
418 end Formal_Model;
419 use Formal_Model;
420
421 Empty_Set : constant Set;
422
423 function "=" (Left, Right : Set) return Boolean with
424 Global => null,
425 Post =>
426
427 -- If two sets are equal, they contain the same elements in the same
428 -- order.
429
430 (if "="'Result then Elements (Left) = Elements (Right)
431
432 -- If they are different, then they do not contain the same elements
433
434 else
435 not E_Elements_Included (Elements (Left), Elements (Right))
436 or not E_Elements_Included (Elements (Right), Elements (Left)));
437
438 function Equivalent_Sets (Left, Right : Set) return Boolean with
439 Global => null,
440 Post => Equivalent_Sets'Result = (Model (Left) = Model (Right));
441
442 function To_Set (New_Item : Element_Type) return Set with
443 Global => null,
444 Post =>
445 M.Is_Singleton (Model (To_Set'Result), New_Item)
446 and Length (To_Set'Result) = 1
447 and E.Get (Elements (To_Set'Result), 1) = New_Item;
448
449 function Is_Empty (Container : Set) return Boolean with
450 Global => null,
451 Post => Is_Empty'Result = (Length (Container) = 0);
452
453 procedure Clear (Container : in out Set) with
454 Global => null,
455 Post => Length (Container) = 0 and M.Is_Empty (Model (Container));
456
457 procedure Assign (Target : in out Set; Source : Set) with
458 Global => null,
459 Pre => Target.Capacity >= Length (Source),
460 Post =>
461 Model (Target) = Model (Source)
462 and Elements (Target) = Elements (Source)
463 and Length (Target) = Length (Source);
464
465 function Copy (Source : Set; Capacity : Count_Type := 0) return Set with
466 Global => null,
467 Pre => Capacity = 0 or else Capacity >= Source.Capacity,
468 Post =>
469 Model (Copy'Result) = Model (Source)
470 and Elements (Copy'Result) = Elements (Source)
471 and Positions (Copy'Result) = Positions (Source)
472 and (if Capacity = 0 then
473 Copy'Result.Capacity = Source.Capacity
474 else
475 Copy'Result.Capacity = Capacity);
476
477 function Element
478 (Container : Set;
479 Position : Cursor) return Element_Type
480 with
481 Global => null,
482 Pre => Has_Element (Container, Position),
483 Post =>
484 Element'Result =
485 E.Get (Elements (Container), P.Get (Positions (Container), Position));
486 pragma Annotate (GNATprove, Inline_For_Proof, Element);
487
488 procedure Replace_Element
489 (Container : in out Set;
490 Position : Cursor;
491 New_Item : Element_Type)
492 with
493 Global => null,
494 Pre => Has_Element (Container, Position),
495 Post =>
496 Length (Container) = Length (Container)'Old
497
498 -- Position now maps to New_Item
499
500 and Element (Container, Position) = New_Item
501
502 -- New_Item is contained in Container
503
504 and Contains (Model (Container), New_Item)
505
506 -- Other elements are preserved
507
508 and M.Included_Except
509 (Model (Container)'Old,
510 Model (Container),
511 Element (Container, Position)'Old)
512 and M.Included_Except
513 (Model (Container),
514 Model (Container)'Old,
515 New_Item)
516
517 -- Mapping from cursors to elements is preserved
518
519 and Mapping_Preserved_Except
520 (E_Left => Elements (Container)'Old,
521 E_Right => Elements (Container),
522 P_Left => Positions (Container)'Old,
523 P_Right => Positions (Container),
524 Position => Position)
525 and Positions (Container) = Positions (Container)'Old;
526
527 procedure Move (Target : in out Set; Source : in out Set) with
528 Global => null,
529 Pre => Target.Capacity >= Length (Source),
530 Post =>
531 Model (Target) = Model (Source)'Old
532 and Elements (Target) = Elements (Source)'Old
533 and Length (Source)'Old = Length (Target)
534 and Length (Source) = 0;
535
536 procedure Insert
537 (Container : in out Set;
538 New_Item : Element_Type;
539 Position : out Cursor;
540 Inserted : out Boolean)
541 with
542 Global => null,
543 Pre =>
544 Length (Container) < Container.Capacity
545 or Contains (Container, New_Item),
546 Post =>
547 Contains (Container, New_Item)
548 and Has_Element (Container, Position)
549 and Equivalent_Elements (Element (Container, Position), New_Item)
550 and E_Is_Find
551 (Elements (Container),
552 New_Item,
553 P.Get (Positions (Container), Position)),
554 Contract_Cases =>
555
556 -- If New_Item is already in Container, it is not modified and Inserted
557 -- is set to False.
558
559 (Contains (Container, New_Item) =>
560 not Inserted
561 and Model (Container) = Model (Container)'Old
562 and Elements (Container) = Elements (Container)'Old
563 and Positions (Container) = Positions (Container)'Old,
564
565 -- Otherwise, New_Item is inserted in Container and Inserted is set to
566 -- True
567
568 others =>
569 Inserted
570 and Length (Container) = Length (Container)'Old + 1
571
572 -- Position now maps to New_Item
573
574 and Element (Container, Position) = New_Item
575
576 -- Other elements are preserved
577
578 and Model (Container)'Old <= Model (Container)
579 and M.Included_Except
580 (Model (Container),
581 Model (Container)'Old,
582 New_Item)
583
584 -- The elements of Container located before Position are preserved
585
586 and E.Range_Equal
587 (Left => Elements (Container)'Old,
588 Right => Elements (Container),
589 Fst => 1,
590 Lst => P.Get (Positions (Container), Position) - 1)
591
592 -- Other elements are shifted by 1
593
594 and E.Range_Shifted
595 (Left => Elements (Container)'Old,
596 Right => Elements (Container),
597 Fst => P.Get (Positions (Container), Position),
598 Lst => Length (Container)'Old,
599 Offset => 1)
600
601 -- A new cursor has been inserted at position Position in
602 -- Container.
603
604 and P_Positions_Shifted
605 (Positions (Container)'Old,
606 Positions (Container),
607 Cut => P.Get (Positions (Container), Position)));
608
609 procedure Insert
610 (Container : in out Set;
611 New_Item : Element_Type)
612 with
613 Global => null,
614 Pre =>
615 Length (Container) < Container.Capacity
616 and then (not Contains (Container, New_Item)),
617 Post =>
618 Length (Container) = Length (Container)'Old + 1
619 and Contains (Container, New_Item)
620
621 -- New_Item is inserted in the set
622
623 and E.Get (Elements (Container),
624 Find (Elements (Container), New_Item)) = New_Item
625
626 -- Other mappings are preserved
627
628 and Model (Container)'Old <= Model (Container)
629 and M.Included_Except
630 (Model (Container),
631 Model (Container)'Old,
632 New_Item)
633
634 -- The elements of Container located before New_Item are preserved
635
636 and E.Range_Equal
637 (Left => Elements (Container)'Old,
638 Right => Elements (Container),
639 Fst => 1,
640 Lst => Find (Elements (Container), New_Item) - 1)
641
642 -- Other elements are shifted by 1
643
644 and E.Range_Shifted
645 (Left => Elements (Container)'Old,
646 Right => Elements (Container),
647 Fst => Find (Elements (Container), New_Item),
648 Lst => Length (Container)'Old,
649 Offset => 1)
650
651 -- A new cursor has been inserted in Container
652
653 and P_Positions_Shifted
654 (Positions (Container)'Old,
655 Positions (Container),
656 Cut => Find (Elements (Container), New_Item));
657
658 procedure Include
659 (Container : in out Set;
660 New_Item : Element_Type)
661 with
662 Global => null,
663 Pre =>
664 Length (Container) < Container.Capacity
665 or Contains (Container, New_Item),
666 Post => Contains (Container, New_Item),
667 Contract_Cases =>
668
669 -- If New_Item is already in Container
670
671 (Contains (Container, New_Item) =>
672
673 -- Elements are preserved
674
675 Model (Container)'Old = Model (Container)
676
677 -- Cursors are preserved
678
679 and Positions (Container) = Positions (Container)'Old
680
681 -- The element equivalent to New_Item in Container is replaced by
682 -- New_Item.
683
684 and E.Get (Elements (Container),
685 Find (Elements (Container), New_Item)) = New_Item
686
687 and E.Equal_Except
688 (Elements (Container)'Old,
689 Elements (Container),
690 Find (Elements (Container), New_Item)),
691
692 -- Otherwise, New_Item is inserted in Container
693
694 others =>
695 Length (Container) = Length (Container)'Old + 1
696
697 -- Other elements are preserved
698
699 and Model (Container)'Old <= Model (Container)
700 and M.Included_Except
701 (Model (Container),
702 Model (Container)'Old,
703 New_Item)
704
705 -- New_Item is inserted in Container
706
707 and E.Get (Elements (Container),
708 Find (Elements (Container), New_Item)) = New_Item
709
710 -- The Elements of Container located before New_Item are preserved
711
712 and E.Range_Equal
713 (Left => Elements (Container)'Old,
714 Right => Elements (Container),
715 Fst => 1,
716 Lst => Find (Elements (Container), New_Item) - 1)
717
718 -- Other Elements are shifted by 1
719
720 and E.Range_Shifted
721 (Left => Elements (Container)'Old,
722 Right => Elements (Container),
723 Fst => Find (Elements (Container), New_Item),
724 Lst => Length (Container)'Old,
725 Offset => 1)
726
727 -- A new cursor has been inserted in Container
728
729 and P_Positions_Shifted
730 (Positions (Container)'Old,
731 Positions (Container),
732 Cut => Find (Elements (Container), New_Item)));
733
734 procedure Replace
735 (Container : in out Set;
736 New_Item : Element_Type)
737 with
738 Global => null,
739 Pre => Contains (Container, New_Item),
740 Post =>
741
742 -- Elements are preserved
743
744 Model (Container)'Old = Model (Container)
745
746 -- Cursors are preserved
747
748 and Positions (Container) = Positions (Container)'Old
749
750 -- The element equivalent to New_Item in Container is replaced by
751 -- New_Item.
752
753 and E.Get (Elements (Container),
754 Find (Elements (Container), New_Item)) = New_Item
755 and E.Equal_Except
756 (Elements (Container)'Old,
757 Elements (Container),
758 Find (Elements (Container), New_Item));
759
760 procedure Exclude
761 (Container : in out Set;
762 Item : Element_Type)
763 with
764 Global => null,
765 Post => not Contains (Container, Item),
766 Contract_Cases =>
767
768 -- If Item is not in Container, nothing is changed
769
770 (not Contains (Container, Item) =>
771 Model (Container) = Model (Container)'Old
772 and Elements (Container) = Elements (Container)'Old
773 and Positions (Container) = Positions (Container)'Old,
774
775 -- Otherwise, Item is removed from Container
776
777 others =>
778 Length (Container) = Length (Container)'Old - 1
779
780 -- Other elements are preserved
781
782 and Model (Container) <= Model (Container)'Old
783 and M.Included_Except
784 (Model (Container)'Old,
785 Model (Container),
786 Item)
787
788 -- The elements of Container located before Item are preserved
789
790 and E.Range_Equal
791 (Left => Elements (Container)'Old,
792 Right => Elements (Container),
793 Fst => 1,
794 Lst => Find (Elements (Container), Item)'Old - 1)
795
796 -- The elements located after Item are shifted by 1
797
798 and E.Range_Shifted
799 (Left => Elements (Container),
800 Right => Elements (Container)'Old,
801 Fst => Find (Elements (Container), Item)'Old,
802 Lst => Length (Container),
803 Offset => 1)
804
805 -- A cursor has been removed from Container
806
807 and P_Positions_Shifted
808 (Positions (Container),
809 Positions (Container)'Old,
810 Cut => Find (Elements (Container), Item)'Old));
811
812 procedure Delete
813 (Container : in out Set;
814 Item : Element_Type)
815 with
816 Global => null,
817 Pre => Contains (Container, Item),
818 Post =>
819 Length (Container) = Length (Container)'Old - 1
820
821 -- Item is no longer in Container
822
823 and not Contains (Container, Item)
824
825 -- Other elements are preserved
826
827 and Model (Container) <= Model (Container)'Old
828 and M.Included_Except
829 (Model (Container)'Old,
830 Model (Container),
831 Item)
832
833 -- The elements of Container located before Item are preserved
834
835 and E.Range_Equal
836 (Left => Elements (Container)'Old,
837 Right => Elements (Container),
838 Fst => 1,
839 Lst => Find (Elements (Container), Item)'Old - 1)
840
841 -- The elements located after Item are shifted by 1
842
843 and E.Range_Shifted
844 (Left => Elements (Container),
845 Right => Elements (Container)'Old,
846 Fst => Find (Elements (Container), Item)'Old,
847 Lst => Length (Container),
848 Offset => 1)
849
850 -- A cursor has been removed from Container
851
852 and P_Positions_Shifted
853 (Positions (Container),
854 Positions (Container)'Old,
855 Cut => Find (Elements (Container), Item)'Old);
856
857 procedure Delete
858 (Container : in out Set;
859 Position : in out Cursor)
860 with
861 Global => null,
862 Pre => Has_Element (Container, Position),
863 Post =>
864 Position = No_Element
865 and Length (Container) = Length (Container)'Old - 1
866
867 -- The element at position Position is no longer in Container
868
869 and not Contains (Container, Element (Container, Position)'Old)
870 and not P.Has_Key (Positions (Container), Position'Old)
871
872 -- Other elements are preserved
873
874 and Model (Container) <= Model (Container)'Old
875 and M.Included_Except
876 (Model (Container)'Old,
877 Model (Container),
878 Element (Container, Position)'Old)
879
880 -- The elements of Container located before Position are preserved.
881
882 and E.Range_Equal
883 (Left => Elements (Container)'Old,
884 Right => Elements (Container),
885 Fst => 1,
886 Lst => P.Get (Positions (Container)'Old, Position'Old) - 1)
887
888 -- The elements located after Position are shifted by 1
889
890 and E.Range_Shifted
891 (Left => Elements (Container),
892 Right => Elements (Container)'Old,
893 Fst => P.Get (Positions (Container)'Old, Position'Old),
894 Lst => Length (Container),
895 Offset => 1)
896
897 -- Position has been removed from Container
898
899 and P_Positions_Shifted
900 (Positions (Container),
901 Positions (Container)'Old,
902 Cut => P.Get (Positions (Container)'Old, Position'Old));
903
904 procedure Delete_First (Container : in out Set) with
905 Global => null,
906 Contract_Cases =>
907 (Length (Container) = 0 => Length (Container) = 0,
908 others =>
909 Length (Container) = Length (Container)'Old - 1
910
911 -- The first element has been removed from Container
912
913 and not Contains (Container, First_Element (Container)'Old)
914
915 -- Other elements are preserved
916
917 and Model (Container) <= Model (Container)'Old
918 and M.Included_Except
919 (Model (Container)'Old,
920 Model (Container),
921 First_Element (Container)'Old)
922
923 -- Other elements are shifted by 1
924
925 and E.Range_Shifted
926 (Left => Elements (Container),
927 Right => Elements (Container)'Old,
928 Fst => 1,
929 Lst => Length (Container),
930 Offset => 1)
931
932 -- First has been removed from Container
933
934 and P_Positions_Shifted
935 (Positions (Container),
936 Positions (Container)'Old,
937 Cut => 1));
938
939 procedure Delete_Last (Container : in out Set) with
940 Global => null,
941 Contract_Cases =>
942 (Length (Container) = 0 => Length (Container) = 0,
943 others =>
944 Length (Container) = Length (Container)'Old - 1
945
946 -- The last element has been removed from Container
947
948 and not Contains (Container, Last_Element (Container)'Old)
949
950 -- Other elements are preserved
951
952 and Model (Container) <= Model (Container)'Old
953 and M.Included_Except
954 (Model (Container)'Old,
955 Model (Container),
956 Last_Element (Container)'Old)
957
958 -- Others elements of Container are preserved
959
960 and E.Range_Equal
961 (Left => Elements (Container)'Old,
962 Right => Elements (Container),
963 Fst => 1,
964 Lst => Length (Container))
965
966 -- Last cursor has been removed from Container
967
968 and Positions (Container) <= Positions (Container)'Old);
969
970 procedure Union (Target : in out Set; Source : Set) with
971 Global => null,
972 Pre =>
973 Length (Source) - Length (Target and Source) <=
974 Target.Capacity - Length (Target),
975 Post =>
976 Length (Target) = Length (Target)'Old
977 - M.Num_Overlaps (Model (Target)'Old, Model (Source))
978 + Length (Source)
979
980 -- Elements already in Target are still in Target
981
982 and Model (Target)'Old <= Model (Target)
983
984 -- Elements of Source are included in Target
985
986 and Model (Source) <= Model (Target)
987
988 -- Elements of Target come from either Source or Target
989
990 and
991 M.Included_In_Union
992 (Model (Target), Model (Source), Model (Target)'Old)
993
994 -- Actual value of elements come from either Left or Right
995
996 and
997 E_Elements_Included
998 (Elements (Target),
999 Model (Target)'Old,
1000 Elements (Target)'Old,
1001 Elements (Source))
1002 and
1003 E_Elements_Included
1004 (Elements (Target)'Old, Model (Target)'Old, Elements (Target))
1005 and
1006 E_Elements_Included
1007 (Elements (Source),
1008 Model (Target)'Old,
1009 Elements (Source),
1010 Elements (Target))
1011
1012 -- Mapping from cursors of Target to elements is preserved
1013
1014 and Mapping_Preserved
1015 (E_Left => Elements (Target)'Old,
1016 E_Right => Elements (Target),
1017 P_Left => Positions (Target)'Old,
1018 P_Right => Positions (Target));
1019
1020 function Union (Left, Right : Set) return Set with
1021 Global => null,
1022 Pre => Length (Left) <= Count_Type'Last - Length (Right),
1023 Post =>
1024 Length (Union'Result) = Length (Left)
1025 - M.Num_Overlaps (Model (Left), Model (Right))
1026 + Length (Right)
1027
1028 -- Elements of Left and Right are in the result of Union
1029
1030 and Model (Left) <= Model (Union'Result)
1031 and Model (Right) <= Model (Union'Result)
1032
1033 -- Elements of the result of union come from either Left or Right
1034
1035 and
1036 M.Included_In_Union
1037 (Model (Union'Result), Model (Left), Model (Right))
1038
1039 -- Actual value of elements come from either Left or Right
1040
1041 and
1042 E_Elements_Included
1043 (Elements (Union'Result),
1044 Model (Left),
1045 Elements (Left),
1046 Elements (Right))
1047 and
1048 E_Elements_Included
1049 (Elements (Left), Model (Left), Elements (Union'Result))
1050 and
1051 E_Elements_Included
1052 (Elements (Right),
1053 Model (Left),
1054 Elements (Right),
1055 Elements (Union'Result));
1056
1057 function "or" (Left, Right : Set) return Set renames Union;
1058
1059 procedure Intersection (Target : in out Set; Source : Set) with
1060 Global => null,
1061 Post =>
1062 Length (Target) =
1063 M.Num_Overlaps (Model (Target)'Old, Model (Source))
1064
1065 -- Elements of Target were already in Target
1066
1067 and Model (Target) <= Model (Target)'Old
1068
1069 -- Elements of Target are in Source
1070
1071 and Model (Target) <= Model (Source)
1072
1073 -- Elements both in Source and Target are in the intersection
1074
1075 and
1076 M.Includes_Intersection
1077 (Model (Target), Model (Source), Model (Target)'Old)
1078
1079 -- Actual value of elements of Target is preserved
1080
1081 and E_Elements_Included (Elements (Target), Elements (Target)'Old)
1082 and
1083 E_Elements_Included
1084 (Elements (Target)'Old, Model (Source), Elements (Target))
1085
1086 -- Mapping from cursors of Target to elements is preserved
1087
1088 and Mapping_Preserved
1089 (E_Left => Elements (Target),
1090 E_Right => Elements (Target)'Old,
1091 P_Left => Positions (Target),
1092 P_Right => Positions (Target)'Old);
1093
1094 function Intersection (Left, Right : Set) return Set with
1095 Global => null,
1096 Post =>
1097 Length (Intersection'Result) =
1098 M.Num_Overlaps (Model (Left), Model (Right))
1099
1100 -- Elements in the result of Intersection are in Left and Right
1101
1102 and Model (Intersection'Result) <= Model (Left)
1103 and Model (Intersection'Result) <= Model (Right)
1104
1105 -- Elements both in Left and Right are in the result of Intersection
1106
1107 and
1108 M.Includes_Intersection
1109 (Model (Intersection'Result), Model (Left), Model (Right))
1110
1111 -- Actual value of elements come from Left
1112
1113 and
1114 E_Elements_Included
1115 (Elements (Intersection'Result), Elements (Left))
1116 and
1117 E_Elements_Included
1118 (Elements (Left), Model (Right), Elements (Intersection'Result));
1119
1120 function "and" (Left, Right : Set) return Set renames Intersection;
1121
1122 procedure Difference (Target : in out Set; Source : Set) with
1123 Global => null,
1124 Post =>
1125 Length (Target) = Length (Target)'Old -
1126 M.Num_Overlaps (Model (Target)'Old, Model (Source))
1127
1128 -- Elements of Target were already in Target
1129
1130 and Model (Target) <= Model (Target)'Old
1131
1132 -- Elements of Target are not in Source
1133
1134 and M.No_Overlap (Model (Target), Model (Source))
1135
1136 -- Elements in Target but not in Source are in the difference
1137
1138 and
1139 M.Included_In_Union
1140 (Model (Target)'Old, Model (Target), Model (Source))
1141
1142 -- Actual value of elements of Target is preserved
1143
1144 and E_Elements_Included (Elements (Target), Elements (Target)'Old)
1145 and
1146 E_Elements_Included
1147 (Elements (Target)'Old, Model (Target), Elements (Target))
1148
1149 -- Mapping from cursors of Target to elements is preserved
1150
1151 and Mapping_Preserved
1152 (E_Left => Elements (Target),
1153 E_Right => Elements (Target)'Old,
1154 P_Left => Positions (Target),
1155 P_Right => Positions (Target)'Old);
1156
1157 function Difference (Left, Right : Set) return Set with
1158 Global => null,
1159 Post =>
1160 Length (Difference'Result) = Length (Left) -
1161 M.Num_Overlaps (Model (Left), Model (Right))
1162
1163 -- Elements of the result of Difference are in Left
1164
1165 and Model (Difference'Result) <= Model (Left)
1166
1167 -- Elements of the result of Difference are in Right
1168
1169 and M.No_Overlap (Model (Difference'Result), Model (Right))
1170
1171 -- Elements in Left but not in Right are in the difference
1172
1173 and
1174 M.Included_In_Union
1175 (Model (Left), Model (Difference'Result), Model (Right))
1176
1177 -- Actual value of elements come from Left
1178
1179 and
1180 E_Elements_Included (Elements (Difference'Result), Elements (Left))
1181 and
1182 E_Elements_Included
1183 (Elements (Left),
1184 Model (Difference'Result),
1185 Elements (Difference'Result));
1186
1187 function "-" (Left, Right : Set) return Set renames Difference;
1188
1189 procedure Symmetric_Difference (Target : in out Set; Source : Set) with
1190 Global => null,
1191 Pre =>
1192 Length (Source) - Length (Target and Source) <=
1193 Target.Capacity - Length (Target) + Length (Target and Source),
1194 Post =>
1195 Length (Target) = Length (Target)'Old -
1196 2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) +
1197 Length (Source)
1198
1199 -- Elements of the difference were not both in Source and in Target
1200
1201 and M.Not_In_Both (Model (Target), Model (Target)'Old, Model (Source))
1202
1203 -- Elements in Target but not in Source are in the difference
1204
1205 and
1206 M.Included_In_Union
1207 (Model (Target)'Old, Model (Target), Model (Source))
1208
1209 -- Elements in Source but not in Target are in the difference
1210
1211 and
1212 M.Included_In_Union
1213 (Model (Source), Model (Target), Model (Target)'Old)
1214
1215 -- Actual value of elements come from either Left or Right
1216
1217 and
1218 E_Elements_Included
1219 (Elements (Target),
1220 Model (Target)'Old,
1221 Elements (Target)'Old,
1222 Elements (Source))
1223 and
1224 E_Elements_Included
1225 (Elements (Target)'Old, Model (Target), Elements (Target))
1226 and
1227 E_Elements_Included
1228 (Elements (Source), Model (Target), Elements (Target));
1229
1230 function Symmetric_Difference (Left, Right : Set) return Set with
1231 Global => null,
1232 Pre => Length (Left) <= Count_Type'Last - Length (Right),
1233 Post =>
1234 Length (Symmetric_Difference'Result) = Length (Left) -
1235 2 * M.Num_Overlaps (Model (Left), Model (Right)) +
1236 Length (Right)
1237
1238 -- Elements of the difference were not both in Left and Right
1239
1240 and
1241 M.Not_In_Both
1242 (Model (Symmetric_Difference'Result), Model (Left), Model (Right))
1243
1244 -- Elements in Left but not in Right are in the difference
1245
1246 and
1247 M.Included_In_Union
1248 (Model (Left), Model (Symmetric_Difference'Result), Model (Right))
1249
1250 -- Elements in Right but not in Left are in the difference
1251
1252 and
1253 M.Included_In_Union
1254 (Model (Right), Model (Symmetric_Difference'Result), Model (Left))
1255
1256 -- Actual value of elements come from either Left or Right
1257
1258 and
1259 E_Elements_Included
1260 (Elements (Symmetric_Difference'Result),
1261 Model (Left),
1262 Elements (Left),
1263 Elements (Right))
1264 and
1265 E_Elements_Included
1266 (Elements (Left),
1267 Model (Symmetric_Difference'Result),
1268 Elements (Symmetric_Difference'Result))
1269 and
1270 E_Elements_Included
1271 (Elements (Right),
1272 Model (Symmetric_Difference'Result),
1273 Elements (Symmetric_Difference'Result));
1274
1275 function "xor" (Left, Right : Set) return Set
1276 renames Symmetric_Difference;
1277
1278 function Overlap (Left, Right : Set) return Boolean with
1279 Global => null,
1280 Post =>
1281 Overlap'Result = not (M.No_Overlap (Model (Left), Model (Right)));
1282
1283 function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with
1284 Global => null,
1285 Post => Is_Subset'Result = (Model (Subset) <= Model (Of_Set));
1286
1287 function First (Container : Set) return Cursor with
1288 Global => null,
1289 Contract_Cases =>
1290 (Length (Container) = 0 =>
1291 First'Result = No_Element,
1292
1293 others =>
1294 Has_Element (Container, First'Result)
1295 and P.Get (Positions (Container), First'Result) = 1);
1296
1297 function First_Element (Container : Set) return Element_Type with
1298 Global => null,
1299 Pre => not Is_Empty (Container),
1300 Post =>
1301 First_Element'Result = E.Get (Elements (Container), 1)
1302 and E_Smaller_Than_Range
1303 (Elements (Container),
1304 2,
1305 Length (Container),
1306 First_Element'Result);
1307
1308 function Last (Container : Set) return Cursor with
1309 Global => null,
1310 Contract_Cases =>
1311 (Length (Container) = 0 =>
1312 Last'Result = No_Element,
1313
1314 others =>
1315 Has_Element (Container, Last'Result)
1316 and P.Get (Positions (Container), Last'Result) =
1317 Length (Container));
1318
1319 function Last_Element (Container : Set) return Element_Type with
1320 Global => null,
1321 Pre => not Is_Empty (Container),
1322 Post =>
1323 Last_Element'Result = E.Get (Elements (Container), Length (Container))
1324 and E_Bigger_Than_Range
1325 (Elements (Container),
1326 1,
1327 Length (Container) - 1,
1328 Last_Element'Result);
1329
1330 function Next (Container : Set; Position : Cursor) return Cursor with
1331 Global => null,
1332 Pre =>
1333 Has_Element (Container, Position) or else Position = No_Element,
1334 Contract_Cases =>
1335 (Position = No_Element
1336 or else P.Get (Positions (Container), Position) = Length (Container)
1337 =>
1338 Next'Result = No_Element,
1339
1340 others =>
1341 Has_Element (Container, Next'Result)
1342 and then P.Get (Positions (Container), Next'Result) =
1343 P.Get (Positions (Container), Position) + 1);
1344
1345 procedure Next (Container : Set; Position : in out Cursor) with
1346 Global => null,
1347 Pre =>
1348 Has_Element (Container, Position) or else Position = No_Element,
1349 Contract_Cases =>
1350 (Position = No_Element
1351 or else P.Get (Positions (Container), Position) = Length (Container)
1352 =>
1353 Position = No_Element,
1354
1355 others =>
1356 Has_Element (Container, Position)
1357 and then P.Get (Positions (Container), Position) =
1358 P.Get (Positions (Container), Position'Old) + 1);
1359
1360 function Previous (Container : Set; Position : Cursor) return Cursor with
1361 Global => null,
1362 Pre =>
1363 Has_Element (Container, Position) or else Position = No_Element,
1364 Contract_Cases =>
1365 (Position = No_Element
1366 or else P.Get (Positions (Container), Position) = 1
1367 =>
1368 Previous'Result = No_Element,
1369
1370 others =>
1371 Has_Element (Container, Previous'Result)
1372 and then P.Get (Positions (Container), Previous'Result) =
1373 P.Get (Positions (Container), Position) - 1);
1374
1375 procedure Previous (Container : Set; Position : in out Cursor) with
1376 Global => null,
1377 Pre =>
1378 Has_Element (Container, Position) or else Position = No_Element,
1379 Contract_Cases =>
1380 (Position = No_Element
1381 or else P.Get (Positions (Container), Position) = 1
1382 =>
1383 Position = No_Element,
1384
1385 others =>
1386 Has_Element (Container, Position)
1387 and then P.Get (Positions (Container), Position) =
1388 P.Get (Positions (Container), Position'Old) - 1);
1389
1390 function Find (Container : Set; Item : Element_Type) return Cursor with
1391 Global => null,
1392 Contract_Cases =>
1393
1394 -- If Item is not contained in Container, Find returns No_Element
1395
1396 (not Contains (Model (Container), Item) =>
1397 not P.Has_Key (Positions (Container), Find'Result)
1398 and Find'Result = No_Element,
1399
1400 -- Otherwise, Find returns a valid cursor in Container
1401
1402 others =>
1403 P.Has_Key (Positions (Container), Find'Result)
1404 and P.Get (Positions (Container), Find'Result) =
1405 Find (Elements (Container), Item)
1406
1407 -- The element designated by the result of Find is Item
1408
1409 and Equivalent_Elements
1410 (Element (Container, Find'Result), Item));
1411
1412 function Floor (Container : Set; Item : Element_Type) return Cursor with
1413 Global => null,
1414 Contract_Cases =>
1415 (Length (Container) = 0 or else Item < First_Element (Container) =>
1416 Floor'Result = No_Element,
1417 others =>
1418 Has_Element (Container, Floor'Result)
1419 and
1420 not (Item < E.Get (Elements (Container),
1421 P.Get (Positions (Container), Floor'Result)))
1422 and E_Is_Find
1423 (Elements (Container),
1424 Item,
1425 P.Get (Positions (Container), Floor'Result)));
1426
1427 function Ceiling (Container : Set; Item : Element_Type) return Cursor with
1428 Global => null,
1429 Contract_Cases =>
1430 (Length (Container) = 0 or else Last_Element (Container) < Item =>
1431 Ceiling'Result = No_Element,
1432 others =>
1433 Has_Element (Container, Ceiling'Result)
1434 and
1435 not (E.Get (Elements (Container),
1436 P.Get (Positions (Container), Ceiling'Result)) <
1437 Item)
1438 and E_Is_Find
1439 (Elements (Container),
1440 Item,
1441 P.Get (Positions (Container), Ceiling'Result)));
1442
1443 function Contains (Container : Set; Item : Element_Type) return Boolean with
1444 Global => null,
1445 Post => Contains'Result = Contains (Model (Container), Item);
1446 pragma Annotate (GNATprove, Inline_For_Proof, Contains);
1447
1448 function Has_Element (Container : Set; Position : Cursor) return Boolean
1449 with
1450 Global => null,
1451 Post =>
1452 Has_Element'Result = P.Has_Key (Positions (Container), Position);
1453 pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
1454
1455 generic
1456 type Key_Type (<>) is private;
1457
1458 with function Key (Element : Element_Type) return Key_Type;
1459
1460 with function "<" (Left, Right : Key_Type) return Boolean is <>;
1461
1462 package Generic_Keys with SPARK_Mode is
1463
1464 function Equivalent_Keys (Left, Right : Key_Type) return Boolean with
1465 Global => null,
1466 Post =>
1467 Equivalent_Keys'Result = (not (Left < Right) and not (Right < Left));
1468 pragma Annotate (GNATprove, Inline_For_Proof, Equivalent_Keys);
1469
1470 package Formal_Model with Ghost is
1471 function E_Bigger_Than_Range
1472 (Container : E.Sequence;
1473 Fst : Positive_Count_Type;
1474 Lst : Count_Type;
1475 Key : Key_Type) return Boolean
1476 with
1477 Global => null,
1478 Pre => Lst <= E.Length (Container),
1479 Post =>
1480 E_Bigger_Than_Range'Result =
1481 (for all I in Fst .. Lst =>
1482 Generic_Keys.Key (E.Get (Container, I)) < Key);
1483 pragma Annotate (GNATprove, Inline_For_Proof, E_Bigger_Than_Range);
1484
1485 function E_Smaller_Than_Range
1486 (Container : E.Sequence;
1487 Fst : Positive_Count_Type;
1488 Lst : Count_Type;
1489 Key : Key_Type) return Boolean
1490 with
1491 Global => null,
1492 Pre => Lst <= E.Length (Container),
1493 Post =>
1494 E_Smaller_Than_Range'Result =
1495 (for all I in Fst .. Lst =>
1496 Key < Generic_Keys.Key (E.Get (Container, I)));
1497 pragma Annotate (GNATprove, Inline_For_Proof, E_Smaller_Than_Range);
1498
1499 function E_Is_Find
1500 (Container : E.Sequence;
1501 Key : Key_Type;
1502 Position : Count_Type) return Boolean
1503 with
1504 Global => null,
1505 Pre => Position - 1 <= E.Length (Container),
1506 Post =>
1507 E_Is_Find'Result =
1508
1509 ((if Position > 0 then
1510 E_Bigger_Than_Range (Container, 1, Position - 1, Key))
1511
1512 and (if Position < E.Length (Container) then
1513 E_Smaller_Than_Range
1514 (Container,
1515 Position + 1,
1516 E.Length (Container),
1517 Key)));
1518 pragma Annotate (GNATprove, Inline_For_Proof, E_Is_Find);
1519
1520 function Find
1521 (Container : E.Sequence;
1522 Key : Key_Type) return Count_Type
1523 -- Search for Key in Container
1524
1525 with
1526 Global => null,
1527 Post =>
1528 (if Find'Result > 0 then
1529 Find'Result <= E.Length (Container)
1530 and Equivalent_Keys
1531 (Key, Generic_Keys.Key (E.Get (Container, Find'Result)))
1532 and E_Is_Find (Container, Key, Find'Result));
1533
1534 function M_Included_Except
1535 (Left : M.Set;
1536 Right : M.Set;
1537 Key : Key_Type) return Boolean
1538 with
1539 Global => null,
1540 Post =>
1541 M_Included_Except'Result =
1542 (for all E of Left =>
1543 Contains (Right, E)
1544 or Equivalent_Keys (Generic_Keys.Key (E), Key));
1545 end Formal_Model;
1546 use Formal_Model;
1547
1548 function Key (Container : Set; Position : Cursor) return Key_Type with
1549 Global => null,
1550 Post => Key'Result = Key (Element (Container, Position));
1551 pragma Annotate (GNATprove, Inline_For_Proof, Key);
1552
1553 function Element (Container : Set; Key : Key_Type) return Element_Type
1554 with
1555 Global => null,
1556 Pre => Contains (Container, Key),
1557 Post =>
1558 Element'Result = Element (Container, Find (Container, Key));
1559 pragma Annotate (GNATprove, Inline_For_Proof, Element);
1560
1561 procedure Replace
1562 (Container : in out Set;
1563 Key : Key_Type;
1564 New_Item : Element_Type)
1565 with
1566 Global => null,
1567 Pre => Contains (Container, Key),
1568 Post =>
1569 Length (Container) = Length (Container)'Old
1570
1571 -- Key now maps to New_Item
1572
1573 and Element (Container, Key) = New_Item
1574
1575 -- New_Item is contained in Container
1576
1577 and Contains (Model (Container), New_Item)
1578
1579 -- Other elements are preserved
1580
1581 and M_Included_Except
1582 (Model (Container)'Old,
1583 Model (Container),
1584 Key)
1585 and M.Included_Except
1586 (Model (Container),
1587 Model (Container)'Old,
1588 New_Item)
1589
1590 -- Mapping from cursors to elements is preserved
1591
1592 and Mapping_Preserved_Except
1593 (E_Left => Elements (Container)'Old,
1594 E_Right => Elements (Container),
1595 P_Left => Positions (Container)'Old,
1596 P_Right => Positions (Container),
1597 Position => Find (Container, Key))
1598 and Positions (Container) = Positions (Container)'Old;
1599
1600 procedure Exclude (Container : in out Set; Key : Key_Type) with
1601 Global => null,
1602 Post => not Contains (Container, Key),
1603 Contract_Cases =>
1604
1605 -- If Key is not in Container, nothing is changed
1606
1607 (not Contains (Container, Key) =>
1608 Model (Container) = Model (Container)'Old
1609 and Elements (Container) = Elements (Container)'Old
1610 and Positions (Container) = Positions (Container)'Old,
1611
1612 -- Otherwise, Key is removed from Container
1613
1614 others =>
1615 Length (Container) = Length (Container)'Old - 1
1616
1617 -- Other elements are preserved
1618
1619 and Model (Container) <= Model (Container)'Old
1620 and M_Included_Except
1621 (Model (Container)'Old,
1622 Model (Container),
1623 Key)
1624
1625 -- The elements of Container located before Key are preserved
1626
1627 and E.Range_Equal
1628 (Left => Elements (Container)'Old,
1629 Right => Elements (Container),
1630 Fst => 1,
1631 Lst => Find (Elements (Container), Key)'Old - 1)
1632
1633 -- The elements located after Key are shifted by 1
1634
1635 and E.Range_Shifted
1636 (Left => Elements (Container),
1637 Right => Elements (Container)'Old,
1638 Fst => Find (Elements (Container), Key)'Old,
1639 Lst => Length (Container),
1640 Offset => 1)
1641
1642 -- A cursor has been removed from Container
1643
1644 and P_Positions_Shifted
1645 (Positions (Container),
1646 Positions (Container)'Old,
1647 Cut => Find (Elements (Container), Key)'Old));
1648
1649 procedure Delete (Container : in out Set; Key : Key_Type) with
1650 Global => null,
1651 Pre => Contains (Container, Key),
1652 Post =>
1653 Length (Container) = Length (Container)'Old - 1
1654
1655 -- Key is no longer in Container
1656
1657 and not Contains (Container, Key)
1658
1659 -- Other elements are preserved
1660
1661 and Model (Container) <= Model (Container)'Old
1662 and M_Included_Except
1663 (Model (Container)'Old,
1664 Model (Container),
1665 Key)
1666
1667 -- The elements of Container located before Key are preserved
1668
1669 and E.Range_Equal
1670 (Left => Elements (Container)'Old,
1671 Right => Elements (Container),
1672 Fst => 1,
1673 Lst => Find (Elements (Container), Key)'Old - 1)
1674
1675 -- The elements located after Key are shifted by 1
1676
1677 and E.Range_Shifted
1678 (Left => Elements (Container),
1679 Right => Elements (Container)'Old,
1680 Fst => Find (Elements (Container), Key)'Old,
1681 Lst => Length (Container),
1682 Offset => 1)
1683
1684 -- A cursor has been removed from Container
1685
1686 and P_Positions_Shifted
1687 (Positions (Container),
1688 Positions (Container)'Old,
1689 Cut => Find (Elements (Container), Key)'Old);
1690
1691 function Find (Container : Set; Key : Key_Type) return Cursor with
1692 Global => null,
1693 Contract_Cases =>
1694
1695 -- If Key is not contained in Container, Find returns No_Element
1696
1697 ((for all E of Model (Container) =>
1698 not Equivalent_Keys (Key, Generic_Keys.Key (E))) =>
1699 not P.Has_Key (Positions (Container), Find'Result)
1700 and Find'Result = No_Element,
1701
1702 -- Otherwise, Find returns a valid cursor in Container
1703
1704 others =>
1705 P.Has_Key (Positions (Container), Find'Result)
1706 and P.Get (Positions (Container), Find'Result) =
1707 Find (Elements (Container), Key)
1708
1709 -- The element designated by the result of Find is Key
1710
1711 and Equivalent_Keys
1712 (Generic_Keys.Key (Element (Container, Find'Result)), Key));
1713
1714 function Floor (Container : Set; Key : Key_Type) return Cursor with
1715 Global => null,
1716 Contract_Cases =>
1717 (Length (Container) = 0
1718 or else Key < Generic_Keys.Key (First_Element (Container)) =>
1719 Floor'Result = No_Element,
1720 others =>
1721 Has_Element (Container, Floor'Result)
1722 and
1723 not (Key <
1724 Generic_Keys.Key
1725 (E.Get (Elements (Container),
1726 P.Get (Positions (Container), Floor'Result))))
1727 and E_Is_Find
1728 (Elements (Container),
1729 Key,
1730 P.Get (Positions (Container), Floor'Result)));
1731
1732 function Ceiling (Container : Set; Key : Key_Type) return Cursor with
1733 Global => null,
1734 Contract_Cases =>
1735 (Length (Container) = 0
1736 or else Generic_Keys.Key (Last_Element (Container)) < Key =>
1737 Ceiling'Result = No_Element,
1738 others =>
1739 Has_Element (Container, Ceiling'Result)
1740 and
1741 not (Generic_Keys.Key
1742 (E.Get (Elements (Container),
1743 P.Get (Positions (Container), Ceiling'Result)))
1744 < Key)
1745 and E_Is_Find
1746 (Elements (Container),
1747 Key,
1748 P.Get (Positions (Container), Ceiling'Result)));
1749
1750 function Contains (Container : Set; Key : Key_Type) return Boolean with
1751 Global => null,
1752 Post =>
1753 Contains'Result =
1754 (for some E of Model (Container) =>
1755 Equivalent_Keys (Key, Generic_Keys.Key (E)));
1756
1757 end Generic_Keys;
1758
1759 private
1760 pragma SPARK_Mode (Off);
1761
1762 pragma Inline (Next);
1763 pragma Inline (Previous);
1764
1765 type Node_Type is record
1766 Has_Element : Boolean := False;
1767 Parent : Count_Type := 0;
1768 Left : Count_Type := 0;
1769 Right : Count_Type := 0;
1770 Color : Red_Black_Trees.Color_Type;
1771 Element : Element_Type;
1772 end record;
1773
1774 package Tree_Types is
1775 new Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type);
1776
1777 type Set (Capacity : Count_Type) is
1778 new Tree_Types.Tree_Type (Capacity) with null record;
1779
1780 use Red_Black_Trees;
1781
1782 Empty_Set : constant Set := (Capacity => 0, others => <>);
1783
1784 end Ada.Containers.Formal_Ordered_Sets;