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-2013, 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 -- There are four new functions:
49 -- function Strict_Equal (Left, Right : Map) return Boolean;
50 -- function Overlap (Left, Right : Map) return Boolean;
51 -- function Left (Container : Map; Position : Cursor) return Map;
52 -- function Right (Container : Map; Position : Cursor) return Map;
54 -- See detailed specifications for these subprograms
56 private with Ada
.Containers
.Hash_Tables
;
59 type Key_Type
is private;
60 type Element_Type
is private;
62 with function Hash
(Key
: Key_Type
) return Hash_Type
;
63 with function Equivalent_Keys
(Left
, Right
: Key_Type
) return Boolean;
64 with function "=" (Left
, Right
: Element_Type
) return Boolean is <>;
66 package Ada
.Containers
.Formal_Hashed_Maps
is
69 type Map
(Capacity
: Count_Type
; Modulus
: Hash_Type
) is private;
70 pragma Preelaborable_Initialization
(Map
);
72 type Cursor
is private;
73 pragma Preelaborable_Initialization
(Cursor
);
75 Empty_Map
: constant Map
;
77 No_Element
: constant Cursor
;
79 function "=" (Left
, Right
: Map
) return Boolean;
81 function Capacity
(Container
: Map
) return Count_Type
;
83 procedure Reserve_Capacity
84 (Container
: in out Map
;
85 Capacity
: Count_Type
)
87 Pre
=> Capacity
<= Container
.Capacity
;
89 function Length
(Container
: Map
) return Count_Type
;
91 function Is_Empty
(Container
: Map
) return Boolean;
93 procedure Clear
(Container
: in out Map
);
95 procedure Assign
(Target
: in out Map
; Source
: Map
) with
96 Pre
=> Target
.Capacity
>= Length
(Source
);
100 Capacity
: Count_Type
:= 0) return Map
102 Pre
=> Capacity
>= Source
.Capacity
;
103 -- Copy returns a container stricty equal to Source. It must have
104 -- the same cursors associated with each element. Therefore:
105 -- - capacity=0 means use container.capacity as capacity of target
106 -- - the modulus cannot be changed.
108 function Key
(Container
: Map
; Position
: Cursor
) return Key_Type
with
109 Pre
=> Has_Element
(Container
, Position
);
113 Position
: Cursor
) return Element_Type
115 Pre
=> Has_Element
(Container
, Position
);
117 procedure Replace_Element
118 (Container
: in out Map
;
120 New_Item
: Element_Type
)
122 Pre
=> Has_Element
(Container
, Position
);
124 procedure Move
(Target
: in out Map
; Source
: in out Map
) with
125 Pre
=> Target
.Capacity
>= Length
(Source
);
128 (Container
: in out Map
;
130 New_Item
: Element_Type
;
131 Position
: out Cursor
;
132 Inserted
: out Boolean)
134 Pre
=> Length
(Container
) < Container
.Capacity
;
137 (Container
: in out Map
;
139 New_Item
: Element_Type
)
141 Pre
=> Length
(Container
) < Container
.Capacity
142 and then (not Contains
(Container
, Key
));
145 (Container
: in out Map
;
147 New_Item
: Element_Type
)
149 Pre
=> Length
(Container
) < Container
.Capacity
;
152 (Container
: in out Map
;
154 New_Item
: Element_Type
)
156 Pre
=> Contains
(Container
, Key
);
158 procedure Exclude
(Container
: in out Map
; Key
: Key_Type
);
160 procedure Delete
(Container
: in out Map
; Key
: Key_Type
) with
161 Pre
=> Contains
(Container
, Key
);
163 procedure Delete
(Container
: in out Map
; Position
: in out Cursor
) with
164 Pre
=> Has_Element
(Container
, Position
);
166 function First
(Container
: Map
) return Cursor
;
168 function Next
(Container
: Map
; Position
: Cursor
) return Cursor
with
169 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
171 procedure Next
(Container
: Map
; Position
: in out Cursor
) with
172 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
174 function Find
(Container
: Map
; Key
: Key_Type
) return Cursor
;
176 function Contains
(Container
: Map
; Key
: Key_Type
) return Boolean;
178 function Element
(Container
: Map
; Key
: Key_Type
) return Element_Type
with
179 Pre
=> Contains
(Container
, Key
);
181 function Has_Element
(Container
: Map
; Position
: Cursor
) return Boolean;
183 function Equivalent_Keys
187 CRight
: Cursor
) return Boolean;
189 function Equivalent_Keys
192 Right
: Key_Type
) return Boolean;
194 function Equivalent_Keys
197 CRight
: Cursor
) return Boolean;
199 function Default_Modulus
(Capacity
: Count_Type
) return Hash_Type
;
201 function Strict_Equal
(Left
, Right
: Map
) return Boolean;
202 -- Strict_Equal returns True if the containers are physically equal, i.e.
203 -- they are structurally equal (function "=" returns True) and that they
204 -- have the same set of cursors.
206 function Left
(Container
: Map
; Position
: Cursor
) return Map
with
207 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
208 function Right
(Container
: Map
; Position
: Cursor
) return Map
with
209 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
210 -- Left returns a container containing all elements preceding Position
211 -- (excluded) in Container. Right returns a container containing all
212 -- elements following Position (included) in Container. These two new
213 -- functions can be used to express invariant properties in loops which
214 -- iterate over containers. Left returns the part of the container already
215 -- scanned and Right the part not scanned yet.
217 function Overlap
(Left
, Right
: Map
) return Boolean;
218 -- Overlap returns True if the containers have common keys
221 pragma Inline
(Length
);
222 pragma Inline
(Is_Empty
);
223 pragma Inline
(Clear
);
225 pragma Inline
(Element
);
226 pragma Inline
(Contains
);
227 pragma Inline
(Capacity
);
228 pragma Inline
(Has_Element
);
229 pragma Inline
(Equivalent_Keys
);
230 pragma Inline
(Next
);
232 type Node_Type
is record
234 Element
: Element_Type
;
236 Has_Element
: Boolean := False;
239 package HT_Types
is new
240 Ada
.Containers
.Hash_Tables
.Generic_Bounded_Hash_Table_Types
243 type Map
(Capacity
: Count_Type
; Modulus
: Hash_Type
) is
244 new HT_Types
.Hash_Table_Type
(Capacity
, Modulus
) with null record;
248 type Cursor
is record
252 Empty_Map
: constant Map
:= (Capacity
=> 0, Modulus
=> 0, others => <>);
254 No_Element
: constant Cursor
:= (Node
=> 0);
256 end Ada
.Containers
.Formal_Hashed_Maps
;