1 ------------------------------------------------------------------------------
3 -- GNAT LIBRARY COMPONENTS --
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 --
9 -- Copyright (C) 2004-2018, Free Software Foundation, Inc. --
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. --
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. --
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. --
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 ------------------------------------------------------------------------------
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.
38 -- The modifications are:
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
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
;
55 type Element_Type
is private;
57 with function "<" (Left
, Right
: Element_Type
) return Boolean is <>;
59 package Ada
.Containers
.Formal_Ordered_Sets
with
62 pragma Annotate
(CodePeer
, Skip_Analysis
);
64 function Equivalent_Elements
(Left
, Right
: Element_Type
) return Boolean
68 Equivalent_Elements
'Result =
69 (not (Left
< Right
) and not (Right
< Left
));
70 pragma Annotate
(GNATprove
, Inline_For_Proof
, Equivalent_Elements
);
72 type Set
(Capacity
: Count_Type
) is private with
73 Iterable
=> (First
=> First
,
75 Has_Element
=> Has_Element
,
77 Default_Initial_Condition
=> Is_Empty
(Set
);
78 pragma Preelaborable_Initialization
(Set
);
84 No_Element
: constant Cursor
:= (Node
=> 0);
86 function Length
(Container
: Set
) return Count_Type
with
88 Post
=> Length
'Result <= Container
.Capacity
;
90 pragma Unevaluated_Use_Of_Old
(Allow
);
92 package Formal_Model
with Ghost
is
93 subtype Positive_Count_Type
is Count_Type
range 1 .. Count_Type
'Last;
95 package M
is new Ada
.Containers
.Functional_Sets
96 (Element_Type
=> Element_Type
,
97 Equivalent_Elements
=> Equivalent_Elements
);
101 Right
: M
.Set
) return Boolean renames M
."=";
105 Right
: M
.Set
) return Boolean renames M
."<=";
107 package E
is new Ada
.Containers
.Functional_Vectors
108 (Element_Type
=> Element_Type
,
109 Index_Type
=> Positive_Count_Type
);
113 Right
: E
.Sequence
) return Boolean renames E
."=";
117 Right
: E
.Sequence
) return Boolean renames E
."<";
121 Right
: E
.Sequence
) return Boolean renames E
."<=";
123 function E_Bigger_Than_Range
124 (Container
: E
.Sequence
;
125 Fst
: Positive_Count_Type
;
127 Item
: Element_Type
) return Boolean
130 Pre
=> Lst
<= E
.Length
(Container
),
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
);
136 function E_Smaller_Than_Range
137 (Container
: E
.Sequence
;
138 Fst
: Positive_Count_Type
;
140 Item
: Element_Type
) return Boolean
143 Pre
=> Lst
<= E
.Length
(Container
),
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
);
150 (Container
: E
.Sequence
;
152 Position
: Count_Type
) return Boolean
155 Pre
=> Position
- 1 <= E
.Length
(Container
),
159 ((if Position
> 0 then
160 E_Bigger_Than_Range
(Container
, 1, Position
- 1, Item
))
162 and (if Position
< E
.Length
(Container
) then
166 E
.Length
(Container
),
168 pragma Annotate
(GNATprove
, Inline_For_Proof
, E_Is_Find
);
171 (Container
: E
.Sequence
;
172 Item
: Element_Type
) return Count_Type
173 -- Search for Item in Container
178 (if Find
'Result > 0 then
179 Find
'Result <= E
.Length
(Container
)
180 and Equivalent_Elements
(Item
, E
.Get
(Container
, Find
'Result)));
182 function E_Elements_Included
184 Right
: E
.Sequence
) return Boolean
185 -- The elements of Left are contained in Right
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
))) =
195 pragma Annotate
(GNATprove
, Inline_For_Proof
, E_Elements_Included
);
197 function E_Elements_Included
200 Right
: E
.Sequence
) return Boolean
201 -- The elements of Container contained in Model are in Right
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
))) =
212 pragma Annotate
(GNATprove
, Inline_For_Proof
, E_Elements_Included
);
214 function E_Elements_Included
215 (Container
: E
.Sequence
;
218 Right
: E
.Sequence
) return Boolean
219 -- The elements of Container contained in Model are in Left and others
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
))) =
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
);
237 package P
is new Ada
.Containers
.Functional_Maps
239 Element_Type
=> Positive_Count_Type
,
240 Equivalent_Keys
=> "=",
241 Enable_Handling_Of_Equivalence
=> False);
245 Right
: P
.Map
) return Boolean renames P
."=";
249 Right
: P
.Map
) return Boolean renames P
."<=";
251 function P_Positions_Shifted
254 Cut
: Positive_Count_Type
;
255 Count
: Count_Type
:= 1) return Boolean
259 P_Positions_Shifted
'Result =
261 -- Big contains all cursors of Small
263 (P
.Keys_Included
(Small
, Big
)
265 -- Cursors located before Cut are not moved, cursors located
266 -- after are shifted by Count.
268 and (for all I
of Small
=>
269 (if P
.Get
(Small
, I
) < Cut
then
270 P
.Get
(Big
, I
) = P
.Get
(Small
, I
)
272 P
.Get
(Big
, I
) - Count
= P
.Get
(Small
, I
)))
274 -- New cursors of Big (if any) are between Cut and Cut - 1 +
277 and (for all I
of Big
=>
279 or P
.Get
(Big
, I
) - Count
in Cut
- Count
.. Cut
- 1));
281 function Mapping_Preserved
282 (E_Left
: E
.Sequence
;
283 E_Right
: E
.Sequence
;
285 P_Right
: P
.Map
) return Boolean
290 (if Mapping_Preserved
'Result then
292 -- Right contains all the cursors of Left
294 P
.Keys_Included
(P_Left
, P_Right
)
296 -- Right contains all the elements of Left
298 and E_Elements_Included
(E_Left
, E_Right
)
300 -- Mappings from cursors to elements induced by E_Left, P_Left
301 -- and E_Right, P_Right are the same.
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
))));
307 function Mapping_Preserved_Except
308 (E_Left
: E
.Sequence
;
309 E_Right
: E
.Sequence
;
312 Position
: Cursor
) return Boolean
317 (if Mapping_Preserved_Except
'Result then
319 -- Right contains all the cursors of Left
321 P
.Keys_Included
(P_Left
, P_Right
)
323 -- Mappings from cursors to elements induced by E_Left, P_Left
324 -- and E_Right, P_Right are the same except for Position.
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
)))));
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.
338 Post
=> M
.Length
(Model
'Result) = Length
(Container
);
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.
348 E
.Length
(Elements
'Result) = Length
(Container
)
350 -- It only contains keys contained in Model
352 and (for all Item
of Elements
'Result =>
353 M
.Contains
(Model
(Container
), Item
))
355 -- It contains all the elements contained in Model
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
)),
363 -- It is sorted in increasing order
365 and (for all I
in 1 .. Length
(Container
) =>
366 Find
(Elements
'Result, E
.Get
(Elements
'Result, I
)) = I
369 (Elements
'Result, E
.Get
(Elements
'Result, I
), I
));
370 pragma Annotate
(GNATprove
, Iterable_For_Proof
, "Model", Elements
);
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.
379 not P
.Has_Key
(Positions
'Result, No_Element
)
381 -- Positions of cursors are smaller than the container's length
384 (for all I
of Positions
'Result =>
385 P
.Get
(Positions
'Result, I
) in 1 .. Length
(Container
)
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.
392 (for all J
of Positions
'Result =>
393 (if P
.Get
(Positions
'Result, I
) = P
.Get
(Positions
'Result, J
)
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.
407 (for all Item
of Elements
(Container
) =>
408 (for some I
of Positions
(Container
) =>
409 E
.Get
(Elements
(Container
), P
.Get
(Positions
(Container
), I
)) =
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.
421 Empty_Set
: constant Set
;
423 function "=" (Left
, Right
: Set
) return Boolean with
427 -- If two sets are equal, they contain the same elements in the same
430 (if "="'Result then Elements (Left) = Elements (Right)
432 -- If they are different, then they do not contain the same elements
435 not E_Elements_Included (Elements (Left), Elements (Right))
436 or not E_Elements_Included (Elements (Right), Elements (Left)));
438 function Equivalent_Sets (Left, Right : Set) return Boolean with
440 Post => Equivalent_Sets'Result = (Model (Left) = Model (Right));
442 function To_Set (New_Item : Element_Type) return Set with
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;
449 function Is_Empty (Container : Set) return Boolean with
451 Post => Is_Empty'Result = (Length (Container) = 0);
453 procedure Clear (Container : in out Set) with
455 Post => Length (Container) = 0 and M.Is_Empty (Model (Container));
457 procedure Assign (Target : in out Set; Source : Set) with
459 Pre => Target.Capacity >= Length (Source),
461 Model (Target) = Model (Source)
462 and Elements (Target) = Elements (Source)
463 and Length (Target) = Length (Source);
465 function Copy (Source : Set; Capacity : Count_Type := 0) return Set with
467 Pre => Capacity = 0 or else Capacity >= Source.Capacity,
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
475 Copy'Result.Capacity = Capacity);
479 Position : Cursor) return Element_Type
482 Pre => Has_Element (Container, Position),
485 E.Get (Elements (Container), P.Get (Positions (Container), Position));
486 pragma Annotate (GNATprove, Inline_For_Proof, Element);
488 procedure Replace_Element
489 (Container : in out Set;
491 New_Item : Element_Type)
494 Pre => Has_Element (Container, Position),
496 Length (Container) = Length (Container)'Old
498 -- Position now maps to New_Item
500 and Element (Container, Position) = New_Item
502 -- New_Item is contained in Container
504 and Contains (Model (Container), New_Item)
506 -- Other elements are preserved
508 and M.Included_Except
509 (Model (Container)'Old,
511 Element (Container, Position)'Old)
512 and M.Included_Except
514 Model (Container)'Old,
517 -- Mapping from cursors to elements is preserved
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;
527 procedure Move (Target : in out Set; Source : in out Set) with
529 Pre => Target.Capacity >= Length (Source),
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;
537 (Container : in out Set;
538 New_Item : Element_Type;
539 Position : out Cursor;
540 Inserted : out Boolean)
544 Length (Container) < Container.Capacity
545 or Contains (Container, New_Item),
547 Contains (Container, New_Item)
548 and Has_Element (Container, Position)
549 and Equivalent_Elements (Element (Container, Position), New_Item)
551 (Elements (Container),
553 P.Get (Positions (Container), Position)),
556 -- If New_Item is already in Container, it is not modified and Inserted
559 (Contains (Container, New_Item) =>
561 and Model (Container) = Model (Container)'Old
562 and Elements (Container) = Elements (Container)'Old
563 and Positions (Container) = Positions (Container)'Old,
565 -- Otherwise, New_Item is inserted in Container and Inserted is set to
570 and Length (Container) = Length (Container)'Old + 1
572 -- Position now maps to New_Item
574 and Element (Container, Position) = New_Item
576 -- Other elements are preserved
578 and Model (Container)'Old <= Model (Container)
579 and M.Included_Except
581 Model (Container)'Old,
584 -- The elements of Container located before Position are preserved
587 (Left => Elements (Container)'Old,
588 Right => Elements (Container),
590 Lst => P.Get (Positions (Container), Position) - 1)
592 -- Other elements are shifted by 1
595 (Left => Elements (Container)'Old,
596 Right => Elements (Container),
597 Fst => P.Get (Positions (Container), Position),
598 Lst => Length (Container)'Old,
601 -- A new cursor has been inserted at position Position in
604 and P_Positions_Shifted
605 (Positions (Container)'Old,
606 Positions (Container),
607 Cut => P.Get (Positions (Container), Position)));
610 (Container : in out Set;
611 New_Item : Element_Type)
615 Length (Container) < Container.Capacity
616 and then (not Contains (Container, New_Item)),
618 Length (Container) = Length (Container)'Old + 1
619 and Contains (Container, New_Item)
621 -- New_Item is inserted in the set
623 and E.Get (Elements (Container),
624 Find (Elements (Container), New_Item)) = New_Item
626 -- Other mappings are preserved
628 and Model (Container)'Old <= Model (Container)
629 and M.Included_Except
631 Model (Container)'Old,
634 -- The elements of Container located before New_Item are preserved
637 (Left => Elements (Container)'Old,
638 Right => Elements (Container),
640 Lst => Find (Elements (Container), New_Item) - 1)
642 -- Other elements are shifted by 1
645 (Left => Elements (Container)'Old,
646 Right => Elements (Container),
647 Fst => Find (Elements (Container), New_Item),
648 Lst => Length (Container)'Old,
651 -- A new cursor has been inserted in Container
653 and P_Positions_Shifted
654 (Positions (Container)'Old,
655 Positions (Container),
656 Cut => Find (Elements (Container), New_Item));
659 (Container : in out Set;
660 New_Item : Element_Type)
664 Length (Container) < Container.Capacity
665 or Contains (Container, New_Item),
666 Post => Contains (Container, New_Item),
669 -- If New_Item is already in Container
671 (Contains (Container, New_Item) =>
673 -- Elements are preserved
675 Model (Container)'Old = Model (Container)
677 -- Cursors are preserved
679 and Positions (Container) = Positions (Container)'Old
681 -- The element equivalent to New_Item in Container is replaced by
684 and E.Get (Elements (Container),
685 Find (Elements (Container), New_Item)) = New_Item
688 (Elements (Container)'Old,
689 Elements (Container),
690 Find (Elements (Container), New_Item)),
692 -- Otherwise, New_Item is inserted in Container
695 Length (Container) = Length (Container)'Old + 1
697 -- Other elements are preserved
699 and Model (Container)'Old <= Model (Container)
700 and M.Included_Except
702 Model (Container)'Old,
705 -- New_Item is inserted in Container
707 and E.Get (Elements (Container),
708 Find (Elements (Container), New_Item)) = New_Item
710 -- The Elements of Container located before New_Item are preserved
713 (Left => Elements (Container)'Old,
714 Right => Elements (Container),
716 Lst => Find (Elements (Container), New_Item) - 1)
718 -- Other Elements are shifted by 1
721 (Left => Elements (Container)'Old,
722 Right => Elements (Container),
723 Fst => Find (Elements (Container), New_Item),
724 Lst => Length (Container)'Old,
727 -- A new cursor has been inserted in Container
729 and P_Positions_Shifted
730 (Positions (Container)'Old,
731 Positions (Container),
732 Cut => Find (Elements (Container), New_Item)));
735 (Container : in out Set;
736 New_Item : Element_Type)
739 Pre => Contains (Container, New_Item),
742 -- Elements are preserved
744 Model (Container)'Old = Model (Container)
746 -- Cursors are preserved
748 and Positions (Container) = Positions (Container)'Old
750 -- The element equivalent to New_Item in Container is replaced by
753 and E.Get (Elements (Container),
754 Find (Elements (Container), New_Item)) = New_Item
756 (Elements (Container)'Old,
757 Elements (Container),
758 Find (Elements (Container), New_Item));
761 (Container : in out Set;
765 Post => not Contains (Container, Item),
768 -- If Item is not in Container, nothing is changed
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,
775 -- Otherwise, Item is removed from Container
778 Length (Container) = Length (Container)'Old - 1
780 -- Other elements are preserved
782 and Model (Container) <= Model (Container)'Old
783 and M.Included_Except
784 (Model (Container)'Old,
788 -- The elements of Container located before Item are preserved
791 (Left => Elements (Container)'Old,
792 Right => Elements (Container),
794 Lst => Find (Elements (Container), Item)'Old - 1)
796 -- The elements located after Item are shifted by 1
799 (Left => Elements (Container),
800 Right => Elements (Container)'Old,
801 Fst => Find (Elements (Container), Item)'Old,
802 Lst => Length (Container),
805 -- A cursor has been removed from Container
807 and P_Positions_Shifted
808 (Positions (Container),
809 Positions (Container)'Old,
810 Cut => Find (Elements (Container), Item)'Old));
813 (Container : in out Set;
817 Pre => Contains (Container, Item),
819 Length (Container) = Length (Container)'Old - 1
821 -- Item is no longer in Container
823 and not Contains (Container, Item)
825 -- Other elements are preserved
827 and Model (Container) <= Model (Container)'Old
828 and M.Included_Except
829 (Model (Container)'Old,
833 -- The elements of Container located before Item are preserved
836 (Left => Elements (Container)'Old,
837 Right => Elements (Container),
839 Lst => Find (Elements (Container), Item)'Old - 1)
841 -- The elements located after Item are shifted by 1
844 (Left => Elements (Container),
845 Right => Elements (Container)'Old,
846 Fst => Find (Elements (Container), Item)'Old,
847 Lst => Length (Container),
850 -- A cursor has been removed from Container
852 and P_Positions_Shifted
853 (Positions (Container),
854 Positions (Container)'Old,
855 Cut => Find (Elements (Container), Item)'Old);
858 (Container : in out Set;
859 Position : in out Cursor)
862 Pre => Has_Element (Container, Position),
864 Position = No_Element
865 and Length (Container) = Length (Container)'Old - 1
867 -- The element at position Position is no longer in Container
869 and not Contains (Container, Element (Container, Position)'Old)
870 and not P.Has_Key (Positions (Container), Position'Old)
872 -- Other elements are preserved
874 and Model (Container) <= Model (Container)'Old
875 and M.Included_Except
876 (Model (Container)'Old,
878 Element (Container, Position)'Old)
880 -- The elements of Container located before Position are preserved.
883 (Left => Elements (Container)'Old,
884 Right => Elements (Container),
886 Lst => P.Get (Positions (Container)'Old, Position'Old) - 1)
888 -- The elements located after Position are shifted by 1
891 (Left => Elements (Container),
892 Right => Elements (Container)'Old,
893 Fst => P.Get (Positions (Container)'Old, Position'Old),
894 Lst => Length (Container),
897 -- Position has been removed from Container
899 and P_Positions_Shifted
900 (Positions (Container),
901 Positions (Container)'Old,
902 Cut => P.Get (Positions (Container)'Old, Position'Old));
904 procedure Delete_First (Container : in out Set) with
907 (Length (Container) = 0 => Length (Container) = 0,
909 Length (Container) = Length (Container)'Old - 1
911 -- The first element has been removed from Container
913 and not Contains (Container, First_Element (Container)'Old)
915 -- Other elements are preserved
917 and Model (Container) <= Model (Container)'Old
918 and M.Included_Except
919 (Model (Container)'Old,
921 First_Element (Container)'Old)
923 -- Other elements are shifted by 1
926 (Left => Elements (Container),
927 Right => Elements (Container)'Old,
929 Lst => Length (Container),
932 -- First has been removed from Container
934 and P_Positions_Shifted
935 (Positions (Container),
936 Positions (Container)'Old,
939 procedure Delete_Last (Container : in out Set) with
942 (Length (Container) = 0 => Length (Container) = 0,
944 Length (Container) = Length (Container)'Old - 1
946 -- The last element has been removed from Container
948 and not Contains (Container, Last_Element (Container)'Old)
950 -- Other elements are preserved
952 and Model (Container) <= Model (Container)'Old
953 and M.Included_Except
954 (Model (Container)'Old,
956 Last_Element (Container)'Old)
958 -- Others elements of Container are preserved
961 (Left => Elements (Container)'Old,
962 Right => Elements (Container),
964 Lst => Length (Container))
966 -- Last cursor has been removed from Container
968 and Positions (Container) <= Positions (Container)'Old);
970 procedure Union (Target : in out Set; Source : Set) with
973 Length (Source) - Length (Target and Source) <=
974 Target.Capacity - Length (Target),
976 Length (Target) = Length (Target)'Old
977 - M.Num_Overlaps (Model (Target)'Old, Model (Source))
980 -- Elements already in Target are still in Target
982 and Model (Target)'Old <= Model (Target)
984 -- Elements of Source are included in Target
986 and Model (Source) <= Model (Target)
988 -- Elements of Target come from either Source or Target
992 (Model (Target), Model (Source), Model (Target)'Old)
994 -- Actual value of elements come from either Left or Right
1000 Elements (Target)'Old,
1004 (Elements (Target)'Old, Model (Target)'Old, Elements (Target))
1012 -- Mapping from cursors of Target to elements is preserved
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));
1020 function Union (Left, Right : Set) return Set with
1022 Pre => Length (Left) <= Count_Type'Last - Length (Right),
1024 Length (Union'Result) = Length (Left)
1025 - M.Num_Overlaps (Model (Left), Model (Right))
1028 -- Elements of Left and Right are in the result of Union
1030 and Model (Left) <= Model (Union'Result)
1031 and Model (Right) <= Model (Union'Result)
1033 -- Elements of the result of union come from either Left or Right
1037 (Model (Union'Result), Model (Left), Model (Right))
1039 -- Actual value of elements come from either Left or Right
1043 (Elements (Union'Result),
1049 (Elements (Left), Model (Left), Elements (Union'Result))
1055 Elements (Union'Result));
1057 function "or" (Left, Right : Set) return Set renames Union;
1059 procedure Intersection (Target : in out Set; Source : Set) with
1063 M.Num_Overlaps (Model (Target)'Old, Model (Source))
1065 -- Elements of Target were already in Target
1067 and Model (Target) <= Model (Target)'Old
1069 -- Elements of Target are in Source
1071 and Model (Target) <= Model (Source)
1073 -- Elements both in Source and Target are in the intersection
1076 M.Includes_Intersection
1077 (Model (Target), Model (Source), Model (Target)'Old)
1079 -- Actual value of elements of Target is preserved
1081 and E_Elements_Included (Elements (Target), Elements (Target)'Old)
1084 (Elements (Target)'Old, Model (Source), Elements (Target))
1086 -- Mapping from cursors of Target to elements is preserved
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);
1094 function Intersection (Left, Right : Set) return Set with
1097 Length (Intersection'Result) =
1098 M.Num_Overlaps (Model (Left), Model (Right))
1100 -- Elements in the result of Intersection are in Left and Right
1102 and Model (Intersection'Result) <= Model (Left)
1103 and Model (Intersection'Result) <= Model (Right)
1105 -- Elements both in Left and Right are in the result of Intersection
1108 M.Includes_Intersection
1109 (Model (Intersection'Result), Model (Left), Model (Right))
1111 -- Actual value of elements come from Left
1115 (Elements (Intersection'Result), Elements (Left))
1118 (Elements (Left), Model (Right), Elements (Intersection'Result));
1120 function "and" (Left, Right : Set) return Set renames Intersection;
1122 procedure Difference (Target : in out Set; Source : Set) with
1125 Length (Target) = Length (Target)'Old -
1126 M.Num_Overlaps (Model (Target)'Old, Model (Source))
1128 -- Elements of Target were already in Target
1130 and Model (Target) <= Model (Target)'Old
1132 -- Elements of Target are not in Source
1134 and M.No_Overlap (Model (Target), Model (Source))
1136 -- Elements in Target but not in Source are in the difference
1140 (Model (Target)'Old, Model (Target), Model (Source))
1142 -- Actual value of elements of Target is preserved
1144 and E_Elements_Included (Elements (Target), Elements (Target)'Old)
1147 (Elements (Target)'Old, Model (Target), Elements (Target))
1149 -- Mapping from cursors of Target to elements is preserved
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);
1157 function Difference (Left, Right : Set) return Set with
1160 Length (Difference'Result) = Length (Left) -
1161 M.Num_Overlaps (Model (Left), Model (Right))
1163 -- Elements of the result of Difference are in Left
1165 and Model (Difference'Result) <= Model (Left)
1167 -- Elements of the result of Difference are in Right
1169 and M.No_Overlap (Model (Difference'Result), Model (Right))
1171 -- Elements in Left but not in Right are in the difference
1175 (Model (Left), Model (Difference'Result), Model (Right))
1177 -- Actual value of elements come from Left
1180 E_Elements_Included (Elements (Difference'Result), Elements (Left))
1184 Model (Difference'Result),
1185 Elements (Difference'Result));
1187 function "-" (Left, Right : Set) return Set renames Difference;
1189 procedure Symmetric_Difference (Target : in out Set; Source : Set) with
1192 Length (Source) - Length (Target and Source) <=
1193 Target.Capacity - Length (Target) + Length (Target and Source),
1195 Length (Target) = Length (Target)'Old -
1196 2 * M.Num_Overlaps (Model (Target)'Old, Model (Source)) +
1199 -- Elements of the difference were not both in Source and in Target
1201 and M.Not_In_Both (Model (Target), Model (Target)'Old, Model (Source))
1203 -- Elements in Target but not in Source are in the difference
1207 (Model (Target)'Old, Model (Target), Model (Source))
1209 -- Elements in Source but not in Target are in the difference
1213 (Model (Source), Model (Target), Model (Target)'Old)
1215 -- Actual value of elements come from either Left or Right
1221 Elements (Target)'Old,
1225 (Elements (Target)'Old, Model (Target), Elements (Target))
1228 (Elements (Source), Model (Target), Elements (Target));
1230 function Symmetric_Difference (Left, Right : Set) return Set with
1232 Pre => Length (Left) <= Count_Type'Last - Length (Right),
1234 Length (Symmetric_Difference'Result) = Length (Left) -
1235 2 * M.Num_Overlaps (Model (Left), Model (Right)) +
1238 -- Elements of the difference were not both in Left and Right
1242 (Model (Symmetric_Difference'Result), Model (Left), Model (Right))
1244 -- Elements in Left but not in Right are in the difference
1248 (Model (Left), Model (Symmetric_Difference'Result), Model (Right))
1250 -- Elements in Right but not in Left are in the difference
1254 (Model (Right), Model (Symmetric_Difference'Result), Model (Left))
1256 -- Actual value of elements come from either Left or Right
1260 (Elements (Symmetric_Difference'Result),
1267 Model (Symmetric_Difference'Result),
1268 Elements (Symmetric_Difference'Result))
1272 Model (Symmetric_Difference'Result),
1273 Elements (Symmetric_Difference'Result));
1275 function "xor" (Left, Right : Set) return Set
1276 renames Symmetric_Difference;
1278 function Overlap (Left, Right : Set) return Boolean with
1281 Overlap'Result = not (M.No_Overlap (Model (Left), Model (Right)));
1283 function Is_Subset (Subset : Set; Of_Set : Set) return Boolean with
1285 Post => Is_Subset'Result = (Model (Subset) <= Model (Of_Set));
1287 function First (Container : Set) return Cursor with
1290 (Length (Container) = 0 =>
1291 First'Result = No_Element,
1294 Has_Element (Container, First'Result)
1295 and P.Get (Positions (Container), First'Result) = 1);
1297 function First_Element (Container : Set) return Element_Type with
1299 Pre => not Is_Empty (Container),
1301 First_Element'Result = E.Get (Elements (Container), 1)
1302 and E_Smaller_Than_Range
1303 (Elements (Container),
1306 First_Element'Result);
1308 function Last (Container : Set) return Cursor with
1311 (Length (Container) = 0 =>
1312 Last'Result = No_Element,
1315 Has_Element (Container, Last'Result)
1316 and P.Get (Positions (Container), Last'Result) =
1317 Length (Container));
1319 function Last_Element (Container : Set) return Element_Type with
1321 Pre => not Is_Empty (Container),
1323 Last_Element'Result = E.Get (Elements (Container), Length (Container))
1324 and E_Bigger_Than_Range
1325 (Elements (Container),
1327 Length (Container) - 1,
1328 Last_Element'Result);
1330 function Next (Container : Set; Position : Cursor) return Cursor with
1333 Has_Element (Container, Position) or else Position = No_Element,
1335 (Position = No_Element
1336 or else P.Get (Positions (Container), Position) = Length (Container)
1338 Next'Result = No_Element,
1341 Has_Element (Container, Next'Result)
1342 and then P.Get (Positions (Container), Next'Result) =
1343 P.Get (Positions (Container), Position) + 1);
1345 procedure Next (Container : Set; Position : in out Cursor) with
1348 Has_Element (Container, Position) or else Position = No_Element,
1350 (Position = No_Element
1351 or else P.Get (Positions (Container), Position) = Length (Container)
1353 Position = No_Element,
1356 Has_Element (Container, Position)
1357 and then P.Get (Positions (Container), Position) =
1358 P.Get (Positions (Container), Position'Old) + 1);
1360 function Previous (Container : Set; Position : Cursor) return Cursor with
1363 Has_Element (Container, Position) or else Position = No_Element,
1365 (Position = No_Element
1366 or else P.Get (Positions (Container), Position) = 1
1368 Previous'Result = No_Element,
1371 Has_Element (Container, Previous'Result)
1372 and then P.Get (Positions (Container), Previous'Result) =
1373 P.Get (Positions (Container), Position) - 1);
1375 procedure Previous (Container : Set; Position : in out Cursor) with
1378 Has_Element (Container, Position) or else Position = No_Element,
1380 (Position = No_Element
1381 or else P.Get (Positions (Container), Position) = 1
1383 Position = No_Element,
1386 Has_Element (Container, Position)
1387 and then P.Get (Positions (Container), Position) =
1388 P.Get (Positions (Container), Position'Old) - 1);
1390 function Find (Container : Set; Item : Element_Type) return Cursor with
1394 -- If Item is not contained in Container, Find returns No_Element
1396 (not Contains (Model (Container), Item) =>
1397 not P.Has_Key (Positions (Container), Find'Result)
1398 and Find'Result = No_Element,
1400 -- Otherwise, Find returns a valid cursor in Container
1403 P.Has_Key (Positions (Container), Find'Result)
1404 and P.Get (Positions (Container), Find'Result) =
1405 Find (Elements (Container), Item)
1407 -- The element designated by the result of Find is Item
1409 and Equivalent_Elements
1410 (Element (Container, Find'Result), Item));
1412 function Floor (Container : Set; Item : Element_Type) return Cursor with
1415 (Length (Container) = 0 or else Item < First_Element (Container) =>
1416 Floor'Result = No_Element,
1418 Has_Element (Container, Floor'Result)
1420 not (Item < E.Get (Elements (Container),
1421 P.Get (Positions (Container), Floor'Result)))
1423 (Elements (Container),
1425 P.Get (Positions (Container), Floor'Result)));
1427 function Ceiling (Container : Set; Item : Element_Type) return Cursor with
1430 (Length (Container) = 0 or else Last_Element (Container) < Item =>
1431 Ceiling'Result = No_Element,
1433 Has_Element (Container, Ceiling'Result)
1435 not (E.Get (Elements (Container),
1436 P.Get (Positions (Container), Ceiling'Result)) <
1439 (Elements (Container),
1441 P.Get (Positions (Container), Ceiling'Result)));
1443 function Contains (Container : Set; Item : Element_Type) return Boolean with
1445 Post => Contains'Result = Contains (Model (Container), Item);
1446 pragma Annotate (GNATprove, Inline_For_Proof, Contains);
1448 function Has_Element (Container : Set; Position : Cursor) return Boolean
1452 Has_Element'Result = P.Has_Key (Positions (Container), Position);
1453 pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
1456 type Key_Type (<>) is private;
1458 with function Key (Element : Element_Type) return Key_Type;
1460 with function "<" (Left, Right : Key_Type) return Boolean is <>;
1462 package Generic_Keys with SPARK_Mode is
1464 function Equivalent_Keys (Left, Right : Key_Type) return Boolean with
1467 Equivalent_Keys'Result = (not (Left < Right) and not (Right < Left));
1468 pragma Annotate (GNATprove, Inline_For_Proof, Equivalent_Keys);
1470 package Formal_Model with Ghost is
1471 function E_Bigger_Than_Range
1472 (Container : E.Sequence;
1473 Fst : Positive_Count_Type;
1475 Key : Key_Type) return Boolean
1478 Pre => Lst <= E.Length (Container),
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);
1485 function E_Smaller_Than_Range
1486 (Container : E.Sequence;
1487 Fst : Positive_Count_Type;
1489 Key : Key_Type) return Boolean
1492 Pre => Lst <= E.Length (Container),
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);
1500 (Container : E.Sequence;
1502 Position : Count_Type) return Boolean
1505 Pre => Position - 1 <= E.Length (Container),
1509 ((if Position > 0 then
1510 E_Bigger_Than_Range (Container, 1, Position - 1, Key))
1512 and (if Position < E.Length (Container) then
1513 E_Smaller_Than_Range
1516 E.Length (Container),
1518 pragma Annotate (GNATprove, Inline_For_Proof, E_Is_Find);
1521 (Container : E.Sequence;
1522 Key : Key_Type) return Count_Type
1523 -- Search for Key in Container
1528 (if Find'Result > 0 then
1529 Find'Result <= E.Length (Container)
1531 (Key, Generic_Keys.Key (E.Get (Container, Find'Result)))
1532 and E_Is_Find (Container, Key, Find'Result));
1534 function M_Included_Except
1537 Key : Key_Type) return Boolean
1541 M_Included_Except'Result =
1542 (for all E of Left =>
1544 or Equivalent_Keys (Generic_Keys.Key (E), Key));
1548 function Key (Container : Set; Position : Cursor) return Key_Type with
1550 Post => Key'Result = Key (Element (Container, Position));
1551 pragma Annotate (GNATprove, Inline_For_Proof, Key);
1553 function Element (Container : Set; Key : Key_Type) return Element_Type
1556 Pre => Contains (Container, Key),
1558 Element'Result = Element (Container, Find (Container, Key));
1559 pragma Annotate (GNATprove, Inline_For_Proof, Element);
1562 (Container : in out Set;
1564 New_Item : Element_Type)
1567 Pre => Contains (Container, Key),
1569 Length (Container) = Length (Container)'Old
1571 -- Key now maps to New_Item
1573 and Element (Container, Key) = New_Item
1575 -- New_Item is contained in Container
1577 and Contains (Model (Container), New_Item)
1579 -- Other elements are preserved
1581 and M_Included_Except
1582 (Model (Container)'Old,
1585 and M.Included_Except
1587 Model (Container)'Old,
1590 -- Mapping from cursors to elements is preserved
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;
1600 procedure Exclude (Container : in out Set; Key : Key_Type) with
1602 Post => not Contains (Container, Key),
1605 -- If Key is not in Container, nothing is changed
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,
1612 -- Otherwise, Key is removed from Container
1615 Length (Container) = Length (Container)'Old - 1
1617 -- Other elements are preserved
1619 and Model (Container) <= Model (Container)'Old
1620 and M_Included_Except
1621 (Model (Container)'Old,
1625 -- The elements of Container located before Key are preserved
1628 (Left => Elements (Container)'Old,
1629 Right => Elements (Container),
1631 Lst => Find (Elements (Container), Key)'Old - 1)
1633 -- The elements located after Key are shifted by 1
1636 (Left => Elements (Container),
1637 Right => Elements (Container)'Old,
1638 Fst => Find (Elements (Container), Key)'Old,
1639 Lst => Length (Container),
1642 -- A cursor has been removed from Container
1644 and P_Positions_Shifted
1645 (Positions (Container),
1646 Positions (Container)'Old,
1647 Cut => Find (Elements (Container), Key)'Old));
1649 procedure Delete (Container : in out Set; Key : Key_Type) with
1651 Pre => Contains (Container, Key),
1653 Length (Container) = Length (Container)'Old - 1
1655 -- Key is no longer in Container
1657 and not Contains (Container, Key)
1659 -- Other elements are preserved
1661 and Model (Container) <= Model (Container)'Old
1662 and M_Included_Except
1663 (Model (Container)'Old,
1667 -- The elements of Container located before Key are preserved
1670 (Left => Elements (Container)'Old,
1671 Right => Elements (Container),
1673 Lst => Find (Elements (Container), Key)'Old - 1)
1675 -- The elements located after Key are shifted by 1
1678 (Left => Elements (Container),
1679 Right => Elements (Container)'Old,
1680 Fst => Find (Elements (Container), Key)'Old,
1681 Lst => Length (Container),
1684 -- A cursor has been removed from Container
1686 and P_Positions_Shifted
1687 (Positions (Container),
1688 Positions (Container)'Old,
1689 Cut => Find (Elements (Container), Key)'Old);
1691 function Find (Container : Set; Key : Key_Type) return Cursor with
1695 -- If Key is not contained in Container, Find returns No_Element
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,
1702 -- Otherwise, Find returns a valid cursor in Container
1705 P.Has_Key (Positions (Container), Find'Result)
1706 and P.Get (Positions (Container), Find'Result) =
1707 Find (Elements (Container), Key)
1709 -- The element designated by the result of Find is Key
1712 (Generic_Keys.Key (Element (Container, Find'Result)), Key));
1714 function Floor (Container : Set; Key : Key_Type) return Cursor with
1717 (Length (Container) = 0
1718 or else Key < Generic_Keys.Key (First_Element (Container)) =>
1719 Floor'Result = No_Element,
1721 Has_Element (Container, Floor'Result)
1725 (E.Get (Elements (Container),
1726 P.Get (Positions (Container), Floor'Result))))
1728 (Elements (Container),
1730 P.Get (Positions (Container), Floor'Result)));
1732 function Ceiling (Container : Set; Key : Key_Type) return Cursor with
1735 (Length (Container) = 0
1736 or else Generic_Keys.Key (Last_Element (Container)) < Key =>
1737 Ceiling'Result = No_Element,
1739 Has_Element (Container, Ceiling'Result)
1741 not (Generic_Keys.Key
1742 (E.Get (Elements (Container),
1743 P.Get (Positions (Container), Ceiling'Result)))
1746 (Elements (Container),
1748 P.Get (Positions (Container), Ceiling'Result)));
1750 function Contains (Container : Set; Key : Key_Type) return Boolean with
1754 (for some E of Model (Container) =>
1755 Equivalent_Keys (Key, Generic_Keys.Key (E)));
1760 pragma SPARK_Mode (Off);
1762 pragma Inline (Next);
1763 pragma Inline (Previous);
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;
1774 package Tree_Types is
1775 new Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type);
1777 type Set (Capacity : Count_Type) is
1778 new Tree_Types.Tree_Type (Capacity) with null record;
1780 use Red_Black_Trees;
1782 Empty_Set : constant Set := (Capacity => 0, others => <>);
1784 end Ada.Containers.Formal_Ordered_Sets;