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-2019, 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
49with Ada.Containers.Functional_Maps;
50with Ada.Containers.Functional_Sets;
51with Ada.Containers.Functional_Vectors;
52private with Ada.Containers.Red_Black_Trees;
53
54generic
55   type Element_Type is private;
56
57   with function "<" (Left, Right : Element_Type) return Boolean is <>;
58
59package Ada.Containers.Formal_Ordered_Sets with
60  SPARK_Mode
61is
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
1759private
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
1784end Ada.Containers.Formal_Ordered_Sets;
1785