1 ------------------------------------------------------------------------------
3 -- GNAT LIBRARY COMPONENTS --
5 -- ADA.CONTAINERS.FORMAL_DOUBLY_LINKED_LISTS --
9 -- Copyright (C) 2004-2015, 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 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.
38 -- The modifications are:
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
48 -- There are three new functions:
50 -- function Strict_Equal (Left, Right : List) return Boolean;
51 -- function First_To_Previous (Container : List; Current : Cursor)
53 -- function Current_To_Last (Container : List; Current : Cursor)
56 -- See subprogram specifications that follow for details
59 type Element_Type
is private;
61 with function "=" (Left
, Right
: Element_Type
)
64 package Ada
.Containers
.Formal_Doubly_Linked_Lists
with
68 pragma Annotate
(GNATprove
, External_Axiomatization
);
69 pragma Annotate
(CodePeer
, Skip_Analysis
);
71 type List
(Capacity
: Count_Type
) is private with
72 Iterable
=> (First
=> First
,
74 Has_Element
=> Has_Element
,
76 Default_Initial_Condition
=> Is_Empty
(List
);
77 pragma Preelaborable_Initialization
(List
);
79 type Cursor
is private;
80 pragma Preelaborable_Initialization
(Cursor
);
82 Empty_List
: constant List
;
84 No_Element
: constant Cursor
;
86 function "=" (Left
, Right
: List
) return Boolean with
89 function Length
(Container
: List
) return Count_Type
with
92 function Is_Empty
(Container
: List
) return Boolean with
95 procedure Clear
(Container
: in out List
) with
98 procedure Assign
(Target
: in out List
; Source
: List
) with
100 Pre
=> Target
.Capacity
>= Length
(Source
);
102 function Copy
(Source
: List
; Capacity
: Count_Type
:= 0) return List
with
104 Pre
=> Capacity
= 0 or else Capacity
>= Source
.Capacity
;
108 Position
: Cursor
) return Element_Type
111 Pre
=> Has_Element
(Container
, Position
);
113 procedure Replace_Element
114 (Container
: in out List
;
116 New_Item
: Element_Type
)
119 Pre
=> Has_Element
(Container
, Position
);
121 procedure Move
(Target
: in out List
; Source
: in out List
) with
123 Pre
=> Target
.Capacity
>= Length
(Source
);
126 (Container
: in out List
;
128 New_Item
: Element_Type
;
129 Count
: Count_Type
:= 1)
132 Pre
=> Length
(Container
) + Count
<= Container
.Capacity
133 and then (Has_Element
(Container
, Before
)
134 or else Before
= No_Element
);
137 (Container
: in out List
;
139 New_Item
: Element_Type
;
140 Position
: out Cursor
;
141 Count
: Count_Type
:= 1)
144 Pre
=> Length
(Container
) + Count
<= Container
.Capacity
145 and then (Has_Element
(Container
, Before
)
146 or else Before
= No_Element
);
149 (Container
: in out List
;
151 Position
: out Cursor
;
152 Count
: Count_Type
:= 1)
155 Pre
=> Length
(Container
) + Count
<= Container
.Capacity
156 and then (Has_Element
(Container
, Before
)
157 or else Before
= No_Element
);
160 (Container
: in out List
;
161 New_Item
: Element_Type
;
162 Count
: Count_Type
:= 1)
165 Pre
=> Length
(Container
) + Count
<= Container
.Capacity
;
168 (Container
: in out List
;
169 New_Item
: Element_Type
;
170 Count
: Count_Type
:= 1)
173 Pre
=> Length
(Container
) + Count
<= Container
.Capacity
;
176 (Container
: in out List
;
177 Position
: in out Cursor
;
178 Count
: Count_Type
:= 1)
181 Pre
=> Has_Element
(Container
, Position
);
183 procedure Delete_First
184 (Container
: in out List
;
185 Count
: Count_Type
:= 1)
189 procedure Delete_Last
190 (Container
: in out List
;
191 Count
: Count_Type
:= 1)
195 procedure Reverse_Elements
(Container
: in out List
) with
199 (Container
: in out List
;
203 Pre
=> Has_Element
(Container
, I
) and then Has_Element
(Container
, J
);
206 (Container
: in out List
;
210 Pre
=> Has_Element
(Container
, I
) and then Has_Element
(Container
, J
);
213 (Target
: in out List
;
215 Source
: in out List
)
218 Pre
=> Length
(Source
) + Length
(Target
) <= Target
.Capacity
219 and then (Has_Element
(Target
, Before
)
220 or else Before
= No_Element
);
223 (Target
: in out List
;
225 Source
: in out List
;
226 Position
: in out Cursor
)
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
);
235 (Container
: in out List
;
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
);
245 function First
(Container
: List
) return Cursor
with
248 function First_Element
(Container
: List
) return Element_Type
with
250 Pre
=> not Is_Empty
(Container
);
252 function Last
(Container
: List
) return Cursor
with
255 function Last_Element
(Container
: List
) return Element_Type
with
257 Pre
=> not Is_Empty
(Container
);
259 function Next
(Container
: List
; Position
: Cursor
) return Cursor
with
261 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
263 procedure Next
(Container
: List
; Position
: in out Cursor
) with
265 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
267 function Previous
(Container
: List
; Position
: Cursor
) return Cursor
with
269 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
271 procedure Previous
(Container
: List
; Position
: in out Cursor
) with
273 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
278 Position
: Cursor
:= No_Element
) return Cursor
281 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
283 function Reverse_Find
286 Position
: Cursor
:= No_Element
) return Cursor
289 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
293 Item
: Element_Type
) return Boolean
297 function Has_Element
(Container
: List
; Position
: Cursor
) return Boolean
302 with function "<" (Left
, Right
: Element_Type
) return Boolean is <>;
303 package Generic_Sorting
with SPARK_Mode
is
305 function Is_Sorted
(Container
: List
) return Boolean with
308 procedure Sort
(Container
: in out List
) with
311 procedure Merge
(Target
, Source
: in out List
) with
316 function Strict_Equal
(Left
, Right
: List
) return Boolean with
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.
323 function First_To_Previous
(Container
: List
; Current
: Cursor
) return List
327 Pre
=> Has_Element
(Container
, Current
) or else Current
= No_Element
;
329 function Current_To_Last
(Container
: List
; Current
: Cursor
) return List
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
343 pragma SPARK_Mode
(Off
);
345 type Node_Type
is record
346 Prev
: Count_Type
'Base := -1;
348 Element
: Element_Type
;
351 function "=" (L
, R
: Node_Type
) return Boolean is abstract;
353 type Node_Array
is array (Count_Type
range <>) of Node_Type
;
354 function "=" (L
, R
: Node_Array
) return Boolean is abstract;
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 => <>);
364 type Cursor
is record
365 Node
: Count_Type
:= 0;
368 Empty_List
: constant List
:= (0, others => <>);
370 No_Element
: constant Cursor
:= (Node
=> 0);
372 end Ada
.Containers
.Formal_Doubly_Linked_Lists
;