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 _ M A P 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_Maps 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 a
44 -- container C and its previous version C'Old) for expressing properties,
45 -- which is not possible if cursors encapsulate an access to the underlying
46 -- container. The operators "<" and ">" that could not be modified that way
49 -- Iteration over maps is done using the Iterable aspect, which is SPARK
50 -- compatible. "For of" iteration ranges over keys instead of elements.
52 with Ada
.Containers
.Functional_Vectors
;
53 with Ada
.Containers
.Functional_Maps
;
54 private with Ada
.Containers
.Red_Black_Trees
;
57 type Key_Type
is private;
58 type Element_Type
is private;
60 with function "<" (Left
, Right
: Key_Type
) return Boolean is <>;
62 package Ada
.Containers
.Formal_Ordered_Maps
with
65 pragma Annotate
(CodePeer
, Skip_Analysis
);
67 function Equivalent_Keys
(Left
, Right
: Key_Type
) return Boolean with
70 Equivalent_Keys
'Result = (not (Left
< Right
) and not (Right
< Left
));
71 pragma Annotate
(GNATprove
, Inline_For_Proof
, Equivalent_Keys
);
73 type Map
(Capacity
: Count_Type
) is private with
74 Iterable
=> (First
=> First
,
76 Has_Element
=> Has_Element
,
78 Default_Initial_Condition
=> Is_Empty
(Map
);
79 pragma Preelaborable_Initialization
(Map
);
85 No_Element
: constant Cursor
:= (Node
=> 0);
87 Empty_Map
: constant Map
;
89 function Length
(Container
: Map
) return Count_Type
with
91 Post
=> Length
'Result <= Container
.Capacity
;
93 pragma Unevaluated_Use_Of_Old
(Allow
);
95 package Formal_Model
with Ghost
is
96 subtype Positive_Count_Type
is Count_Type
range 1 .. Count_Type
'Last;
98 package M
is new Ada
.Containers
.Functional_Maps
99 (Element_Type
=> Element_Type
,
100 Key_Type
=> Key_Type
,
101 Equivalent_Keys
=> Equivalent_Keys
);
105 Right
: M
.Map
) return Boolean renames M
."=";
109 Right
: M
.Map
) return Boolean renames M
."<=";
111 package K
is new Ada
.Containers
.Functional_Vectors
112 (Element_Type
=> Key_Type
,
113 Index_Type
=> Positive_Count_Type
);
117 Right
: K
.Sequence
) return Boolean renames K
."=";
121 Right
: K
.Sequence
) return Boolean renames K
."<";
125 Right
: K
.Sequence
) return Boolean renames K
."<=";
127 function K_Bigger_Than_Range
128 (Container
: K
.Sequence
;
129 Fst
: Positive_Count_Type
;
131 Key
: Key_Type
) return Boolean
134 Pre
=> Lst
<= K
.Length
(Container
),
136 K_Bigger_Than_Range
'Result =
137 (for all I
in Fst
.. Lst
=> K
.Get
(Container
, I
) < Key
);
138 pragma Annotate
(GNATprove
, Inline_For_Proof
, K_Bigger_Than_Range
);
140 function K_Smaller_Than_Range
141 (Container
: K
.Sequence
;
142 Fst
: Positive_Count_Type
;
144 Key
: Key_Type
) return Boolean
147 Pre
=> Lst
<= K
.Length
(Container
),
149 K_Smaller_Than_Range
'Result =
150 (for all I
in Fst
.. Lst
=> Key
< K
.Get
(Container
, I
));
151 pragma Annotate
(GNATprove
, Inline_For_Proof
, K_Smaller_Than_Range
);
154 (Container
: K
.Sequence
;
156 Position
: Count_Type
) return Boolean
159 Pre
=> Position
- 1 <= K
.Length
(Container
),
162 ((if Position
> 0 then
163 K_Bigger_Than_Range
(Container
, 1, Position
- 1, Key
))
166 (if Position
< K
.Length
(Container
) then
170 K
.Length
(Container
),
172 pragma Annotate
(GNATprove
, Inline_For_Proof
, K_Is_Find
);
174 function Find
(Container
: K
.Sequence
; Key
: Key_Type
) return Count_Type
175 -- Search for Key in Container
180 (if Find
'Result > 0 then
181 Find
'Result <= K
.Length
(Container
)
182 and Equivalent_Keys
(Key
, K
.Get
(Container
, Find
'Result)));
184 package P
is new Ada
.Containers
.Functional_Maps
186 Element_Type
=> Positive_Count_Type
,
187 Equivalent_Keys
=> "=",
188 Enable_Handling_Of_Equivalence
=> False);
192 Right
: P
.Map
) return Boolean renames P
."=";
196 Right
: P
.Map
) return Boolean renames P
."<=";
198 function P_Positions_Shifted
201 Cut
: Positive_Count_Type
;
202 Count
: Count_Type
:= 1) return Boolean
206 P_Positions_Shifted
'Result =
208 -- Big contains all cursors of Small
210 (P
.Keys_Included
(Small
, Big
)
212 -- Cursors located before Cut are not moved, cursors located
213 -- after are shifted by Count.
215 and (for all I
of Small
=>
216 (if P
.Get
(Small
, I
) < Cut
then
217 P
.Get
(Big
, I
) = P
.Get
(Small
, I
)
219 P
.Get
(Big
, I
) - Count
= P
.Get
(Small
, I
)))
221 -- New cursors of Big (if any) are between Cut and Cut - 1 +
224 and (for all I
of Big
=>
226 or P
.Get
(Big
, I
) - Count
in Cut
- Count
.. Cut
- 1));
228 function Model
(Container
: Map
) return M
.Map
with
229 -- The high-level model of a map is a map from keys to elements. Neither
230 -- cursors nor order of elements are represented in this model. Keys are
231 -- modeled up to equivalence.
236 function Keys
(Container
: Map
) return K
.Sequence
with
237 -- The Keys sequence represents the underlying list structure of maps
238 -- that is used for iteration. It stores the actual values of keys in
239 -- the map. It does not model cursors nor elements.
244 K
.Length
(Keys
'Result) = Length
(Container
)
246 -- It only contains keys contained in Model
248 and (for all Key
of Keys
'Result =>
249 M
.Has_Key
(Model
(Container
), Key
))
251 -- It contains all the keys contained in Model
253 and (for all Key
of Model
(Container
) =>
254 (Find
(Keys
'Result, Key
) > 0
255 and then Equivalent_Keys
256 (K
.Get
(Keys
'Result, Find
(Keys
'Result, Key
)),
259 -- It is sorted in increasing order
261 and (for all I
in 1 .. Length
(Container
) =>
262 Find
(Keys
'Result, K
.Get
(Keys
'Result, I
)) = I
263 and K_Is_Find
(Keys
'Result, K
.Get
(Keys
'Result, I
), I
));
264 pragma Annotate
(GNATprove
, Iterable_For_Proof
, "Model", Keys
);
266 function Positions
(Container
: Map
) return P
.Map
with
267 -- The Positions map is used to model cursors. It only contains valid
268 -- cursors and maps them to their position in the container.
273 not P
.Has_Key
(Positions
'Result, No_Element
)
275 -- Positions of cursors are smaller than the container's length.
278 (for all I
of Positions
'Result =>
279 P
.Get
(Positions
'Result, I
) in 1 .. Length
(Container
)
281 -- No two cursors have the same position. Note that we do not
282 -- state that there is a cursor in the map for each position, as
283 -- it is rarely needed.
286 (for all J
of Positions
'Result =>
287 (if P
.Get
(Positions
'Result, I
) = P
.Get
(Positions
'Result, J
)
290 procedure Lift_Abstraction_Level
(Container
: Map
) with
291 -- Lift_Abstraction_Level is a ghost procedure that does nothing but
292 -- assume that we can access the same elements by iterating over
293 -- positions or cursors.
294 -- This information is not generally useful except when switching from
295 -- a low-level, cursor-aware view of a container, to a high-level,
296 -- position-based view.
301 (for all Key
of Keys
(Container
) =>
302 (for some I
of Positions
(Container
) =>
303 K
.Get
(Keys
(Container
), P
.Get
(Positions
(Container
), I
)) =
308 K
: Key_Type
) return Boolean renames M
.Has_Key
;
309 -- To improve readability of contracts, we rename the function used to
310 -- search for a key in the model to Contains.
314 K
: Key_Type
) return Element_Type
renames M
.Get
;
315 -- To improve readability of contracts, we rename the function used to
316 -- access an element in the model to Element.
320 function "=" (Left
, Right
: Map
) return Boolean with
322 Post
=> "="'Result = (Model (Left) = Model (Right));
324 function Is_Empty (Container : Map) return Boolean with
326 Post => Is_Empty'Result = (Length (Container) = 0);
328 procedure Clear (Container : in out Map) with
330 Post => Length (Container) = 0 and M.Is_Empty (Model (Container));
332 procedure Assign (Target : in out Map; Source : Map) with
334 Pre => Target.Capacity >= Length (Source),
336 Model (Target) = Model (Source)
337 and Keys (Target) = Keys (Source)
338 and Length (Source) = Length (Target);
340 function Copy (Source : Map; Capacity : Count_Type := 0) return Map with
342 Pre => Capacity = 0 or else Capacity >= Source.Capacity,
344 Model (Copy'Result) = Model (Source)
345 and Keys (Copy'Result) = Keys (Source)
346 and Positions (Copy'Result) = Positions (Source)
347 and (if Capacity = 0 then
348 Copy'Result.Capacity = Source.Capacity
350 Copy'Result.Capacity = Capacity);
352 function Key (Container : Map; Position : Cursor) return Key_Type with
354 Pre => Has_Element (Container, Position),
357 K.Get (Keys (Container), P.Get (Positions (Container), Position));
358 pragma Annotate (GNATprove, Inline_For_Proof, Key);
362 Position : Cursor) return Element_Type
365 Pre => Has_Element (Container, Position),
367 Element'Result = Element (Model (Container), Key (Container, Position));
368 pragma Annotate (GNATprove, Inline_For_Proof, Element);
370 procedure Replace_Element
371 (Container : in out Map;
373 New_Item : Element_Type)
376 Pre => Has_Element (Container, Position),
379 -- Order of keys and cursors is preserved
381 Keys (Container) = Keys (Container)'Old
382 and Positions (Container) = Positions (Container)'Old
384 -- New_Item is now associated with the key at position Position in
387 and Element (Container, Position) = New_Item
389 -- Elements associated with other keys are preserved
391 and M.Same_Keys (Model (Container), Model (Container)'Old)
392 and M.Elements_Equal_Except
394 Model (Container)'Old,
395 Key (Container, Position));
397 procedure Move (Target : in out Map; Source : in out Map) with
399 Pre => Target.Capacity >= Length (Source),
401 Model (Target) = Model (Source)'Old
402 and Keys (Target) = Keys (Source)'Old
403 and Length (Source)'Old = Length (Target)
404 and Length (Source) = 0;
407 (Container : in out Map;
409 New_Item : Element_Type;
410 Position : out Cursor;
411 Inserted : out Boolean)
415 Length (Container) < Container.Capacity or Contains (Container, Key),
417 Contains (Container, Key)
418 and Has_Element (Container, Position)
420 (Formal_Ordered_Maps.Key (Container, Position), Key)
424 P.Get (Positions (Container), Position)),
427 -- If Key is already in Container, it is not modified and Inserted is
430 (Contains (Container, Key) =>
432 and Model (Container) = Model (Container)'Old
433 and Keys (Container) = Keys (Container)'Old
434 and Positions (Container) = Positions (Container)'Old,
436 -- Otherwise, Key is inserted in Container and Inserted is set to True
440 and Length (Container) = Length (Container)'Old + 1
442 -- Key now maps to New_Item
444 and Formal_Ordered_Maps.Key (Container, Position) = Key
445 and Element (Model (Container), Key) = New_Item
447 -- Other mappings are preserved
449 and Model (Container)'Old <= Model (Container)
450 and M.Keys_Included_Except
452 Model (Container)'Old,
455 -- The keys of Container located before Position are preserved
458 (Left => Keys (Container)'Old,
459 Right => Keys (Container),
461 Lst => P.Get (Positions (Container), Position) - 1)
463 -- Other keys are shifted by 1
466 (Left => Keys (Container)'Old,
467 Right => Keys (Container),
468 Fst => P.Get (Positions (Container), Position),
469 Lst => Length (Container)'Old,
472 -- A new cursor has been inserted at position Position in
475 and P_Positions_Shifted
476 (Positions (Container)'Old,
477 Positions (Container),
478 Cut => P.Get (Positions (Container), Position)));
481 (Container : in out Map;
483 New_Item : Element_Type)
487 Length (Container) < Container.Capacity
488 and then (not Contains (Container, Key)),
490 Length (Container) = Length (Container)'Old + 1
491 and Contains (Container, Key)
493 -- Key now maps to New_Item
495 and K.Get (Keys (Container), Find (Keys (Container), Key)) = Key
496 and Element (Model (Container), Key) = New_Item
498 -- Other mappings are preserved
500 and Model (Container)'Old <= Model (Container)
501 and M.Keys_Included_Except
503 Model (Container)'Old,
506 -- The keys of Container located before Key are preserved
509 (Left => Keys (Container)'Old,
510 Right => Keys (Container),
512 Lst => Find (Keys (Container), Key) - 1)
514 -- Other keys are shifted by 1
517 (Left => Keys (Container)'Old,
518 Right => Keys (Container),
519 Fst => Find (Keys (Container), Key),
520 Lst => Length (Container)'Old,
523 -- A new cursor has been inserted in Container
525 and P_Positions_Shifted
526 (Positions (Container)'Old,
527 Positions (Container),
528 Cut => Find (Keys (Container), Key));
531 (Container : in out Map;
533 New_Item : Element_Type)
537 Length (Container) < Container.Capacity or Contains (Container, Key),
539 Contains (Container, Key) and Element (Container, Key) = New_Item,
542 -- If Key is already in Container, Key is mapped to New_Item
544 (Contains (Container, Key) =>
546 -- Cursors are preserved
548 Positions (Container) = Positions (Container)'Old
550 -- The key equivalent to Key in Container is replaced by Key
553 (Keys (Container), Find (Keys (Container), Key)) = Key
556 (Keys (Container)'Old,
558 Find (Keys (Container), Key))
560 -- Elements associated with other keys are preserved
562 and M.Same_Keys (Model (Container), Model (Container)'Old)
563 and M.Elements_Equal_Except
565 Model (Container)'Old,
568 -- Otherwise, Key is inserted in Container
571 Length (Container) = Length (Container)'Old + 1
573 -- Other mappings are preserved
575 and Model (Container)'Old <= Model (Container)
576 and M.Keys_Included_Except
578 Model (Container)'Old,
581 -- Key is inserted in Container
584 (Keys (Container), Find (Keys (Container), Key)) = Key
586 -- The keys of Container located before Key are preserved
589 (Left => Keys (Container)'Old,
590 Right => Keys (Container),
592 Lst => Find (Keys (Container), Key) - 1)
594 -- Other keys are shifted by 1
597 (Left => Keys (Container)'Old,
598 Right => Keys (Container),
599 Fst => Find (Keys (Container), Key),
600 Lst => Length (Container)'Old,
603 -- A new cursor has been inserted in Container
605 and P_Positions_Shifted
606 (Positions (Container)'Old,
607 Positions (Container),
608 Cut => Find (Keys (Container), Key)));
611 (Container : in out Map;
613 New_Item : Element_Type)
616 Pre => Contains (Container, Key),
619 -- Cursors are preserved
621 Positions (Container) = Positions (Container)'Old
623 -- The key equivalent to Key in Container is replaced by Key
625 and K.Get (Keys (Container), Find (Keys (Container), Key)) = Key
627 (Keys (Container)'Old,
629 Find (Keys (Container), Key))
631 -- New_Item is now associated with the Key in Container
633 and Element (Model (Container), Key) = New_Item
635 -- Elements associated with other keys are preserved
637 and M.Same_Keys (Model (Container), Model (Container)'Old)
638 and M.Elements_Equal_Except
640 Model (Container)'Old,
643 procedure Exclude (Container : in out Map; Key : Key_Type) with
645 Post => not Contains (Container, Key),
648 -- If Key is not in Container, nothing is changed
650 (not Contains (Container, Key) =>
651 Model (Container) = Model (Container)'Old
652 and Keys (Container) = Keys (Container)'Old
653 and Positions (Container) = Positions (Container)'Old,
655 -- Otherwise, Key is removed from Container
658 Length (Container) = Length (Container)'Old - 1
660 -- Other mappings are preserved
662 and Model (Container) <= Model (Container)'Old
663 and M.Keys_Included_Except
664 (Model (Container)'Old,
668 -- The keys of Container located before Key are preserved
671 (Left => Keys (Container)'Old,
672 Right => Keys (Container),
674 Lst => Find (Keys (Container), Key)'Old - 1)
676 -- The keys located after Key are shifted by 1
679 (Left => Keys (Container),
680 Right => Keys (Container)'Old,
681 Fst => Find (Keys (Container), Key)'Old,
682 Lst => Length (Container),
685 -- A cursor has been removed from Container
687 and P_Positions_Shifted
688 (Positions (Container),
689 Positions (Container)'Old,
690 Cut => Find (Keys (Container), Key)'Old));
692 procedure Delete (Container : in out Map; Key : Key_Type) with
694 Pre => Contains (Container, Key),
696 Length (Container) = Length (Container)'Old - 1
698 -- Key is no longer in Container
700 and not Contains (Container, Key)
702 -- Other mappings are preserved
704 and Model (Container) <= Model (Container)'Old
705 and M.Keys_Included_Except
706 (Model (Container)'Old,
710 -- The keys of Container located before Key are preserved
713 (Left => Keys (Container)'Old,
714 Right => Keys (Container),
716 Lst => Find (Keys (Container), Key)'Old - 1)
718 -- The keys located after Key are shifted by 1
721 (Left => Keys (Container),
722 Right => Keys (Container)'Old,
723 Fst => Find (Keys (Container), Key)'Old,
724 Lst => Length (Container),
727 -- A cursor has been removed from Container
729 and P_Positions_Shifted
730 (Positions (Container),
731 Positions (Container)'Old,
732 Cut => Find (Keys (Container), Key)'Old);
734 procedure Delete (Container : in out Map; Position : in out Cursor) with
736 Pre => Has_Element (Container, Position),
738 Position = No_Element
739 and Length (Container) = Length (Container)'Old - 1
741 -- The key at position Position is no longer in Container
743 and not Contains (Container, Key (Container, Position)'Old)
744 and not P.Has_Key (Positions (Container), Position'Old)
746 -- Other mappings are preserved
748 and Model (Container) <= Model (Container)'Old
749 and M.Keys_Included_Except
750 (Model (Container)'Old,
752 Key (Container, Position)'Old)
754 -- The keys of Container located before Position are preserved.
757 (Left => Keys (Container)'Old,
758 Right => Keys (Container),
760 Lst => P.Get (Positions (Container)'Old, Position'Old) - 1)
762 -- The keys located after Position are shifted by 1
765 (Left => Keys (Container),
766 Right => Keys (Container)'Old,
767 Fst => P.Get (Positions (Container)'Old, Position'Old),
768 Lst => Length (Container),
771 -- Position has been removed from Container
773 and P_Positions_Shifted
774 (Positions (Container),
775 Positions (Container)'Old,
776 Cut => P.Get (Positions (Container)'Old, Position'Old));
778 procedure Delete_First (Container : in out Map) with
781 (Length (Container) = 0 => Length (Container) = 0,
783 Length (Container) = Length (Container)'Old - 1
785 -- The first key has been removed from Container
787 and not Contains (Container, First_Key (Container)'Old)
789 -- Other mappings are preserved
791 and Model (Container) <= Model (Container)'Old
792 and M.Keys_Included_Except
793 (Model (Container)'Old,
795 First_Key (Container)'Old)
797 -- Other keys are shifted by 1
800 (Left => Keys (Container),
801 Right => Keys (Container)'Old,
803 Lst => Length (Container),
806 -- First has been removed from Container
808 and P_Positions_Shifted
809 (Positions (Container),
810 Positions (Container)'Old,
813 procedure Delete_Last (Container : in out Map) with
816 (Length (Container) = 0 => Length (Container) = 0,
818 Length (Container) = Length (Container)'Old - 1
820 -- The last key has been removed from Container
822 and not Contains (Container, Last_Key (Container)'Old)
824 -- Other mappings are preserved
826 and Model (Container) <= Model (Container)'Old
827 and M.Keys_Included_Except
828 (Model (Container)'Old,
830 Last_Key (Container)'Old)
832 -- Others keys of Container are preserved
835 (Left => Keys (Container)'Old,
836 Right => Keys (Container),
838 Lst => Length (Container))
840 -- Last cursor has been removed from Container
842 and Positions (Container) <= Positions (Container)'Old);
844 function First (Container : Map) return Cursor with
847 (Length (Container) = 0 =>
848 First'Result = No_Element,
851 Has_Element (Container, First'Result)
852 and P.Get (Positions (Container), First'Result) = 1);
854 function First_Element (Container : Map) return Element_Type with
856 Pre => not Is_Empty (Container),
858 First_Element'Result =
859 Element (Model (Container), First_Key (Container));
861 function First_Key (Container : Map) return Key_Type with
863 Pre => not Is_Empty (Container),
865 First_Key'Result = K.Get (Keys (Container), 1)
866 and K_Smaller_Than_Range
867 (Keys (Container), 2, Length (Container), First_Key'Result);
869 function Last (Container : Map) return Cursor with
872 (Length (Container) = 0 =>
873 Last'Result = No_Element,
876 Has_Element (Container, Last'Result)
877 and P.Get (Positions (Container), Last'Result) =
880 function Last_Element (Container : Map) return Element_Type with
882 Pre => not Is_Empty (Container),
884 Last_Element'Result = Element (Model (Container), Last_Key (Container));
886 function Last_Key (Container : Map) return Key_Type with
888 Pre => not Is_Empty (Container),
890 Last_Key'Result = K.Get (Keys (Container), Length (Container))
891 and K_Bigger_Than_Range
892 (Keys (Container), 1, Length (Container) - 1, Last_Key'Result);
894 function Next (Container : Map; Position : Cursor) return Cursor with
897 Has_Element (Container, Position) or else Position = No_Element,
899 (Position = No_Element
900 or else P.Get (Positions (Container), Position) = Length (Container)
902 Next'Result = No_Element,
905 Has_Element (Container, Next'Result)
906 and then P.Get (Positions (Container), Next'Result) =
907 P.Get (Positions (Container), Position) + 1);
909 procedure Next (Container : Map; Position : in out Cursor) with
912 Has_Element (Container, Position) or else Position = No_Element,
914 (Position = No_Element
915 or else P.Get (Positions (Container), Position) = Length (Container)
917 Position = No_Element,
920 Has_Element (Container, Position)
921 and then P.Get (Positions (Container), Position) =
922 P.Get (Positions (Container), Position'Old) + 1);
924 function Previous (Container : Map; Position : Cursor) return Cursor with
927 Has_Element (Container, Position) or else Position = No_Element,
929 (Position = No_Element
930 or else P.Get (Positions (Container), Position) = 1
932 Previous'Result = No_Element,
935 Has_Element (Container, Previous'Result)
936 and then P.Get (Positions (Container), Previous'Result) =
937 P.Get (Positions (Container), Position) - 1);
939 procedure Previous (Container : Map; Position : in out Cursor) with
942 Has_Element (Container, Position) or else Position = No_Element,
944 (Position = No_Element
945 or else P.Get (Positions (Container), Position) = 1
947 Position = No_Element,
950 Has_Element (Container, Position)
951 and then P.Get (Positions (Container), Position) =
952 P.Get (Positions (Container), Position'Old) - 1);
954 function Find (Container : Map; Key : Key_Type) return Cursor with
958 -- If Key is not contained in Container, Find returns No_Element
960 (not Contains (Model (Container), Key) =>
961 not P.Has_Key (Positions (Container), Find'Result)
962 and Find'Result = No_Element,
964 -- Otherwise, Find returns a valid cursor in Container
967 P.Has_Key (Positions (Container), Find'Result)
968 and P.Get (Positions (Container), Find'Result) =
969 Find (Keys (Container), Key)
971 -- The key designated by the result of Find is Key
974 (Formal_Ordered_Maps.Key (Container, Find'Result), Key));
976 function Element (Container : Map; Key : Key_Type) return Element_Type with
978 Pre => Contains (Container, Key),
979 Post => Element'Result = Element (Model (Container), Key);
980 pragma Annotate (GNATprove, Inline_For_Proof, Element);
982 function Floor (Container : Map; Key : Key_Type) return Cursor with
985 (Length (Container) = 0 or else Key < First_Key (Container) =>
986 Floor'Result = No_Element,
989 Has_Element (Container, Floor'Result)
990 and not (Key < K.Get (Keys (Container),
991 P.Get (Positions (Container), Floor'Result)))
995 P.Get (Positions (Container), Floor'Result)));
997 function Ceiling (Container : Map; Key : Key_Type) return Cursor with
1000 (Length (Container) = 0 or else Last_Key (Container) < Key =>
1001 Ceiling'Result = No_Element,
1003 Has_Element (Container, Ceiling'Result)
1006 P.Get (Positions (Container), Ceiling'Result)) < Key)
1010 P.Get (Positions (Container), Ceiling'Result)));
1012 function Contains (Container : Map; Key : Key_Type) return Boolean with
1014 Post => Contains'Result = Contains (Model (Container), Key);
1015 pragma Annotate (GNATprove, Inline_For_Proof, Contains);
1017 function Has_Element (Container : Map; Position : Cursor) return Boolean
1021 Has_Element'Result = P.Has_Key (Positions (Container), Position);
1022 pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
1025 pragma SPARK_Mode (Off);
1027 pragma Inline (Next);
1028 pragma Inline (Previous);
1030 subtype Node_Access is Count_Type;
1032 use Red_Black_Trees;
1034 type Node_Type is record
1035 Has_Element : Boolean := False;
1036 Parent : Node_Access := 0;
1037 Left : Node_Access := 0;
1038 Right : Node_Access := 0;
1039 Color : Red_Black_Trees.Color_Type := Red;
1041 Element : Element_Type;
1044 package Tree_Types is
1045 new Ada.Containers.Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type);
1047 type Map (Capacity : Count_Type) is
1048 new Tree_Types.Tree_Type (Capacity) with null record;
1050 Empty_Map : constant Map := (Capacity => 0, others => <>);
1052 end Ada.Containers.Formal_Ordered_Maps;