File : a-cfdlli.ads
1 ------------------------------------------------------------------------------
2 -- --
3 -- GNAT LIBRARY COMPONENTS --
4 -- --
5 -- ADA.CONTAINERS.FORMAL_DOUBLY_LINKED_LISTS --
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 Ada.Containers.Bounded_Doubly_Linked_Lists 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: Next, Previous, Query_Element, Has_Element,
42 -- Iterate, Reverse_Iterate, Element. This change is motivated by the need
43 -- 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.
47
48 -- There are three new functions:
49
50 -- function Strict_Equal (Left, Right : List) return Boolean;
51 -- function First_To_Previous (Container : List; Current : Cursor)
52 -- return List;
53 -- function Current_To_Last (Container : List; Current : Cursor)
54 -- return List;
55
56 -- See subprogram specifications that follow for details
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 with
65 Pure,
66 SPARK_Mode
67 is
68 pragma Annotate (GNATprove, External_Axiomatization);
69 pragma Annotate (CodePeer, Skip_Analysis);
70
71 type List (Capacity : Count_Type) is private with
72 Iterable => (First => First,
73 Next => Next,
74 Has_Element => Has_Element,
75 Element => Element),
76 Default_Initial_Condition => Is_Empty (List);
77 pragma Preelaborable_Initialization (List);
78
79 type Cursor is private;
80 pragma Preelaborable_Initialization (Cursor);
81
82 Empty_List : constant List;
83
84 No_Element : constant Cursor;
85
86 function "=" (Left, Right : List) return Boolean with
87 Global => null;
88
89 function Length (Container : List) return Count_Type with
90 Global => null;
91
92 function Is_Empty (Container : List) return Boolean with
93 Global => null;
94
95 procedure Clear (Container : in out List) with
96 Global => null;
97
98 procedure Assign (Target : in out List; Source : List) with
99 Global => null,
100 Pre => Target.Capacity >= Length (Source);
101
102 function Copy (Source : List; Capacity : Count_Type := 0) return List with
103 Global => null,
104 Pre => Capacity = 0 or else Capacity >= Source.Capacity;
105
106 function Element
107 (Container : List;
108 Position : Cursor) return Element_Type
109 with
110 Global => null,
111 Pre => Has_Element (Container, Position);
112
113 procedure Replace_Element
114 (Container : in out List;
115 Position : Cursor;
116 New_Item : Element_Type)
117 with
118 Global => null,
119 Pre => Has_Element (Container, Position);
120
121 procedure Move (Target : in out List; Source : in out List) with
122 Global => null,
123 Pre => Target.Capacity >= Length (Source);
124
125 procedure Insert
126 (Container : in out List;
127 Before : Cursor;
128 New_Item : Element_Type;
129 Count : Count_Type := 1)
130 with
131 Global => null,
132 Pre => Length (Container) + Count <= Container.Capacity
133 and then (Has_Element (Container, Before)
134 or else Before = No_Element);
135
136 procedure Insert
137 (Container : in out List;
138 Before : Cursor;
139 New_Item : Element_Type;
140 Position : out Cursor;
141 Count : Count_Type := 1)
142 with
143 Global => null,
144 Pre => Length (Container) + Count <= Container.Capacity
145 and then (Has_Element (Container, Before)
146 or else Before = No_Element);
147
148 procedure Insert
149 (Container : in out List;
150 Before : Cursor;
151 Position : out Cursor;
152 Count : Count_Type := 1)
153 with
154 Global => null,
155 Pre => Length (Container) + Count <= Container.Capacity
156 and then (Has_Element (Container, Before)
157 or else Before = No_Element);
158
159 procedure Prepend
160 (Container : in out List;
161 New_Item : Element_Type;
162 Count : Count_Type := 1)
163 with
164 Global => null,
165 Pre => Length (Container) + Count <= Container.Capacity;
166
167 procedure Append
168 (Container : in out List;
169 New_Item : Element_Type;
170 Count : Count_Type := 1)
171 with
172 Global => null,
173 Pre => Length (Container) + Count <= Container.Capacity;
174
175 procedure Delete
176 (Container : in out List;
177 Position : in out Cursor;
178 Count : Count_Type := 1)
179 with
180 Global => null,
181 Pre => Has_Element (Container, Position);
182
183 procedure Delete_First
184 (Container : in out List;
185 Count : Count_Type := 1)
186 with
187 Global => null;
188
189 procedure Delete_Last
190 (Container : in out List;
191 Count : Count_Type := 1)
192 with
193 Global => null;
194
195 procedure Reverse_Elements (Container : in out List) with
196 Global => null;
197
198 procedure Swap
199 (Container : in out List;
200 I, J : Cursor)
201 with
202 Global => null,
203 Pre => Has_Element (Container, I) and then Has_Element (Container, J);
204
205 procedure Swap_Links
206 (Container : in out List;
207 I, J : Cursor)
208 with
209 Global => null,
210 Pre => Has_Element (Container, I) and then Has_Element (Container, J);
211
212 procedure Splice
213 (Target : in out List;
214 Before : Cursor;
215 Source : in out List)
216 with
217 Global => null,
218 Pre => Length (Source) + Length (Target) <= Target.Capacity
219 and then (Has_Element (Target, Before)
220 or else Before = No_Element);
221
222 procedure Splice
223 (Target : in out List;
224 Before : Cursor;
225 Source : in out List;
226 Position : in out Cursor)
227 with
228 Global => null,
229 Pre => Length (Source) + Length (Target) <= Target.Capacity
230 and then (Has_Element (Target, Before)
231 or else Before = No_Element)
232 and then Has_Element (Source, Position);
233
234 procedure Splice
235 (Container : in out List;
236 Before : Cursor;
237 Position : Cursor)
238 with
239 Global => null,
240 Pre => 2 * Length (Container) <= Container.Capacity
241 and then (Has_Element (Container, Before)
242 or else Before = No_Element)
243 and then Has_Element (Container, Position);
244
245 function First (Container : List) return Cursor with
246 Global => null;
247
248 function First_Element (Container : List) return Element_Type with
249 Global => null,
250 Pre => not Is_Empty (Container);
251
252 function Last (Container : List) return Cursor with
253 Global => null;
254
255 function Last_Element (Container : List) return Element_Type with
256 Global => null,
257 Pre => not Is_Empty (Container);
258
259 function Next (Container : List; Position : Cursor) return Cursor with
260 Global => null,
261 Pre => Has_Element (Container, Position) or else Position = No_Element;
262
263 procedure Next (Container : List; Position : in out Cursor) with
264 Global => null,
265 Pre => Has_Element (Container, Position) or else Position = No_Element;
266
267 function Previous (Container : List; Position : Cursor) return Cursor with
268 Global => null,
269 Pre => Has_Element (Container, Position) or else Position = No_Element;
270
271 procedure Previous (Container : List; Position : in out Cursor) with
272 Global => null,
273 Pre => Has_Element (Container, Position) or else Position = No_Element;
274
275 function Find
276 (Container : List;
277 Item : Element_Type;
278 Position : Cursor := No_Element) return Cursor
279 with
280 Global => null,
281 Pre => Has_Element (Container, Position) or else Position = No_Element;
282
283 function Reverse_Find
284 (Container : List;
285 Item : Element_Type;
286 Position : Cursor := No_Element) return Cursor
287 with
288 Global => null,
289 Pre => Has_Element (Container, Position) or else Position = No_Element;
290
291 function Contains
292 (Container : List;
293 Item : Element_Type) return Boolean
294 with
295 Global => null;
296
297 function Has_Element (Container : List; Position : Cursor) return Boolean
298 with
299 Global => null;
300
301 generic
302 with function "<" (Left, Right : Element_Type) return Boolean is <>;
303 package Generic_Sorting with SPARK_Mode is
304
305 function Is_Sorted (Container : List) return Boolean with
306 Global => null;
307
308 procedure Sort (Container : in out List) with
309 Global => null;
310
311 procedure Merge (Target, Source : in out List) with
312 Global => null;
313
314 end Generic_Sorting;
315
316 function Strict_Equal (Left, Right : List) return Boolean with
317 Ghost,
318 Global => null;
319 -- Strict_Equal returns True if the containers are physically equal, i.e.
320 -- they are structurally equal (function "=" returns True) and that they
321 -- have the same set of cursors.
322
323 function First_To_Previous (Container : List; Current : Cursor) return List
324 with
325 Ghost,
326 Global => null,
327 Pre => Has_Element (Container, Current) or else Current = No_Element;
328
329 function Current_To_Last (Container : List; Current : Cursor) return List
330 with
331 Ghost,
332 Global => null,
333 Pre => Has_Element (Container, Current) or else Current = No_Element;
334 -- First_To_Previous returns a container containing all elements preceding
335 -- Current (excluded) in Container. Current_To_Last returns a container
336 -- containing all elements following Current (included) in Container.
337 -- These two new functions can be used to express invariant properties in
338 -- loops which iterate over containers. First_To_Previous returns the part
339 -- of the container already scanned and Current_To_Last the part not
340 -- scanned yet.
341
342 private
343 pragma SPARK_Mode (Off);
344
345 type Node_Type is record
346 Prev : Count_Type'Base := -1;
347 Next : Count_Type;
348 Element : Element_Type;
349 end record;
350
351 function "=" (L, R : Node_Type) return Boolean is abstract;
352
353 type Node_Array is array (Count_Type range <>) of Node_Type;
354 function "=" (L, R : Node_Array) return Boolean is abstract;
355
356 type List (Capacity : Count_Type) is record
357 Free : Count_Type'Base := -1;
358 Length : Count_Type := 0;
359 First : Count_Type := 0;
360 Last : Count_Type := 0;
361 Nodes : Node_Array (1 .. Capacity) := (others => <>);
362 end record;
363
364 type Cursor is record
365 Node : Count_Type := 0;
366 end record;
367
368 Empty_List : constant List := (0, others => <>);
369
370 No_Element : constant Cursor := (Node => 0);
371
372 end Ada.Containers.Formal_Doubly_Linked_Lists;