1 ------------------------------------------------------------------------------
3 -- GNAT LIBRARY COMPONENTS --
5 -- ADA.CONTAINERS.FORMAL_DOUBLY_LINKED_LISTS --
9 -- Copyright (C) 2004-2013, 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 to facilitate formal proofs by making it
34 -- easier to express properties.
36 -- The modifications are:
38 -- A parameter for the container is added to every function reading the
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,
43 -- which is not possible if cursors encapsulate an access to the underlying
46 -- There are three new functions:
48 -- function Strict_Equal (Left, Right : List) return Boolean;
49 -- function Left (Container : List; Position : Cursor) return List;
50 -- function Right (Container : List; Position : Cursor) return List;
52 -- See subprogram specifications that follow for details
55 type Element_Type
is private;
57 with function "=" (Left
, Right
: Element_Type
)
60 package Ada
.Containers
.Formal_Doubly_Linked_Lists
is
63 type List
(Capacity
: Count_Type
) is private;
64 pragma Preelaborable_Initialization
(List
);
66 type Cursor
is private;
67 pragma Preelaborable_Initialization
(Cursor
);
69 Empty_List
: constant List
;
71 No_Element
: constant Cursor
;
73 function "=" (Left
, Right
: List
) return Boolean;
75 function Length
(Container
: List
) return Count_Type
;
77 function Is_Empty
(Container
: List
) return Boolean;
79 procedure Clear
(Container
: in out List
);
81 procedure Assign
(Target
: in out List
; Source
: List
) with
82 Pre
=> Target
.Capacity
>= Length
(Source
);
84 function Copy
(Source
: List
; Capacity
: Count_Type
:= 0) return List
;
88 Position
: Cursor
) return Element_Type
90 Pre
=> Has_Element
(Container
, Position
);
92 procedure Replace_Element
93 (Container
: in out List
;
95 New_Item
: Element_Type
)
97 Pre
=> Has_Element
(Container
, Position
);
99 procedure Move
(Target
: in out List
; Source
: in out List
) with
100 Pre
=> Target
.Capacity
>= Length
(Source
);
103 (Container
: in out List
;
105 New_Item
: Element_Type
;
106 Count
: Count_Type
:= 1)
108 Pre
=> Length
(Container
) + Count
<= Container
.Capacity
109 and then (Has_Element
(Container
, Before
)
110 or else Before
= No_Element
);
113 (Container
: in out List
;
115 New_Item
: Element_Type
;
116 Position
: out Cursor
;
117 Count
: Count_Type
:= 1)
119 Pre
=> Length
(Container
) + Count
<= Container
.Capacity
120 and then (Has_Element
(Container
, Before
)
121 or else Before
= No_Element
);
124 (Container
: in out List
;
126 Position
: out Cursor
;
127 Count
: Count_Type
:= 1)
129 Pre
=> Length
(Container
) + Count
<= Container
.Capacity
130 and then (Has_Element
(Container
, Before
)
131 or else Before
= No_Element
);
134 (Container
: in out List
;
135 New_Item
: Element_Type
;
136 Count
: Count_Type
:= 1)
138 Pre
=> Length
(Container
) + Count
<= Container
.Capacity
;
141 (Container
: in out List
;
142 New_Item
: Element_Type
;
143 Count
: Count_Type
:= 1)
145 Pre
=> Length
(Container
) + Count
<= Container
.Capacity
;
148 (Container
: in out List
;
149 Position
: in out Cursor
;
150 Count
: Count_Type
:= 1)
152 Pre
=> Has_Element
(Container
, Position
);
154 procedure Delete_First
155 (Container
: in out List
;
156 Count
: Count_Type
:= 1);
158 procedure Delete_Last
159 (Container
: in out List
;
160 Count
: Count_Type
:= 1);
162 procedure Reverse_Elements
(Container
: in out List
);
165 (Container
: in out List
;
168 Pre
=> Has_Element
(Container
, I
) and then Has_Element
(Container
, J
);
171 (Container
: in out List
;
174 Pre
=> Has_Element
(Container
, I
) and then Has_Element
(Container
, J
);
177 (Target
: in out List
;
179 Source
: in out List
)
181 Pre
=> Length
(Source
) + Length
(Target
) <= Target
.Capacity
182 and then (Has_Element
(Target
, Before
)
183 or else Before
= No_Element
);
186 (Target
: in out List
;
188 Source
: in out List
;
189 Position
: in out Cursor
)
191 Pre
=> Length
(Source
) + Length
(Target
) <= Target
.Capacity
192 and then (Has_Element
(Target
, Before
)
193 or else Before
= No_Element
)
194 and then Has_Element
(Source
, Position
);
197 (Container
: in out List
;
201 Pre
=> 2 * Length
(Container
) <= Container
.Capacity
202 and then (Has_Element
(Container
, Before
)
203 or else Before
= No_Element
)
204 and then Has_Element
(Container
, Position
);
206 function First
(Container
: List
) return Cursor
;
208 function First_Element
(Container
: List
) return Element_Type
with
209 Pre
=> not Is_Empty
(Container
);
211 function Last
(Container
: List
) return Cursor
;
213 function Last_Element
(Container
: List
) return Element_Type
with
214 Pre
=> not Is_Empty
(Container
);
216 function Next
(Container
: List
; Position
: Cursor
) return Cursor
with
217 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
219 procedure Next
(Container
: List
; Position
: in out Cursor
) with
220 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
222 function Previous
(Container
: List
; Position
: Cursor
) return Cursor
with
223 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
225 procedure Previous
(Container
: List
; Position
: in out Cursor
) with
226 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
231 Position
: Cursor
:= No_Element
) return Cursor
233 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
235 function Reverse_Find
238 Position
: Cursor
:= No_Element
) return Cursor
240 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
244 Item
: Element_Type
) return Boolean;
246 function Has_Element
(Container
: List
; Position
: Cursor
) return Boolean;
249 with function "<" (Left
, Right
: Element_Type
) return Boolean is <>;
250 package Generic_Sorting
is
252 function Is_Sorted
(Container
: List
) return Boolean;
254 procedure Sort
(Container
: in out List
);
256 procedure Merge
(Target
, Source
: in out List
);
260 function Strict_Equal
(Left
, Right
: List
) return Boolean;
261 -- Strict_Equal returns True if the containers are physically equal, i.e.
262 -- they are structurally equal (function "=" returns True) and that they
263 -- have the same set of cursors.
265 function Left
(Container
: List
; Position
: Cursor
) return List
with
266 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
267 function Right
(Container
: List
; Position
: Cursor
) return List
with
268 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
269 -- Left returns a container containing all elements preceding Position
270 -- (excluded) in Container. Right returns a container containing all
271 -- elements following Position (included) in Container. These two new
272 -- functions can be used to express invariant properties in loops which
273 -- iterate over containers. Left returns the part of the container already
274 -- scanned and Right the part not scanned yet.
278 type Node_Type
is record
279 Prev
: Count_Type
'Base := -1;
281 Element
: Element_Type
;
284 function "=" (L
, R
: Node_Type
) return Boolean is abstract;
286 type Node_Array
is array (Count_Type
range <>) of Node_Type
;
287 function "=" (L
, R
: Node_Array
) return Boolean is abstract;
289 type List
(Capacity
: Count_Type
) is tagged record
290 Nodes
: Node_Array
(1 .. Capacity
) := (others => <>);
291 Free
: Count_Type
'Base := -1;
292 Length
: Count_Type
:= 0;
293 First
: Count_Type
:= 0;
294 Last
: Count_Type
:= 0;
297 type Cursor
is record
298 Node
: Count_Type
:= 0;
301 Empty_List
: constant List
:= (0, others => <>);
303 No_Element
: constant Cursor
:= (Node
=> 0);
305 end Ada
.Containers
.Formal_Doubly_Linked_Lists
;