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-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_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 -- There are four new functions:
51 -- function Strict_Equal (Left, Right : Map) return Boolean;
52 -- function Overlap (Left, Right : Map) return Boolean;
53 -- function First_To_Previous (Container : Map; Current : Cursor)
55 -- function Current_To_Last (Container : Map; Current : Cursor)
58 -- See detailed specifications for these subprograms
60 private with Ada
.Containers
.Red_Black_Trees
;
63 type Key_Type
is private;
64 type Element_Type
is private;
66 with function "<" (Left
, Right
: Key_Type
) return Boolean is <>;
67 with function "=" (Left
, Right
: Element_Type
) return Boolean is <>;
69 package Ada
.Containers
.Formal_Ordered_Maps
is
70 pragma Annotate
(GNATprove
, External_Axiomatization
);
73 function Equivalent_Keys
(Left
, Right
: Key_Type
) return Boolean with
76 type Map
(Capacity
: Count_Type
) is private with
77 Iterable
=> (First
=> First
,
79 Has_Element
=> Has_Element
,
81 pragma Preelaborable_Initialization
(Map
);
83 type Cursor
is private;
84 pragma Preelaborable_Initialization
(Cursor
);
86 Empty_Map
: constant Map
;
88 No_Element
: constant Cursor
;
90 function "=" (Left
, Right
: Map
) return Boolean with
93 function Length
(Container
: Map
) return Count_Type
with
96 function Is_Empty
(Container
: Map
) return Boolean with
99 procedure Clear
(Container
: in out Map
) with
102 procedure Assign
(Target
: in out Map
; Source
: Map
) with
104 Pre
=> Target
.Capacity
>= Length
(Source
);
106 function Copy
(Source
: Map
; Capacity
: Count_Type
:= 0) return Map
with
108 Pre
=> Capacity
= 0 or else Capacity
>= Source
.Capacity
;
110 function Key
(Container
: Map
; Position
: Cursor
) return Key_Type
with
112 Pre
=> Has_Element
(Container
, Position
);
116 Position
: Cursor
) return Element_Type
119 Pre
=> Has_Element
(Container
, Position
);
121 procedure Replace_Element
122 (Container
: in out Map
;
124 New_Item
: Element_Type
)
127 Pre
=> Has_Element
(Container
, Position
);
129 procedure Move
(Target
: in out Map
; Source
: in out Map
) with
131 Pre
=> Target
.Capacity
>= Length
(Source
);
134 (Container
: in out Map
;
136 New_Item
: Element_Type
;
137 Position
: out Cursor
;
138 Inserted
: out Boolean)
141 Pre
=> Length
(Container
) < Container
.Capacity
;
144 (Container
: in out Map
;
146 New_Item
: Element_Type
)
149 Pre
=> Length
(Container
) < Container
.Capacity
150 and then (not Contains
(Container
, Key
));
153 (Container
: in out Map
;
155 New_Item
: Element_Type
)
158 Pre
=> Length
(Container
) < Container
.Capacity
;
161 (Container
: in out Map
;
163 New_Item
: Element_Type
)
166 Pre
=> Contains
(Container
, Key
);
168 procedure Exclude
(Container
: in out Map
; Key
: Key_Type
) with
171 procedure Delete
(Container
: in out Map
; Key
: Key_Type
) with
173 Pre
=> Contains
(Container
, Key
);
175 procedure Delete
(Container
: in out Map
; Position
: in out Cursor
) with
177 Pre
=> Has_Element
(Container
, Position
);
179 procedure Delete_First
(Container
: in out Map
) with
182 procedure Delete_Last
(Container
: in out Map
) with
185 function First
(Container
: Map
) return Cursor
with
188 function First_Element
(Container
: Map
) return Element_Type
with
190 Pre
=> not Is_Empty
(Container
);
192 function First_Key
(Container
: Map
) return Key_Type
with
194 Pre
=> not Is_Empty
(Container
);
196 function Last
(Container
: Map
) return Cursor
with
199 function Last_Element
(Container
: Map
) return Element_Type
with
201 Pre
=> not Is_Empty
(Container
);
203 function Last_Key
(Container
: Map
) return Key_Type
with
205 Pre
=> not Is_Empty
(Container
);
207 function Next
(Container
: Map
; Position
: Cursor
) return Cursor
with
209 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
211 procedure Next
(Container
: Map
; Position
: in out Cursor
) with
213 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
215 function Previous
(Container
: Map
; Position
: Cursor
) return Cursor
with
217 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
219 procedure Previous
(Container
: Map
; Position
: in out Cursor
) with
221 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
223 function Find
(Container
: Map
; Key
: Key_Type
) return Cursor
with
226 function Element
(Container
: Map
; Key
: Key_Type
) return Element_Type
with
228 Pre
=> Contains
(Container
, Key
);
230 function Floor
(Container
: Map
; Key
: Key_Type
) return Cursor
with
233 function Ceiling
(Container
: Map
; Key
: Key_Type
) return Cursor
with
236 function Contains
(Container
: Map
; Key
: Key_Type
) return Boolean with
239 function Has_Element
(Container
: Map
; Position
: Cursor
) return Boolean
243 function Strict_Equal
(Left
, Right
: Map
) return Boolean with
245 -- Strict_Equal returns True if the containers are physically equal, i.e.
246 -- they are structurally equal (function "=" returns True) and that they
247 -- have the same set of cursors.
249 function First_To_Previous
(Container
: Map
; Current
: Cursor
) return Map
252 Pre
=> Has_Element
(Container
, Current
) or else Current
= No_Element
;
253 function Current_To_Last
(Container
: Map
; Current
: Cursor
) return Map
256 Pre
=> Has_Element
(Container
, Current
) or else Current
= No_Element
;
257 -- First_To_Previous returns a container containing all elements preceding
258 -- Current (excluded) in Container. Current_To_Last returns a container
259 -- containing all elements following Current (included) in Container.
260 -- These two new functions can be used to express invariant properties in
261 -- loops which iterate over containers. First_To_Previous returns the part
262 -- of the container already scanned and Current_To_Last the part not
265 function Overlap
(Left
, Right
: Map
) return Boolean with
267 -- Overlap returns True if the containers have common keys
270 pragma Inline
(Next
);
271 pragma Inline
(Previous
);
273 subtype Node_Access
is Count_Type
;
277 type Node_Type
is record
278 Has_Element
: Boolean := False;
279 Parent
: Node_Access
:= 0;
280 Left
: Node_Access
:= 0;
281 Right
: Node_Access
:= 0;
282 Color
: Red_Black_Trees
.Color_Type
:= Red
;
284 Element
: Element_Type
;
287 package Tree_Types
is
288 new Ada
.Containers
.Red_Black_Trees
.Generic_Bounded_Tree_Types
(Node_Type
);
290 type Map
(Capacity
: Count_Type
) is
291 new Tree_Types
.Tree_Type
(Capacity
) with null record;
293 type Cursor
is record
297 Empty_Map
: constant Map
:= (Capacity
=> 0, others => <>);
299 No_Element
: constant Cursor
:= (Node
=> 0);
301 end Ada
.Containers
.Formal_Ordered_Maps
;