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 _ H A S H E D _ M A P S --
9 -- Copyright (C) 2004-2017, 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_Hashed_Maps in the
33 -- Ada 2012 RM. The modifications are meant to facilitate formal proofs by
34 -- making it easier to express properties, and by making the specification of
35 -- this unit compatible with SPARK 2014. Note that the API of this unit may be
36 -- subject to incompatible changes as SPARK 2014 evolves.
38 -- The modifications are:
40 -- A parameter for the container is added to every function reading the
41 -- contents of a container: Key, Element, Next, Query_Element, Has_Element,
42 -- Iterate, Equivalent_Keys. This change is motivated by the need to have
43 -- cursors which are valid on different containers (typically a container C
44 -- and its previous version C'Old) for expressing properties, which is not
45 -- possible if cursors encapsulate an access to the underlying container.
47 -- Iteration over maps is done using the Iterable aspect, which is SPARK
48 -- compatible. "For of" iteration ranges over keys instead of elements.
50 with Ada
.Containers
.Functional_Vectors
;
51 with Ada
.Containers
.Functional_Maps
;
52 private with Ada
.Containers
.Hash_Tables
;
55 type Key_Type
is private;
56 type Element_Type
is private;
58 with function Hash
(Key
: Key_Type
) return Hash_Type
;
59 with function Equivalent_Keys
61 Right
: Key_Type
) return Boolean is "=";
63 package Ada
.Containers
.Formal_Hashed_Maps
with
66 pragma Annotate
(CodePeer
, Skip_Analysis
);
68 type Map
(Capacity
: Count_Type
; Modulus
: Hash_Type
) is private with
69 Iterable
=> (First
=> First
,
71 Has_Element
=> Has_Element
,
73 Default_Initial_Condition
=> Is_Empty
(Map
);
74 pragma Preelaborable_Initialization
(Map
);
76 Empty_Map
: constant Map
;
82 No_Element
: constant Cursor
:= (Node
=> 0);
84 function Length
(Container
: Map
) return Count_Type
with
86 Post
=> Length
'Result <= Container
.Capacity
;
88 pragma Unevaluated_Use_Of_Old
(Allow
);
90 package Formal_Model
with Ghost
is
91 subtype Positive_Count_Type
is Count_Type
range 1 .. Count_Type
'Last;
93 package M
is new Ada
.Containers
.Functional_Maps
94 (Element_Type
=> Element_Type
,
96 Equivalent_Keys
=> Equivalent_Keys
);
100 Right
: M
.Map
) return Boolean renames M
."=";
104 Right
: M
.Map
) return Boolean renames M
."<=";
106 package K
is new Ada
.Containers
.Functional_Vectors
107 (Element_Type
=> Key_Type
,
108 Index_Type
=> Positive_Count_Type
);
112 Right
: K
.Sequence
) return Boolean renames K
."=";
116 Right
: K
.Sequence
) return Boolean renames K
."<";
120 Right
: K
.Sequence
) return Boolean renames K
."<=";
122 function Find
(Container
: K
.Sequence
; Key
: Key_Type
) return Count_Type
123 -- Search for Key in Container
128 (if Find
'Result > 0 then
129 Find
'Result <= K
.Length
(Container
)
130 and Equivalent_Keys
(Key
, K
.Get
(Container
, Find
'Result)));
132 function K_Keys_Included
134 Right
: K
.Sequence
) return Boolean
135 -- Return True if Right contains all the keys of Left
140 K_Keys_Included
'Result =
141 (for all I
in 1 .. K
.Length
(Left
) =>
142 Find
(Right
, K
.Get
(Left
, I
)) > 0
143 and then K
.Get
(Right
, Find
(Right
, K
.Get
(Left
, I
))) =
146 package P
is new Ada
.Containers
.Functional_Maps
148 Element_Type
=> Positive_Count_Type
,
149 Equivalent_Keys
=> "=",
150 Enable_Handling_Of_Equivalence
=> False);
154 Right
: P
.Map
) return Boolean renames P
."=";
158 Right
: P
.Map
) return Boolean renames P
."<=";
160 function Mapping_Preserved
161 (K_Left
: K
.Sequence
;
162 K_Right
: K
.Sequence
;
164 P_Right
: P
.Map
) return Boolean
168 (if Mapping_Preserved
'Result then
170 -- Right contains all the cursors of Left
172 P
.Keys_Included
(P_Left
, P_Right
)
174 -- Right contains all the keys of Left
176 and K_Keys_Included
(K_Left
, K_Right
)
178 -- Mappings from cursors to elements induced by K_Left, P_Left
179 -- and K_Right, P_Right are the same.
181 and (for all C
of P_Left
=>
182 K
.Get
(K_Left
, P
.Get
(P_Left
, C
)) =
183 K
.Get
(K_Right
, P
.Get
(P_Right
, C
))));
185 function Model
(Container
: Map
) return M
.Map
with
186 -- The high-level model of a map is a map from keys to elements. Neither
187 -- cursors nor order of elements are represented in this model. Keys are
188 -- modeled up to equivalence.
193 function Keys
(Container
: Map
) return K
.Sequence
with
194 -- The Keys sequence represents the underlying list structure of maps
195 -- that is used for iteration. It stores the actual values of keys in
196 -- the map. It does not model cursors nor elements.
201 K
.Length
(Keys
'Result) = Length
(Container
)
203 -- It only contains keys contained in Model
205 and (for all Key
of Keys
'Result =>
206 M
.Has_Key
(Model
(Container
), Key
))
208 -- It contains all the keys contained in Model
210 and (for all Key
of Model
(Container
) =>
211 (Find
(Keys
'Result, Key
) > 0
212 and then Equivalent_Keys
213 (K
.Get
(Keys
'Result, Find
(Keys
'Result, Key
)),
216 -- It has no duplicate
218 and (for all I
in 1 .. Length
(Container
) =>
219 Find
(Keys
'Result, K
.Get
(Keys
'Result, I
)) = I
)
221 and (for all I
in 1 .. Length
(Container
) =>
222 (for all J
in 1 .. Length
(Container
) =>
224 (K
.Get
(Keys
'Result, I
), K
.Get
(Keys
'Result, J
))
227 pragma Annotate
(GNATprove
, Iterable_For_Proof
, "Model", Keys
);
229 function Positions
(Container
: Map
) return P
.Map
with
230 -- The Positions map is used to model cursors. It only contains valid
231 -- cursors and maps them to their position in the container.
236 not P
.Has_Key
(Positions
'Result, No_Element
)
238 -- Positions of cursors are smaller than the container's length
241 (for all I
of Positions
'Result =>
242 P
.Get
(Positions
'Result, I
) in 1 .. Length
(Container
)
244 -- No two cursors have the same position. Note that we do not
245 -- state that there is a cursor in the map for each position, as
246 -- it is rarely needed.
249 (for all J
of Positions
'Result =>
250 (if P
.Get
(Positions
'Result, I
) = P
.Get
(Positions
'Result, J
)
253 procedure Lift_Abstraction_Level
(Container
: Map
) with
254 -- Lift_Abstraction_Level is a ghost procedure that does nothing but
255 -- assume that we can access the same elements by iterating over
256 -- positions or cursors.
257 -- This information is not generally useful except when switching from
258 -- a low-level, cursor-aware view of a container, to a high-level,
259 -- position-based view.
264 (for all Key
of Keys
(Container
) =>
265 (for some I
of Positions
(Container
) =>
266 K
.Get
(Keys
(Container
), P
.Get
(Positions
(Container
), I
)) =
271 K
: Key_Type
) return Boolean renames M
.Has_Key
;
272 -- To improve readability of contracts, we rename the function used to
273 -- search for a key in the model to Contains.
277 K
: Key_Type
) return Element_Type
renames M
.Get
;
278 -- To improve readability of contracts, we rename the function used to
279 -- access an element in the model to Element.
284 function "=" (Left
, Right
: Map
) return Boolean with
286 Post
=> "="'Result = (Model (Left) = Model (Right));
288 function Capacity (Container : Map) return Count_Type with
290 Post => Capacity'Result = Container.Capacity;
292 procedure Reserve_Capacity
293 (Container : in out Map;
294 Capacity : Count_Type)
297 Pre => Capacity <= Container.Capacity,
299 Model (Container) = Model (Container)'Old
300 and Length (Container)'Old = Length (Container)
302 -- Actual keys are preserved
304 and K_Keys_Included (Keys (Container), Keys (Container)'Old)
305 and K_Keys_Included (Keys (Container)'Old, Keys (Container));
307 function Is_Empty (Container : Map) return Boolean with
309 Post => Is_Empty'Result = (Length (Container) = 0);
311 procedure Clear (Container : in out Map) with
313 Post => Length (Container) = 0 and M.Is_Empty (Model (Container));
315 procedure Assign (Target : in out Map; Source : Map) with
317 Pre => Target.Capacity >= Length (Source),
319 Model (Target) = Model (Source)
320 and Length (Source) = Length (Target)
322 -- Actual keys are preserved
324 and K_Keys_Included (Keys (Target), Keys (Source))
325 and K_Keys_Included (Keys (Source), Keys (Target));
329 Capacity : Count_Type := 0) return Map
332 Pre => Capacity = 0 or else Capacity >= Source.Capacity,
334 Model (Copy'Result) = Model (Source)
335 and Keys (Copy'Result) = Keys (Source)
336 and Positions (Copy'Result) = Positions (Source)
337 and (if Capacity = 0 then
338 Copy'Result.Capacity = Source.Capacity
340 Copy'Result.Capacity = Capacity);
341 -- Copy returns a container stricty equal to Source. It must have the same
342 -- cursors associated with each element. Therefore:
343 -- - capacity=0 means use Source.Capacity as capacity of target
344 -- - the modulus cannot be changed.
346 function Key (Container : Map; Position : Cursor) return Key_Type with
348 Pre => Has_Element (Container, Position),
351 K.Get (Keys (Container), P.Get (Positions (Container), Position));
352 pragma Annotate (GNATprove, Inline_For_Proof, Key);
356 Position : Cursor) return Element_Type
359 Pre => Has_Element (Container, Position),
361 Element'Result = Element (Model (Container), Key (Container, Position));
362 pragma Annotate (GNATprove, Inline_For_Proof, Element);
364 procedure Replace_Element
365 (Container : in out Map;
367 New_Item : Element_Type)
370 Pre => Has_Element (Container, Position),
373 -- Order of keys and cursors is preserved
375 Keys (Container) = Keys (Container)'Old
376 and Positions (Container) = Positions (Container)'Old
378 -- New_Item is now associated with the key at position Position in
381 and Element (Container, Position) = New_Item
383 -- Elements associated with other keys are preserved
385 and M.Same_Keys (Model (Container), Model (Container)'Old)
386 and M.Elements_Equal_Except
388 Model (Container)'Old,
389 Key (Container, Position));
391 procedure Move (Target : in out Map; Source : in out Map) with
393 Pre => Target.Capacity >= Length (Source),
395 Model (Target) = Model (Source)'Old
396 and Length (Source)'Old = Length (Target)
397 and Length (Source) = 0
399 -- Actual keys are preserved
401 and K_Keys_Included (Keys (Target), Keys (Source)'Old)
402 and K_Keys_Included (Keys (Source)'Old, Keys (Target));
405 (Container : in out Map;
407 New_Item : Element_Type;
408 Position : out Cursor;
409 Inserted : out Boolean)
413 Length (Container) < Container.Capacity or Contains (Container, Key),
415 Contains (Container, Key)
416 and Has_Element (Container, Position)
418 (Formal_Hashed_Maps.Key (Container, Position), Key),
421 -- If Key is already in Container, it is not modified and Inserted is
424 (Contains (Container, Key) =>
426 and Model (Container) = Model (Container)'Old
427 and Keys (Container) = Keys (Container)'Old
428 and Positions (Container) = Positions (Container)'Old,
430 -- Otherwise, Key is inserted in Container and Inserted is set to True
434 and Length (Container) = Length (Container)'Old + 1
436 -- Key now maps to New_Item
438 and Formal_Hashed_Maps.Key (Container, Position) = Key
439 and Element (Model (Container), Key) = New_Item
441 -- Other keys are preserved
443 and Model (Container)'Old <= Model (Container)
444 and M.Keys_Included_Except
446 Model (Container)'Old,
449 -- Mapping from cursors to keys is preserved
451 and Mapping_Preserved
452 (K_Left => Keys (Container)'Old,
453 K_Right => Keys (Container),
454 P_Left => Positions (Container)'Old,
455 P_Right => Positions (Container))
456 and P.Keys_Included_Except
457 (Positions (Container),
458 Positions (Container)'Old,
462 (Container : in out Map;
464 New_Item : Element_Type)
468 Length (Container) < Container.Capacity
469 and then (not Contains (Container, Key)),
471 Length (Container) = Length (Container)'Old + 1
472 and Contains (Container, Key)
474 -- Key now maps to New_Item
476 and Formal_Hashed_Maps.Key (Container, Find (Container, Key)) = Key
477 and Element (Model (Container), Key) = New_Item
479 -- Other keys are preserved
481 and Model (Container)'Old <= Model (Container)
482 and M.Keys_Included_Except
484 Model (Container)'Old,
487 -- Mapping from cursors to keys is preserved
489 and Mapping_Preserved
490 (K_Left => Keys (Container)'Old,
491 K_Right => Keys (Container),
492 P_Left => Positions (Container)'Old,
493 P_Right => Positions (Container))
494 and P.Keys_Included_Except
495 (Positions (Container),
496 Positions (Container)'Old,
497 Find (Container, Key));
500 (Container : in out Map;
502 New_Item : Element_Type)
506 Length (Container) < Container.Capacity or Contains (Container, Key),
508 Contains (Container, Key) and Element (Container, Key) = New_Item,
511 -- If Key is already in Container, Key is mapped to New_Item
513 (Contains (Container, Key) =>
515 -- Cursors are preserved
517 Positions (Container) = Positions (Container)'Old
519 -- The key equivalent to Key in Container is replaced by Key
523 P.Get (Positions (Container), Find (Container, Key))) = Key
525 (Keys (Container)'Old,
527 P.Get (Positions (Container), Find (Container, Key)))
529 -- Elements associated with other keys are preserved
531 and M.Same_Keys (Model (Container), Model (Container)'Old)
532 and M.Elements_Equal_Except
534 Model (Container)'Old,
537 -- Otherwise, Key is inserted in Container
540 Length (Container) = Length (Container)'Old + 1
542 -- Other keys are preserved
544 and Model (Container)'Old <= Model (Container)
545 and M.Keys_Included_Except
547 Model (Container)'Old,
550 -- Key is inserted in Container
554 P.Get (Positions (Container), Find (Container, Key))) = Key
556 -- Mapping from cursors to keys is preserved
558 and Mapping_Preserved
559 (K_Left => Keys (Container)'Old,
560 K_Right => Keys (Container),
561 P_Left => Positions (Container)'Old,
562 P_Right => Positions (Container))
563 and P.Keys_Included_Except
564 (Positions (Container),
565 Positions (Container)'Old,
566 Find (Container, Key)));
569 (Container : in out Map;
571 New_Item : Element_Type)
574 Pre => Contains (Container, Key),
577 -- Cursors are preserved
579 Positions (Container) = Positions (Container)'Old
581 -- The key equivalent to Key in Container is replaced by Key
585 P.Get (Positions (Container), Find (Container, Key))) = Key
587 (Keys (Container)'Old,
589 P.Get (Positions (Container), Find (Container, Key)))
591 -- New_Item is now associated with the Key in Container
593 and Element (Model (Container), Key) = New_Item
595 -- Elements associated with other keys are preserved
597 and M.Same_Keys (Model (Container), Model (Container)'Old)
598 and M.Elements_Equal_Except
600 Model (Container)'Old,
603 procedure Exclude (Container : in out Map; Key : Key_Type) with
605 Post => not Contains (Container, Key),
608 -- If Key is not in Container, nothing is changed
610 (not Contains (Container, Key) =>
611 Model (Container) = Model (Container)'Old
612 and Keys (Container) = Keys (Container)'Old
613 and Positions (Container) = Positions (Container)'Old,
615 -- Otherwise, Key is removed from Container
618 Length (Container) = Length (Container)'Old - 1
620 -- Other keys are preserved
622 and Model (Container) <= Model (Container)'Old
623 and M.Keys_Included_Except
624 (Model (Container)'Old,
628 -- Mapping from cursors to keys is preserved
630 and Mapping_Preserved
631 (K_Left => Keys (Container),
632 K_Right => Keys (Container)'Old,
633 P_Left => Positions (Container),
634 P_Right => Positions (Container)'Old)
635 and P.Keys_Included_Except
636 (Positions (Container)'Old,
637 Positions (Container),
638 Find (Container, Key)'Old));
640 procedure Delete (Container : in out Map; Key : Key_Type) with
642 Pre => Contains (Container, Key),
644 Length (Container) = Length (Container)'Old - 1
646 -- Key is no longer in Container
648 and not Contains (Container, Key)
650 -- Other keys are preserved
652 and Model (Container) <= Model (Container)'Old
653 and M.Keys_Included_Except
654 (Model (Container)'Old,
658 -- Mapping from cursors to keys is preserved
660 and Mapping_Preserved
661 (K_Left => Keys (Container),
662 K_Right => Keys (Container)'Old,
663 P_Left => Positions (Container),
664 P_Right => Positions (Container)'Old)
665 and P.Keys_Included_Except
666 (Positions (Container)'Old,
667 Positions (Container),
668 Find (Container, Key)'Old);
670 procedure Delete (Container : in out Map; Position : in out Cursor) with
672 Pre => Has_Element (Container, Position),
674 Position = No_Element
675 and Length (Container) = Length (Container)'Old - 1
677 -- The key at position Position is no longer in Container
679 and not Contains (Container, Key (Container, Position)'Old)
680 and not P.Has_Key (Positions (Container), Position'Old)
682 -- Other keys are preserved
684 and Model (Container) <= Model (Container)'Old
685 and M.Keys_Included_Except
686 (Model (Container)'Old,
688 Key (Container, Position)'Old)
690 -- Mapping from cursors to keys is preserved
692 and Mapping_Preserved
693 (K_Left => Keys (Container),
694 K_Right => Keys (Container)'Old,
695 P_Left => Positions (Container),
696 P_Right => Positions (Container)'Old)
697 and P.Keys_Included_Except
698 (Positions (Container)'Old,
699 Positions (Container),
702 function First (Container : Map) return Cursor with
705 (Length (Container) = 0 =>
706 First'Result = No_Element,
709 Has_Element (Container, First'Result)
710 and P.Get (Positions (Container), First'Result) = 1);
712 function Next (Container : Map; Position : Cursor) return Cursor with
715 Has_Element (Container, Position) or else Position = No_Element,
717 (Position = No_Element
718 or else P.Get (Positions (Container), Position) = Length (Container)
720 Next'Result = No_Element,
723 Has_Element (Container, Next'Result)
724 and then P.Get (Positions (Container), Next'Result) =
725 P.Get (Positions (Container), Position) + 1);
727 procedure Next (Container : Map; Position : in out Cursor) with
730 Has_Element (Container, Position) or else Position = No_Element,
732 (Position = No_Element
733 or else P.Get (Positions (Container), Position) = Length (Container)
735 Position = No_Element,
738 Has_Element (Container, Position)
739 and then P.Get (Positions (Container), Position) =
740 P.Get (Positions (Container), Position'Old) + 1);
742 function Find (Container : Map; Key : Key_Type) return Cursor with
746 -- If Key is not contained in Container, Find returns No_Element
748 (not Contains (Model (Container), Key) =>
749 Find'Result = No_Element,
751 -- Otherwise, Find returns a valid cursor in Container
754 P.Has_Key (Positions (Container), Find'Result)
755 and P.Get (Positions (Container), Find'Result) =
756 Find (Keys (Container), Key)
758 -- The key designated by the result of Find is Key
761 (Formal_Hashed_Maps.Key (Container, Find'Result), Key));
763 function Contains (Container : Map; Key : Key_Type) return Boolean with
765 Post => Contains'Result = Contains (Model (Container), Key);
766 pragma Annotate (GNATprove, Inline_For_Proof, Contains);
768 function Element (Container : Map; Key : Key_Type) return Element_Type with
770 Pre => Contains (Container, Key),
771 Post => Element'Result = Element (Model (Container), Key);
772 pragma Annotate (GNATprove, Inline_For_Proof, Element);
774 function Has_Element (Container : Map; Position : Cursor) return Boolean
778 Has_Element'Result = P.Has_Key (Positions (Container), Position);
779 pragma Annotate (GNATprove, Inline_For_Proof, Has_Element);
781 function Default_Modulus (Capacity : Count_Type) return Hash_Type with
785 pragma SPARK_Mode (Off);
787 pragma Inline (Length);
788 pragma Inline (Is_Empty);
789 pragma Inline (Clear);
791 pragma Inline (Element);
792 pragma Inline (Contains);
793 pragma Inline (Capacity);
794 pragma Inline (Has_Element);
795 pragma Inline (Equivalent_Keys);
796 pragma Inline (Next);
798 type Node_Type is record
800 Element : Element_Type;
802 Has_Element : Boolean := False;
805 package HT_Types is new
806 Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type);
808 type Map (Capacity : Count_Type; Modulus : Hash_Type) is
809 new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
813 Empty_Map : constant Map := (Capacity => 0, Modulus => 0, others => <>);
815 end Ada.Containers.Formal_Hashed_Maps;