File : a-cfhama.ads
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT LIBRARY COMPONENTS --
4 -- --
5 -- A D A . C O N T A I N E R S . F O R M A L _ H A S H E D _ M A P S --
6 -- --
7 -- S p e c --
8 -- --
9 -- Copyright (C) 2004-2015, Free Software Foundation, Inc. --
10 -- --
11 -- This specification is derived from the Ada Reference Manual for use with --
12 -- GNAT. The copyright notice above, and the license provisions that follow --
13 -- apply solely to the contents of the part following the private keyword. --
14 -- --
15 -- GNAT is free software; you can redistribute it and/or modify it under --
16 -- terms of the GNU General Public License as published by the Free Soft- --
17 -- ware Foundation; either version 3, or (at your option) any later ver- --
18 -- sion. GNAT is distributed in the hope that it will be useful, but WITH- --
19 -- OUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY --
20 -- or FITNESS FOR A PARTICULAR PURPOSE. --
21 -- --
22 -- --
23 -- --
24 -- --
25 -- --
26 -- You should have received a copy of the GNU General Public License and --
27 -- a copy of the GCC Runtime Library Exception along with this program; --
28 -- see the files COPYING3 and COPYING.RUNTIME respectively. If not, see --
29 -- <http://www.gnu.org/licenses/>. --
30 ------------------------------------------------------------------------------
31
32 -- This spec is derived from package Ada.Containers.Bounded_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.
37
38 -- The modifications are:
39
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.
46
47 -- There are four new functions:
48
49 -- function Strict_Equal (Left, Right : Map) return Boolean;
50 -- function Overlap (Left, Right : Map) return Boolean;
51 -- function First_To_Previous (Container : Map; Current : Cursor)
52 -- return Map;
53 -- function Current_To_Last (Container : Map; Current : Cursor)
54 -- return Map;
55
56 -- See detailed specifications for these subprograms
57
58 private with Ada.Containers.Hash_Tables;
59
60 generic
61 type Key_Type is private;
62 type Element_Type is private;
63
64 with function Hash (Key : Key_Type) return Hash_Type;
65 with function Equivalent_Keys (Left, Right : Key_Type) return Boolean;
66 with function "=" (Left, Right : Element_Type) return Boolean is <>;
67
68 package Ada.Containers.Formal_Hashed_Maps with
69 Pure,
70 SPARK_Mode
71 is
72 pragma Annotate (GNATprove, External_Axiomatization);
73 pragma Annotate (CodePeer, Skip_Analysis);
74
75 type Map (Capacity : Count_Type; Modulus : Hash_Type) is private with
76 Iterable => (First => First,
77 Next => Next,
78 Has_Element => Has_Element,
79 Element => Element),
80 Default_Initial_Condition => Is_Empty (Map);
81 pragma Preelaborable_Initialization (Map);
82
83 type Cursor is private;
84 pragma Preelaborable_Initialization (Cursor);
85
86 Empty_Map : constant Map;
87
88 No_Element : constant Cursor;
89
90 function "=" (Left, Right : Map) return Boolean with
91 Global => null;
92
93 function Capacity (Container : Map) return Count_Type with
94 Global => null;
95
96 procedure Reserve_Capacity
97 (Container : in out Map;
98 Capacity : Count_Type)
99 with
100 Global => null,
101 Pre => Capacity <= Container.Capacity;
102
103 function Length (Container : Map) return Count_Type with
104 Global => null;
105
106 function Is_Empty (Container : Map) return Boolean with
107 Global => null;
108
109 procedure Clear (Container : in out Map) with
110 Global => null;
111
112 procedure Assign (Target : in out Map; Source : Map) with
113 Global => null,
114 Pre => Target.Capacity >= Length (Source);
115
116 function Copy
117 (Source : Map;
118 Capacity : Count_Type := 0) return Map
119 with
120 Global => null,
121 Pre => Capacity = 0 or else Capacity >= Source.Capacity;
122 -- Copy returns a container stricty equal to Source. It must have
123 -- the same cursors associated with each element. Therefore:
124 -- - capacity=0 means use container.capacity as capacity of target
125 -- - the modulus cannot be changed.
126
127 function Key (Container : Map; Position : Cursor) return Key_Type with
128 Global => null,
129 Pre => Has_Element (Container, Position);
130
131 function Element
132 (Container : Map;
133 Position : Cursor) return Element_Type
134 with
135 Global => null,
136 Pre => Has_Element (Container, Position);
137
138 procedure Replace_Element
139 (Container : in out Map;
140 Position : Cursor;
141 New_Item : Element_Type)
142 with
143 Global => null,
144 Pre => Has_Element (Container, Position);
145
146 procedure Move (Target : in out Map; Source : in out Map) with
147 Global => null,
148 Pre => Target.Capacity >= Length (Source);
149
150 procedure Insert
151 (Container : in out Map;
152 Key : Key_Type;
153 New_Item : Element_Type;
154 Position : out Cursor;
155 Inserted : out Boolean)
156 with
157 Global => null,
158 Pre => Length (Container) < Container.Capacity;
159
160 procedure Insert
161 (Container : in out Map;
162 Key : Key_Type;
163 New_Item : Element_Type)
164 with
165 Global => null,
166 Pre => Length (Container) < Container.Capacity
167 and then (not Contains (Container, Key));
168
169 procedure Include
170 (Container : in out Map;
171 Key : Key_Type;
172 New_Item : Element_Type)
173 with
174 Global => null,
175 Pre => Length (Container) < Container.Capacity;
176
177 procedure Replace
178 (Container : in out Map;
179 Key : Key_Type;
180 New_Item : Element_Type)
181 with
182 Global => null,
183 Pre => Contains (Container, Key);
184
185 procedure Exclude (Container : in out Map; Key : Key_Type) with
186 Global => null;
187
188 procedure Delete (Container : in out Map; Key : Key_Type) with
189 Global => null,
190 Pre => Contains (Container, Key);
191
192 procedure Delete (Container : in out Map; Position : in out Cursor) with
193 Global => null,
194 Pre => Has_Element (Container, Position);
195
196 function First (Container : Map) return Cursor with
197 Global => null;
198
199 function Next (Container : Map; Position : Cursor) return Cursor with
200 Global => null,
201 Pre => Has_Element (Container, Position) or else Position = No_Element;
202
203 procedure Next (Container : Map; Position : in out Cursor) with
204 Global => null,
205 Pre => Has_Element (Container, Position) or else Position = No_Element;
206
207 function Find (Container : Map; Key : Key_Type) return Cursor with
208 Global => null;
209
210 function Contains (Container : Map; Key : Key_Type) return Boolean with
211 Global => null;
212
213 function Element (Container : Map; Key : Key_Type) return Element_Type with
214 Global => null,
215 Pre => Contains (Container, Key);
216
217 function Has_Element (Container : Map; Position : Cursor) return Boolean
218 with
219 Global => null;
220
221 function Equivalent_Keys
222 (Left : Map;
223 CLeft : Cursor;
224 Right : Map;
225 CRight : Cursor) return Boolean
226 with
227 Global => null;
228
229 function Equivalent_Keys
230 (Left : Map;
231 CLeft : Cursor;
232 Right : Key_Type) return Boolean
233 with
234 Global => null;
235
236 function Equivalent_Keys
237 (Left : Key_Type;
238 Right : Map;
239 CRight : Cursor) return Boolean
240 with
241 Global => null;
242
243 function Default_Modulus (Capacity : Count_Type) return Hash_Type with
244 Global => null;
245
246 function Strict_Equal (Left, Right : Map) return Boolean with
247 Ghost,
248 Global => null;
249 -- Strict_Equal returns True if the containers are physically equal, i.e.
250 -- they are structurally equal (function "=" returns True) and that they
251 -- have the same set of cursors.
252
253 function First_To_Previous (Container : Map; Current : Cursor) return Map
254 with
255 Ghost,
256 Global => null,
257 Pre => Has_Element (Container, Current) or else Current = No_Element;
258
259 function Current_To_Last (Container : Map; Current : Cursor) return Map
260 with
261 Ghost,
262 Global => null,
263 Pre => Has_Element (Container, Current) or else Current = No_Element;
264 -- First_To_Previous returns a container containing all elements preceding
265 -- Current (excluded) in Container. Current_To_Last returns a container
266 -- containing all elements following Current (included) in Container.
267 -- These two new functions can be used to express invariant properties in
268 -- loops which iterate over containers. First_To_Previous returns the part
269 -- of the container already scanned and Current_To_Last the part not
270 -- scanned yet.
271
272 function Overlap (Left, Right : Map) return Boolean with
273 Global => null;
274 -- Overlap returns True if the containers have common keys
275
276 private
277 pragma SPARK_Mode (Off);
278
279 pragma Inline (Length);
280 pragma Inline (Is_Empty);
281 pragma Inline (Clear);
282 pragma Inline (Key);
283 pragma Inline (Element);
284 pragma Inline (Contains);
285 pragma Inline (Capacity);
286 pragma Inline (Has_Element);
287 pragma Inline (Equivalent_Keys);
288 pragma Inline (Next);
289
290 type Node_Type is record
291 Key : Key_Type;
292 Element : Element_Type;
293 Next : Count_Type;
294 Has_Element : Boolean := False;
295 end record;
296
297 package HT_Types is new
298 Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type);
299
300 type Map (Capacity : Count_Type; Modulus : Hash_Type) is
301 new HT_Types.Hash_Table_Type (Capacity, Modulus) with null record;
302
303 use HT_Types;
304
305 type Cursor is record
306 Node : Count_Type;
307 end record;
308
309 Empty_Map : constant Map := (Capacity => 0, Modulus => 0, others => <>);
310
311 No_Element : constant Cursor := (Node => 0);
312
313 end Ada.Containers.Formal_Hashed_Maps;