]>
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 | -- -- | |
203876fc | 9 | -- Copyright (C) 2004-2015, 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 | 32 | -- This spec is derived from Ada.Containers.Bounded_Doubly_Linked_Lists in the |
2fc07285 AC |
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. | |
d11cfaf8 RD |
37 | |
38 | -- The modifications are: | |
300b98bb AC |
39 | |
40 | -- A parameter for the container is added to every function reading the | |
d11cfaf8 RD |
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, | |
300b98bb AC |
45 | -- which is not possible if cursors encapsulate an access to the underlying |
46 | -- container. | |
47 | ||
83fa09c5 | 48 | -- There are three new functions: |
300b98bb | 49 | |
83fa09c5 | 50 | -- function Strict_Equal (Left, Right : List) return Boolean; |
c6d2191a AC |
51 | -- function First_To_Previous (Container : List; Current : Cursor) |
52 | -- return List; | |
53 | -- function Current_To_Last (Container : List; Current : Cursor) | |
54 | -- return List; | |
300b98bb | 55 | |
27a8f150 | 56 | -- See subprogram specifications that follow for details |
bd65a2d7 AC |
57 | |
58 | generic | |
59 | type Element_Type is private; | |
60 | ||
61 | with function "=" (Left, Right : Element_Type) | |
62 | return Boolean is <>; | |
63 | ||
5fde9688 AC |
64 | package Ada.Containers.Formal_Doubly_Linked_Lists with |
65 | Pure, | |
66 | SPARK_Mode | |
67 | is | |
36eef04a | 68 | pragma Annotate (GNATprove, External_Axiomatization); |
6031f544 | 69 | pragma Annotate (CodePeer, Skip_Analysis); |
bd65a2d7 | 70 | |
edbd98c4 AC |
71 | type List (Capacity : Count_Type) is private with |
72 | Iterable => (First => First, | |
73 | Next => Next, | |
74 | Has_Element => Has_Element, | |
9ceeaf9d | 75 | Element => Element), |
203876fc | 76 | Default_Initial_Condition => Is_Empty (List); |
9686dbc7 | 77 | pragma Preelaborable_Initialization (List); |
bd65a2d7 AC |
78 | |
79 | type Cursor is private; | |
80 | pragma Preelaborable_Initialization (Cursor); | |
81 | ||
82 | Empty_List : constant List; | |
83 | ||
84 | No_Element : constant Cursor; | |
85 | ||
47fb6ca8 AC |
86 | function "=" (Left, Right : List) return Boolean with |
87 | Global => null; | |
bd65a2d7 | 88 | |
47fb6ca8 AC |
89 | function Length (Container : List) return Count_Type with |
90 | Global => null; | |
bd65a2d7 | 91 | |
47fb6ca8 AC |
92 | function Is_Empty (Container : List) return Boolean with |
93 | Global => null; | |
bd65a2d7 | 94 | |
47fb6ca8 AC |
95 | procedure Clear (Container : in out List) with |
96 | Global => null; | |
bd65a2d7 | 97 | |
16788d44 | 98 | procedure Assign (Target : in out List; Source : List) with |
47fb6ca8 AC |
99 | Global => null, |
100 | Pre => Target.Capacity >= Length (Source); | |
bd65a2d7 | 101 | |
b1d12996 | 102 | function Copy (Source : List; Capacity : Count_Type := 0) return List with |
47fb6ca8 AC |
103 | Global => null, |
104 | Pre => Capacity = 0 or else Capacity >= Source.Capacity; | |
bd65a2d7 | 105 | |
16788d44 RD |
106 | function Element |
107 | (Container : List; | |
108 | Position : Cursor) return Element_Type | |
109 | with | |
47fb6ca8 AC |
110 | Global => null, |
111 | Pre => Has_Element (Container, Position); | |
bd65a2d7 AC |
112 | |
113 | procedure Replace_Element | |
114 | (Container : in out List; | |
115 | Position : Cursor; | |
67a90476 | 116 | New_Item : Element_Type) |
16788d44 | 117 | with |
47fb6ca8 AC |
118 | Global => null, |
119 | Pre => Has_Element (Container, Position); | |
bd65a2d7 | 120 | |
16788d44 | 121 | procedure Move (Target : in out List; Source : in out List) with |
47fb6ca8 AC |
122 | Global => null, |
123 | Pre => Target.Capacity >= Length (Source); | |
bd65a2d7 AC |
124 | |
125 | procedure Insert | |
126 | (Container : in out List; | |
127 | Before : Cursor; | |
128 | New_Item : Element_Type; | |
67a90476 | 129 | Count : Count_Type := 1) |
16788d44 | 130 | with |
47fb6ca8 AC |
131 | Global => null, |
132 | Pre => Length (Container) + Count <= Container.Capacity | |
133 | and then (Has_Element (Container, Before) | |
134 | or else Before = No_Element); | |
bd65a2d7 AC |
135 | |
136 | procedure Insert | |
137 | (Container : in out List; | |
138 | Before : Cursor; | |
139 | New_Item : Element_Type; | |
140 | Position : out Cursor; | |
67a90476 | 141 | Count : Count_Type := 1) |
16788d44 | 142 | with |
47fb6ca8 AC |
143 | Global => null, |
144 | Pre => Length (Container) + Count <= Container.Capacity | |
145 | and then (Has_Element (Container, Before) | |
146 | or else Before = No_Element); | |
bd65a2d7 AC |
147 | |
148 | procedure Insert | |
149 | (Container : in out List; | |
150 | Before : Cursor; | |
151 | Position : out Cursor; | |
67a90476 | 152 | Count : Count_Type := 1) |
16788d44 | 153 | with |
47fb6ca8 AC |
154 | Global => null, |
155 | Pre => Length (Container) + Count <= Container.Capacity | |
156 | and then (Has_Element (Container, Before) | |
157 | or else Before = No_Element); | |
bd65a2d7 AC |
158 | |
159 | procedure Prepend | |
160 | (Container : in out List; | |
161 | New_Item : Element_Type; | |
67a90476 | 162 | Count : Count_Type := 1) |
16788d44 | 163 | with |
47fb6ca8 AC |
164 | Global => null, |
165 | Pre => Length (Container) + Count <= Container.Capacity; | |
bd65a2d7 AC |
166 | |
167 | procedure Append | |
168 | (Container : in out List; | |
169 | New_Item : Element_Type; | |
67a90476 | 170 | Count : Count_Type := 1) |
16788d44 | 171 | with |
47fb6ca8 AC |
172 | Global => null, |
173 | Pre => Length (Container) + Count <= Container.Capacity; | |
bd65a2d7 AC |
174 | |
175 | procedure Delete | |
176 | (Container : in out List; | |
177 | Position : in out Cursor; | |
67a90476 | 178 | Count : Count_Type := 1) |
16788d44 | 179 | with |
47fb6ca8 AC |
180 | Global => null, |
181 | Pre => Has_Element (Container, Position); | |
bd65a2d7 AC |
182 | |
183 | procedure Delete_First | |
184 | (Container : in out List; | |
47fb6ca8 AC |
185 | Count : Count_Type := 1) |
186 | with | |
187 | Global => null; | |
bd65a2d7 AC |
188 | |
189 | procedure Delete_Last | |
190 | (Container : in out List; | |
47fb6ca8 AC |
191 | Count : Count_Type := 1) |
192 | with | |
193 | Global => null; | |
bd65a2d7 | 194 | |
47fb6ca8 AC |
195 | procedure Reverse_Elements (Container : in out List) with |
196 | Global => null; | |
bd65a2d7 AC |
197 | |
198 | procedure Swap | |
199 | (Container : in out List; | |
67a90476 | 200 | I, J : Cursor) |
16788d44 | 201 | with |
47fb6ca8 AC |
202 | Global => null, |
203 | Pre => Has_Element (Container, I) and then Has_Element (Container, J); | |
bd65a2d7 AC |
204 | |
205 | procedure Swap_Links | |
206 | (Container : in out List; | |
67a90476 | 207 | I, J : Cursor) |
16788d44 | 208 | with |
47fb6ca8 AC |
209 | Global => null, |
210 | Pre => Has_Element (Container, I) and then Has_Element (Container, J); | |
bd65a2d7 AC |
211 | |
212 | procedure Splice | |
213 | (Target : in out List; | |
214 | Before : Cursor; | |
67a90476 | 215 | Source : in out List) |
16788d44 | 216 | with |
47fb6ca8 AC |
217 | Global => null, |
218 | Pre => Length (Source) + Length (Target) <= Target.Capacity | |
219 | and then (Has_Element (Target, Before) | |
220 | or else Before = No_Element); | |
bd65a2d7 AC |
221 | |
222 | procedure Splice | |
223 | (Target : in out List; | |
224 | Before : Cursor; | |
225 | Source : in out List; | |
67a90476 | 226 | Position : in out Cursor) |
16788d44 | 227 | with |
47fb6ca8 AC |
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); | |
bd65a2d7 AC |
233 | |
234 | procedure Splice | |
235 | (Container : in out List; | |
236 | Before : Cursor; | |
67a90476 | 237 | Position : Cursor) |
16788d44 | 238 | with |
47fb6ca8 AC |
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); | |
bd65a2d7 | 244 | |
47fb6ca8 AC |
245 | function First (Container : List) return Cursor with |
246 | Global => null; | |
bd65a2d7 | 247 | |
16788d44 | 248 | function First_Element (Container : List) return Element_Type with |
47fb6ca8 AC |
249 | Global => null, |
250 | Pre => not Is_Empty (Container); | |
bd65a2d7 | 251 | |
47fb6ca8 AC |
252 | function Last (Container : List) return Cursor with |
253 | Global => null; | |
bd65a2d7 | 254 | |
16788d44 | 255 | function Last_Element (Container : List) return Element_Type with |
47fb6ca8 AC |
256 | Global => null, |
257 | Pre => not Is_Empty (Container); | |
bd65a2d7 | 258 | |
16788d44 | 259 | function Next (Container : List; Position : Cursor) return Cursor with |
47fb6ca8 AC |
260 | Global => null, |
261 | Pre => Has_Element (Container, Position) or else Position = No_Element; | |
bd65a2d7 | 262 | |
16788d44 | 263 | procedure Next (Container : List; Position : in out Cursor) with |
47fb6ca8 AC |
264 | Global => null, |
265 | Pre => Has_Element (Container, Position) or else Position = No_Element; | |
bd65a2d7 | 266 | |
16788d44 | 267 | function Previous (Container : List; Position : Cursor) return Cursor with |
47fb6ca8 AC |
268 | Global => null, |
269 | Pre => Has_Element (Container, Position) or else Position = No_Element; | |
bd65a2d7 | 270 | |
16788d44 | 271 | procedure Previous (Container : List; Position : in out Cursor) with |
47fb6ca8 AC |
272 | Global => null, |
273 | Pre => Has_Element (Container, Position) or else Position = No_Element; | |
bd65a2d7 AC |
274 | |
275 | function Find | |
276 | (Container : List; | |
277 | Item : Element_Type; | |
67a90476 | 278 | Position : Cursor := No_Element) return Cursor |
16788d44 | 279 | with |
47fb6ca8 AC |
280 | Global => null, |
281 | Pre => Has_Element (Container, Position) or else Position = No_Element; | |
bd65a2d7 AC |
282 | |
283 | function Reverse_Find | |
284 | (Container : List; | |
285 | Item : Element_Type; | |
67a90476 | 286 | Position : Cursor := No_Element) return Cursor |
16788d44 | 287 | with |
47fb6ca8 AC |
288 | Global => null, |
289 | Pre => Has_Element (Container, Position) or else Position = No_Element; | |
bd65a2d7 AC |
290 | |
291 | function Contains | |
292 | (Container : List; | |
47fb6ca8 AC |
293 | Item : Element_Type) return Boolean |
294 | with | |
295 | Global => null; | |
bd65a2d7 | 296 | |
47fb6ca8 AC |
297 | function Has_Element (Container : List; Position : Cursor) return Boolean |
298 | with | |
299 | Global => null; | |
bd65a2d7 | 300 | |
bd65a2d7 AC |
301 | generic |
302 | with function "<" (Left, Right : Element_Type) return Boolean is <>; | |
c96c518f | 303 | package Generic_Sorting with SPARK_Mode is |
bd65a2d7 | 304 | |
47fb6ca8 AC |
305 | function Is_Sorted (Container : List) return Boolean with |
306 | Global => null; | |
bd65a2d7 | 307 | |
47fb6ca8 AC |
308 | procedure Sort (Container : in out List) with |
309 | Global => null; | |
bd65a2d7 | 310 | |
47fb6ca8 AC |
311 | procedure Merge (Target, Source : in out List) with |
312 | Global => null; | |
bd65a2d7 AC |
313 | |
314 | end Generic_Sorting; | |
315 | ||
47fb6ca8 | 316 | function Strict_Equal (Left, Right : List) return Boolean with |
8ad1c2df | 317 | Ghost, |
47fb6ca8 | 318 | Global => null; |
e51537ff RD |
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. | |
bd65a2d7 | 322 | |
c6d2191a AC |
323 | function First_To_Previous (Container : List; Current : Cursor) return List |
324 | with | |
8ad1c2df | 325 | Ghost, |
47fb6ca8 | 326 | Global => null, |
c6d2191a | 327 | Pre => Has_Element (Container, Current) or else Current = No_Element; |
8ad1c2df | 328 | |
c6d2191a AC |
329 | function Current_To_Last (Container : List; Current : Cursor) return List |
330 | with | |
8ad1c2df | 331 | Ghost, |
47fb6ca8 | 332 | Global => null, |
c6d2191a AC |
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. | |
bd65a2d7 AC |
341 | |
342 | private | |
5fde9688 | 343 | pragma SPARK_Mode (Off); |
bd65a2d7 AC |
344 | |
345 | type Node_Type is record | |
346 | Prev : Count_Type'Base := -1; | |
347 | Next : Count_Type; | |
9686dbc7 | 348 | Element : Element_Type; |
bd65a2d7 | 349 | end record; |
88115c2a | 350 | |
bd65a2d7 AC |
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 | ||
0f8b3e5d | 356 | type List (Capacity : Count_Type) is record |
bd65a2d7 | 357 | Free : Count_Type'Base := -1; |
bd65a2d7 AC |
358 | Length : Count_Type := 0; |
359 | First : Count_Type := 0; | |
360 | Last : Count_Type := 0; | |
0f8b3e5d | 361 | Nodes : Node_Array (1 .. Capacity) := (others => <>); |
bd65a2d7 AC |
362 | end record; |
363 | ||
d11cfaf8 RD |
364 | type Cursor is record |
365 | Node : Count_Type := 0; | |
366 | end record; | |
bd65a2d7 | 367 | |
bd65a2d7 AC |
368 | Empty_List : constant List := (0, others => <>); |
369 | ||
370 | No_Element : constant Cursor := (Node => 0); | |
371 | ||
372 | end Ada.Containers.Formal_Doubly_Linked_Lists; |