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 _ S E T S --
9 -- Copyright (C) 2004-2015, 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_Sets 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 -- content of a container: Element, Next, Query_Element, Has_Element, Key,
42 -- Iterate, Equivalent_Elements. This change is motivated by the need to
43 -- 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
48 -- There are three new functions:
50 -- function Strict_Equal (Left, Right : Set) return Boolean;
51 -- function First_To_Previous (Container : Set; Current : Cursor)
53 -- function Current_To_Last (Container : Set; Current : Cursor)
56 -- See detailed specifications for these subprograms
58 private with Ada
.Containers
.Hash_Tables
;
61 type Element_Type
is private;
63 with function Hash
(Element
: Element_Type
) return Hash_Type
;
65 with function Equivalent_Elements
(Left
, Right
: Element_Type
)
68 with function "=" (Left
, Right
: Element_Type
) return Boolean is <>;
70 package Ada
.Containers
.Formal_Hashed_Sets
with
74 pragma Annotate
(GNATprove
, External_Axiomatization
);
75 pragma Annotate
(CodePeer
, Skip_Analysis
);
77 type Set
(Capacity
: Count_Type
; Modulus
: Hash_Type
) is private with
78 Iterable
=> (First
=> First
,
80 Has_Element
=> Has_Element
,
82 Default_Initial_Condition
=> Is_Empty
(Set
);
83 pragma Preelaborable_Initialization
(Set
);
85 type Cursor
is private;
86 pragma Preelaborable_Initialization
(Cursor
);
88 Empty_Set
: constant Set
;
90 No_Element
: constant Cursor
;
92 function "=" (Left
, Right
: Set
) return Boolean with
95 function Equivalent_Sets
(Left
, Right
: Set
) return Boolean with
98 function To_Set
(New_Item
: Element_Type
) return Set
with
101 function Capacity
(Container
: Set
) return Count_Type
with
104 procedure Reserve_Capacity
105 (Container
: in out Set
;
106 Capacity
: Count_Type
)
109 Pre
=> Capacity
<= Container
.Capacity
;
111 function Length
(Container
: Set
) return Count_Type
with
114 function Is_Empty
(Container
: Set
) return Boolean with
117 procedure Clear
(Container
: in out Set
) with
120 procedure Assign
(Target
: in out Set
; Source
: Set
) with
122 Pre
=> Target
.Capacity
>= Length
(Source
);
126 Capacity
: Count_Type
:= 0) return Set
129 Pre
=> Capacity
= 0 or else Capacity
>= Source
.Capacity
;
133 Position
: Cursor
) return Element_Type
136 Pre
=> Has_Element
(Container
, Position
);
138 procedure Replace_Element
139 (Container
: in out Set
;
141 New_Item
: Element_Type
)
144 Pre
=> Has_Element
(Container
, Position
);
146 procedure Move
(Target
: in out Set
; Source
: in out Set
) with
148 Pre
=> Target
.Capacity
>= Length
(Source
);
151 (Container
: in out Set
;
152 New_Item
: Element_Type
;
153 Position
: out Cursor
;
154 Inserted
: out Boolean)
157 Pre
=> Length
(Container
) < Container
.Capacity
;
159 procedure Insert
(Container
: in out Set
; New_Item
: Element_Type
) with
161 Pre
=> Length
(Container
) < Container
.Capacity
162 and then (not Contains
(Container
, New_Item
));
164 procedure Include
(Container
: in out Set
; New_Item
: Element_Type
) with
166 Pre
=> Length
(Container
) < Container
.Capacity
;
168 procedure Replace
(Container
: in out Set
; New_Item
: Element_Type
) with
170 Pre
=> Contains
(Container
, New_Item
);
172 procedure Exclude
(Container
: in out Set
; Item
: Element_Type
) with
175 procedure Delete
(Container
: in out Set
; Item
: Element_Type
) with
177 Pre
=> Contains
(Container
, Item
);
179 procedure Delete
(Container
: in out Set
; Position
: in out Cursor
) with
181 Pre
=> Has_Element
(Container
, Position
);
183 procedure Union
(Target
: in out Set
; Source
: Set
) with
185 Pre
=> Length
(Target
) + Length
(Source
) -
186 Length
(Intersection
(Target
, Source
)) <= Target
.Capacity
;
188 function Union
(Left
, Right
: Set
) return Set
with
190 Pre
=> Length
(Left
) + Length
(Right
) -
191 Length
(Intersection
(Left
, Right
)) <= Count_Type
'Last;
193 function "or" (Left
, Right
: Set
) return Set
renames Union
;
195 procedure Intersection
(Target
: in out Set
; Source
: Set
) with
198 function Intersection
(Left
, Right
: Set
) return Set
with
201 function "and" (Left
, Right
: Set
) return Set
renames Intersection
;
203 procedure Difference
(Target
: in out Set
; Source
: Set
) with
206 function Difference
(Left
, Right
: Set
) return Set
with
209 function "-" (Left
, Right
: Set
) return Set
renames Difference
;
211 procedure Symmetric_Difference
(Target
: in out Set
; Source
: Set
) with
213 Pre
=> Length
(Target
) + Length
(Source
) -
214 2 * Length
(Intersection
(Target
, Source
)) <= Target
.Capacity
;
216 function Symmetric_Difference
(Left
, Right
: Set
) return Set
with
218 Pre
=> Length
(Left
) + Length
(Right
) -
219 2 * Length
(Intersection
(Left
, Right
)) <= Count_Type
'Last;
221 function "xor" (Left
, Right
: Set
) return Set
222 renames Symmetric_Difference
;
224 function Overlap
(Left
, Right
: Set
) return Boolean with
227 function Is_Subset
(Subset
: Set
; Of_Set
: Set
) return Boolean with
230 function First
(Container
: Set
) return Cursor
with
233 function Next
(Container
: Set
; Position
: Cursor
) return Cursor
with
235 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
237 procedure Next
(Container
: Set
; Position
: in out Cursor
) with
239 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
243 Item
: Element_Type
) return Cursor
247 function Contains
(Container
: Set
; Item
: Element_Type
) return Boolean with
250 function Has_Element
(Container
: Set
; Position
: Cursor
) return Boolean
254 function Equivalent_Elements
(Left
: Set
; CLeft
: Cursor
;
255 Right
: Set
; CRight
: Cursor
) return Boolean
259 function Equivalent_Elements
260 (Left
: Set
; CLeft
: Cursor
;
261 Right
: Element_Type
) return Boolean
265 function Equivalent_Elements
266 (Left
: Element_Type
;
267 Right
: Set
; CRight
: Cursor
) return Boolean
271 function Default_Modulus
(Capacity
: Count_Type
) return Hash_Type
with
275 type Key_Type
(<>) is private;
277 with function Key
(Element
: Element_Type
) return Key_Type
;
279 with function Hash
(Key
: Key_Type
) return Hash_Type
;
281 with function Equivalent_Keys
(Left
, Right
: Key_Type
) return Boolean;
283 package Generic_Keys
with SPARK_Mode
is
285 function Key
(Container
: Set
; Position
: Cursor
) return Key_Type
with
288 function Element
(Container
: Set
; Key
: Key_Type
) return Element_Type
293 (Container
: in out Set
;
295 New_Item
: Element_Type
)
299 procedure Exclude
(Container
: in out Set
; Key
: Key_Type
) with
302 procedure Delete
(Container
: in out Set
; Key
: Key_Type
) with
305 function Find
(Container
: Set
; Key
: Key_Type
) return Cursor
with
308 function Contains
(Container
: Set
; Key
: Key_Type
) return Boolean with
313 function Strict_Equal
(Left
, Right
: Set
) return Boolean with
316 -- Strict_Equal returns True if the containers are physically equal, i.e.
317 -- they are structurally equal (function "=" returns True) and that they
318 -- have the same set of cursors.
320 function First_To_Previous
(Container
: Set
; Current
: Cursor
) return Set
324 Pre
=> Has_Element
(Container
, Current
) or else Current
= No_Element
;
326 function Current_To_Last
(Container
: Set
; Current
: Cursor
) return Set
330 Pre
=> Has_Element
(Container
, Current
) or else Current
= No_Element
;
331 -- First_To_Previous returns a container containing all elements preceding
332 -- Current (excluded) in Container. Current_To_Last returns a container
333 -- containing all elements following Current (included) in Container.
334 -- These two new functions can be used to express invariant properties in
335 -- loops which iterate over containers. First_To_Previous returns the part
336 -- of the container already scanned and Current_To_Last the part not
340 pragma SPARK_Mode
(Off
);
342 pragma Inline
(Next
);
346 Element
: Element_Type
;
348 Has_Element
: Boolean := False;
351 package HT_Types
is new
352 Ada
.Containers
.Hash_Tables
.Generic_Bounded_Hash_Table_Types
(Node_Type
);
354 type Set
(Capacity
: Count_Type
; Modulus
: Hash_Type
) is
355 new HT_Types
.Hash_Table_Type
(Capacity
, Modulus
) with null record;
359 type Cursor
is record
363 No_Element
: constant Cursor
:= (Node
=> 0);
365 Empty_Set
: constant Set
:= (Capacity
=> 0, Modulus
=> 0, others => <>);
367 end Ada
.Containers
.Formal_Hashed_Sets
;