]>
Commit | Line | Data |
---|---|---|
bd65a2d7 AC |
1 | ------------------------------------------------------------------------------ |
2 | -- -- | |
3 | -- GNAT LIBRARY COMPONENTS -- | |
4 | -- -- | |
5 | -- ADA.CONTAINERS.FORMAL_DOUBLY_LINKED_LISTS -- | |
6 | -- -- | |
7 | -- S p e c -- | |
8 | -- -- | |
e2441021 | 9 | -- Copyright (C) 2004-2013, Free Software Foundation, Inc. -- |
bd65a2d7 AC |
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 | -- 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. -- | |
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 | ||
d11cfaf8 RD |
32 | -- This spec is derived from Ada.Containers.Bounded_Doubly_Linked_Lists in the |
33 | -- Ada 2012 RM. The modifications are to facilitate formal proofs by making it | |
34 | -- easier to express properties. | |
35 | ||
36 | -- The modifications are: | |
300b98bb AC |
37 | |
38 | -- A parameter for the container is added to every function reading the | |
d11cfaf8 RD |
39 | -- contents of a container: Next, Previous, Query_Element, Has_Element, |
40 | -- Iterate, Reverse_Iterate, Element. This change is motivated by the need | |
41 | -- to have cursors which are valid on different containers (typically a | |
42 | -- container C and its previous version C'Old) for expressing properties, | |
300b98bb AC |
43 | -- which is not possible if cursors encapsulate an access to the underlying |
44 | -- container. | |
45 | ||
83fa09c5 | 46 | -- There are three new functions: |
300b98bb | 47 | |
83fa09c5 | 48 | -- function Strict_Equal (Left, Right : List) return Boolean; |
300b98bb AC |
49 | -- function Left (Container : List; Position : Cursor) return List; |
50 | -- function Right (Container : List; Position : Cursor) return List; | |
51 | ||
e51537ff | 52 | -- See detailed specifications for these subprograms |
300b98bb | 53 | |
bd65a2d7 | 54 | private with Ada.Streams; |
e2441021 | 55 | private with Ada.Finalization; |
88115c2a | 56 | with Ada.Iterator_Interfaces; |
bd65a2d7 AC |
57 | |
58 | generic | |
59 | type Element_Type is private; | |
60 | ||
61 | with function "=" (Left, Right : Element_Type) | |
62 | return Boolean is <>; | |
63 | ||
64 | package Ada.Containers.Formal_Doubly_Linked_Lists is | |
65 | pragma Pure; | |
66 | ||
88115c2a AC |
67 | type List (Capacity : Count_Type) is tagged private with |
68 | Constant_Indexing => Constant_Reference, | |
69 | Default_Iterator => Iterate, | |
70 | Iterator_Element => Element_Type; | |
bd65a2d7 AC |
71 | -- pragma Preelaborable_Initialization (List); |
72 | ||
73 | type Cursor is private; | |
74 | pragma Preelaborable_Initialization (Cursor); | |
75 | ||
76 | Empty_List : constant List; | |
77 | ||
78 | No_Element : constant Cursor; | |
79 | ||
88115c2a AC |
80 | function Not_No_Element (Position : Cursor) return Boolean; |
81 | ||
82 | package List_Iterator_Interfaces is new | |
83 | Ada.Iterator_Interfaces (Cursor => Cursor, Has_Element => Not_No_Element); | |
84 | ||
85 | function Iterate (Container : List; Start : Cursor) | |
86 | return List_Iterator_Interfaces.Reversible_Iterator'Class; | |
87 | ||
88 | function Iterate (Container : List) | |
89 | return List_Iterator_Interfaces.Reversible_Iterator'Class; | |
90 | ||
bd65a2d7 AC |
91 | function "=" (Left, Right : List) return Boolean; |
92 | ||
93 | function Length (Container : List) return Count_Type; | |
94 | ||
95 | function Is_Empty (Container : List) return Boolean; | |
96 | ||
97 | procedure Clear (Container : in out List); | |
98 | ||
99 | procedure Assign (Target : in out List; Source : List); | |
100 | ||
101 | function Copy (Source : List; Capacity : Count_Type := 0) return List; | |
102 | ||
103 | function Element (Container : List; Position : Cursor) return Element_Type; | |
104 | ||
105 | procedure Replace_Element | |
106 | (Container : in out List; | |
107 | Position : Cursor; | |
108 | New_Item : Element_Type); | |
109 | ||
110 | procedure Query_Element | |
111 | (Container : List; Position : Cursor; | |
112 | Process : not null access procedure (Element : Element_Type)); | |
113 | ||
114 | procedure Update_Element | |
115 | (Container : in out List; | |
116 | Position : Cursor; | |
117 | Process : not null access procedure (Element : in out Element_Type)); | |
118 | ||
119 | procedure Move (Target : in out List; Source : in out List); | |
120 | ||
121 | procedure Insert | |
122 | (Container : in out List; | |
123 | Before : Cursor; | |
124 | New_Item : Element_Type; | |
125 | Count : Count_Type := 1); | |
126 | ||
127 | procedure Insert | |
128 | (Container : in out List; | |
129 | Before : Cursor; | |
130 | New_Item : Element_Type; | |
131 | Position : out Cursor; | |
132 | Count : Count_Type := 1); | |
133 | ||
134 | procedure Insert | |
135 | (Container : in out List; | |
136 | Before : Cursor; | |
137 | Position : out Cursor; | |
138 | Count : Count_Type := 1); | |
139 | ||
140 | procedure Prepend | |
141 | (Container : in out List; | |
142 | New_Item : Element_Type; | |
143 | Count : Count_Type := 1); | |
144 | ||
145 | procedure Append | |
146 | (Container : in out List; | |
147 | New_Item : Element_Type; | |
148 | Count : Count_Type := 1); | |
149 | ||
150 | procedure Delete | |
151 | (Container : in out List; | |
152 | Position : in out Cursor; | |
153 | Count : Count_Type := 1); | |
154 | ||
155 | procedure Delete_First | |
156 | (Container : in out List; | |
157 | Count : Count_Type := 1); | |
158 | ||
159 | procedure Delete_Last | |
160 | (Container : in out List; | |
161 | Count : Count_Type := 1); | |
162 | ||
163 | procedure Reverse_Elements (Container : in out List); | |
164 | ||
165 | procedure Swap | |
166 | (Container : in out List; | |
167 | I, J : Cursor); | |
168 | ||
169 | procedure Swap_Links | |
170 | (Container : in out List; | |
171 | I, J : Cursor); | |
172 | ||
173 | procedure Splice | |
174 | (Target : in out List; | |
175 | Before : Cursor; | |
176 | Source : in out List); | |
177 | ||
178 | procedure Splice | |
179 | (Target : in out List; | |
180 | Before : Cursor; | |
181 | Source : in out List; | |
182 | Position : in out Cursor); | |
183 | ||
184 | procedure Splice | |
185 | (Container : in out List; | |
186 | Before : Cursor; | |
187 | Position : Cursor); | |
188 | ||
189 | function First (Container : List) return Cursor; | |
190 | ||
191 | function First_Element (Container : List) return Element_Type; | |
192 | ||
193 | function Last (Container : List) return Cursor; | |
194 | ||
195 | function Last_Element (Container : List) return Element_Type; | |
196 | ||
197 | function Next (Container : List; Position : Cursor) return Cursor; | |
198 | ||
199 | procedure Next (Container : List; Position : in out Cursor); | |
200 | ||
201 | function Previous (Container : List; Position : Cursor) return Cursor; | |
202 | ||
203 | procedure Previous (Container : List; Position : in out Cursor); | |
204 | ||
205 | function Find | |
206 | (Container : List; | |
207 | Item : Element_Type; | |
208 | Position : Cursor := No_Element) return Cursor; | |
209 | ||
210 | function Reverse_Find | |
211 | (Container : List; | |
212 | Item : Element_Type; | |
213 | Position : Cursor := No_Element) return Cursor; | |
214 | ||
215 | function Contains | |
216 | (Container : List; | |
217 | Item : Element_Type) return Boolean; | |
218 | ||
219 | function Has_Element (Container : List; Position : Cursor) return Boolean; | |
220 | ||
221 | procedure Iterate | |
222 | (Container : List; | |
223 | Process : | |
224 | not null access procedure (Container : List; Position : Cursor)); | |
225 | ||
226 | procedure Reverse_Iterate | |
227 | (Container : List; | |
228 | Process : | |
229 | not null access procedure (Container : List; Position : Cursor)); | |
230 | ||
231 | generic | |
232 | with function "<" (Left, Right : Element_Type) return Boolean is <>; | |
233 | package Generic_Sorting is | |
234 | ||
235 | function Is_Sorted (Container : List) return Boolean; | |
236 | ||
237 | procedure Sort (Container : in out List); | |
238 | ||
239 | procedure Merge (Target, Source : in out List); | |
240 | ||
241 | end Generic_Sorting; | |
242 | ||
88115c2a AC |
243 | type Constant_Reference_Type |
244 | (Element : not null access constant Element_Type) is private | |
245 | with | |
246 | Implicit_Dereference => Element; | |
247 | ||
248 | function Constant_Reference | |
d781a615 AC |
249 | (Container : List; -- SHOULD BE ALIASED ??? |
250 | Position : Cursor) return Constant_Reference_Type; | |
88115c2a | 251 | |
bd65a2d7 | 252 | function Strict_Equal (Left, Right : List) return Boolean; |
e51537ff RD |
253 | -- Strict_Equal returns True if the containers are physically equal, i.e. |
254 | -- they are structurally equal (function "=" returns True) and that they | |
255 | -- have the same set of cursors. | |
bd65a2d7 | 256 | |
e51537ff | 257 | function Left (Container : List; Position : Cursor) return List; |
bd65a2d7 | 258 | function Right (Container : List; Position : Cursor) return List; |
e51537ff RD |
259 | -- Left returns a container containing all elements preceding Position |
260 | -- (excluded) in Container. Right returns a container containing all | |
261 | -- elements following Position (included) in Container. These two new | |
262 | -- functions can be used to express invariant properties in loops which | |
263 | -- iterate over containers. Left returns the part of the container already | |
264 | -- scanned and Right the part not scanned yet. | |
bd65a2d7 AC |
265 | |
266 | private | |
267 | ||
268 | type Node_Type is record | |
269 | Prev : Count_Type'Base := -1; | |
270 | Next : Count_Type; | |
88115c2a | 271 | Element : aliased Element_Type; |
bd65a2d7 | 272 | end record; |
88115c2a | 273 | |
bd65a2d7 AC |
274 | function "=" (L, R : Node_Type) return Boolean is abstract; |
275 | ||
276 | type Node_Array is array (Count_Type range <>) of Node_Type; | |
277 | function "=" (L, R : Node_Array) return Boolean is abstract; | |
278 | ||
686d0984 | 279 | type List (Capacity : Count_Type) is tagged record |
bd65a2d7 AC |
280 | Nodes : Node_Array (1 .. Capacity) := (others => <>); |
281 | Free : Count_Type'Base := -1; | |
282 | Busy : Natural := 0; | |
283 | Lock : Natural := 0; | |
bd65a2d7 AC |
284 | Length : Count_Type := 0; |
285 | First : Count_Type := 0; | |
286 | Last : Count_Type := 0; | |
bd65a2d7 AC |
287 | end record; |
288 | ||
289 | use Ada.Streams; | |
290 | ||
291 | procedure Read | |
292 | (Stream : not null access Root_Stream_Type'Class; | |
293 | Item : out List); | |
294 | ||
295 | for List'Read use Read; | |
296 | ||
297 | procedure Write | |
298 | (Stream : not null access Root_Stream_Type'Class; | |
299 | Item : List); | |
300 | ||
301 | for List'Write use Write; | |
302 | ||
88115c2a AC |
303 | type List_Access is access all List; |
304 | for List_Access'Storage_Size use 0; | |
305 | ||
d11cfaf8 RD |
306 | type Cursor is record |
307 | Node : Count_Type := 0; | |
308 | end record; | |
bd65a2d7 | 309 | |
473e20df AC |
310 | type Constant_Reference_Type |
311 | (Element : not null access constant Element_Type) is null record; | |
312 | ||
bd65a2d7 AC |
313 | procedure Read |
314 | (Stream : not null access Root_Stream_Type'Class; | |
315 | Item : out Cursor); | |
316 | ||
317 | for Cursor'Read use Read; | |
318 | ||
319 | procedure Write | |
320 | (Stream : not null access Root_Stream_Type'Class; | |
321 | Item : Cursor); | |
322 | ||
323 | for Cursor'Write use Write; | |
324 | ||
325 | Empty_List : constant List := (0, others => <>); | |
326 | ||
327 | No_Element : constant Cursor := (Node => 0); | |
328 | ||
e2441021 AC |
329 | use Ada.Finalization; |
330 | ||
331 | type Iterator is new Limited_Controlled and | |
332 | List_Iterator_Interfaces.Reversible_Iterator with | |
333 | record | |
334 | Container : List_Access; | |
335 | Node : Count_Type; | |
336 | end record; | |
337 | ||
338 | overriding procedure Finalize (Object : in out Iterator); | |
339 | ||
340 | overriding function First (Object : Iterator) return Cursor; | |
341 | overriding function Last (Object : Iterator) return Cursor; | |
342 | ||
343 | overriding function Next | |
344 | (Object : Iterator; | |
345 | Position : Cursor) return Cursor; | |
346 | ||
347 | overriding function Previous | |
348 | (Object : Iterator; | |
349 | Position : Cursor) return Cursor; | |
350 | ||
bd65a2d7 | 351 | end Ada.Containers.Formal_Doubly_Linked_Lists; |