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-2011, 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 to facilitate formal proofs by
34 -- making it easier to express properties.
36 -- The modifications are:
38 -- A parameter for the container is added to every function reading the
39 -- content of a container: Key, Element, Next, Query_Element, Previous,
40 -- Has_Element, Iterate, Reverse_Iterate. This change is motivated by the
41 -- need to have cursors which are valid on different containers (typically a
42 -- container C and its previous version C'Old) for expressing properties,
43 -- which is not possible if cursors encapsulate an access to the underlying
44 -- container. The operators "<" and ">" that could not be modified that way
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
.Red_Black_Trees
;
57 private with Ada
.Streams
;
60 type Key_Type
is private;
61 type Element_Type
is private;
63 with function "<" (Left
, Right
: Key_Type
) return Boolean is <>;
64 with function "=" (Left
, Right
: Element_Type
) return Boolean is <>;
66 package Ada
.Containers
.Formal_Ordered_Maps
is
69 function Equivalent_Keys
(Left
, Right
: Key_Type
) return Boolean;
71 type Map
(Capacity
: Count_Type
) is tagged private;
72 pragma Preelaborable_Initialization
(Map
);
74 type Cursor
is private;
75 pragma Preelaborable_Initialization
(Cursor
);
77 Empty_Map
: constant Map
;
79 No_Element
: constant Cursor
;
81 function "=" (Left
, Right
: Map
) return Boolean;
83 function Length
(Container
: Map
) return Count_Type
;
85 function Is_Empty
(Container
: Map
) return Boolean;
87 procedure Clear
(Container
: in out Map
);
89 procedure Assign
(Target
: in out Map
; Source
: Map
);
91 function Copy
(Source
: Map
; Capacity
: Count_Type
:= 0) return Map
;
93 function Key
(Container
: Map
; Position
: Cursor
) return Key_Type
;
95 function Element
(Container
: Map
; Position
: Cursor
) return Element_Type
;
97 procedure Replace_Element
98 (Container
: in out Map
;
100 New_Item
: Element_Type
);
102 procedure Query_Element
103 (Container
: in out Map
;
105 Process
: not null access
106 procedure (Key
: Key_Type
; Element
: Element_Type
));
108 procedure Update_Element
109 (Container
: in out Map
;
111 Process
: not null access
112 procedure (Key
: Key_Type
; Element
: in out Element_Type
));
114 procedure Move
(Target
: in out Map
; Source
: in out Map
);
117 (Container
: in out Map
;
119 New_Item
: Element_Type
;
120 Position
: out Cursor
;
121 Inserted
: out Boolean);
124 (Container
: in out Map
;
126 Position
: out Cursor
;
127 Inserted
: out Boolean);
130 (Container
: in out Map
;
132 New_Item
: Element_Type
);
135 (Container
: in out Map
;
137 New_Item
: Element_Type
);
140 (Container
: in out Map
;
142 New_Item
: Element_Type
);
144 procedure Exclude
(Container
: in out Map
; Key
: Key_Type
);
146 procedure Delete
(Container
: in out Map
; Key
: Key_Type
);
148 procedure Delete
(Container
: in out Map
; Position
: in out Cursor
);
150 procedure Delete_First
(Container
: in out Map
);
152 procedure Delete_Last
(Container
: in out Map
);
154 function First
(Container
: Map
) return Cursor
;
156 function First_Element
(Container
: Map
) return Element_Type
;
158 function First_Key
(Container
: Map
) return Key_Type
;
160 function Last
(Container
: Map
) return Cursor
;
162 function Last_Element
(Container
: Map
) return Element_Type
;
164 function Last_Key
(Container
: Map
) return Key_Type
;
166 function Next
(Container
: Map
; Position
: Cursor
) return Cursor
;
168 procedure Next
(Container
: Map
; Position
: in out Cursor
);
170 function Previous
(Container
: Map
; Position
: Cursor
) return Cursor
;
172 procedure Previous
(Container
: Map
; Position
: in out Cursor
);
174 function Find
(Container
: Map
; Key
: Key_Type
) return Cursor
;
176 function Element
(Container
: Map
; Key
: Key_Type
) return Element_Type
;
178 function Floor
(Container
: Map
; Key
: Key_Type
) return Cursor
;
180 function Ceiling
(Container
: Map
; Key
: Key_Type
) return Cursor
;
182 function Contains
(Container
: Map
; Key
: Key_Type
) return Boolean;
184 function Has_Element
(Container
: Map
; Position
: Cursor
) return Boolean;
189 not null access procedure (Container
: Map
; Position
: Cursor
));
191 procedure Reverse_Iterate
193 Process
: not null access
194 procedure (Container
: Map
; Position
: Cursor
));
196 function Strict_Equal
(Left
, Right
: Map
) return Boolean;
197 -- Strict_Equal returns True if the containers are physically equal, i.e.
198 -- they are structurally equal (function "=" returns True) and that they
199 -- have the same set of cursors.
201 function Left
(Container
: Map
; Position
: Cursor
) return Map
;
202 function Right
(Container
: Map
; Position
: Cursor
) return Map
;
203 -- Left returns a container containing all elements preceding Position
204 -- (excluded) in Container. Right returns a container containing all
205 -- elements following Position (included) in Container. These two new
206 -- functions can be used to express invariant properties in loops which
207 -- iterate over containers. Left returns the part of the container already
208 -- scanned and Right the part not scanned yet.
210 function Overlap
(Left
, Right
: Map
) return Boolean;
211 -- Overlap returns True if the containers have common keys
214 pragma Inline
(Next
);
215 pragma Inline
(Previous
);
217 subtype Node_Access
is Count_Type
;
221 type Node_Type
is record
222 Has_Element
: Boolean := False;
223 Parent
: Node_Access
:= 0;
224 Left
: Node_Access
:= 0;
225 Right
: Node_Access
:= 0;
226 Color
: Red_Black_Trees
.Color_Type
:= Red
;
228 Element
: Element_Type
;
231 package Tree_Types
is
232 new Ada
.Containers
.Red_Black_Trees
.Generic_Bounded_Tree_Types
(Node_Type
);
234 type Map
(Capacity
: Count_Type
) is
235 new Tree_Types
.Tree_Type
(Capacity
) with null record;
239 type Cursor
is record
244 (Stream
: not null access Root_Stream_Type
'Class;
247 for Cursor
'Write use Write
;
250 (Stream
: not null access Root_Stream_Type
'Class;
253 for Cursor
'Read use Read
;
255 No_Element
: constant Cursor
:= (Node
=> 0);
258 (Stream
: not null access Root_Stream_Type
'Class;
261 for Map
'Write use Write
;
264 (Stream
: not null access Root_Stream_Type
'Class;
265 Container
: out Map
);
267 for Map
'Read use Read
;
269 Empty_Map
: constant Map
:= (Capacity
=> 0, others => <>);
271 end Ada
.Containers
.Formal_Ordered_Maps
;