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 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 Left (Container : List; Position : Cursor) return List;
52 -- function Right (Container : List; Position : Cursor) return List;
54 -- See subprogram specifications that follow for details
57 type Element_Type
is private;
59 with function "=" (Left
, Right
: Element_Type
)
62 package Ada
.Containers
.Formal_Doubly_Linked_Lists
is
63 pragma Annotate
(GNATprove
, External_Axiomatization
);
66 type List
(Capacity
: Count_Type
) is private;
67 pragma Preelaborable_Initialization
(List
);
69 type Cursor
is private;
70 pragma Preelaborable_Initialization
(Cursor
);
72 Empty_List
: constant List
;
74 No_Element
: constant Cursor
;
76 function "=" (Left
, Right
: List
) return Boolean;
78 function Length
(Container
: List
) return Count_Type
;
80 function Is_Empty
(Container
: List
) return Boolean;
82 procedure Clear
(Container
: in out List
);
84 procedure Assign
(Target
: in out List
; Source
: List
) with
85 Pre
=> Target
.Capacity
>= Length
(Source
);
87 function Copy
(Source
: List
; Capacity
: Count_Type
:= 0) return List
with
88 Pre
=> Capacity
= 0 or else Capacity
>= Source
.Capacity
;
92 Position
: Cursor
) return Element_Type
94 Pre
=> Has_Element
(Container
, Position
);
96 procedure Replace_Element
97 (Container
: in out List
;
99 New_Item
: Element_Type
)
101 Pre
=> Has_Element
(Container
, Position
);
103 procedure Move
(Target
: in out List
; Source
: in out List
) with
104 Pre
=> Target
.Capacity
>= Length
(Source
);
107 (Container
: in out List
;
109 New_Item
: Element_Type
;
110 Count
: Count_Type
:= 1)
112 Pre
=> Length
(Container
) + Count
<= Container
.Capacity
113 and then (Has_Element
(Container
, Before
)
114 or else Before
= No_Element
);
117 (Container
: in out List
;
119 New_Item
: Element_Type
;
120 Position
: out Cursor
;
121 Count
: Count_Type
:= 1)
123 Pre
=> Length
(Container
) + Count
<= Container
.Capacity
124 and then (Has_Element
(Container
, Before
)
125 or else Before
= No_Element
);
128 (Container
: in out List
;
130 Position
: out Cursor
;
131 Count
: Count_Type
:= 1)
133 Pre
=> Length
(Container
) + Count
<= Container
.Capacity
134 and then (Has_Element
(Container
, Before
)
135 or else Before
= No_Element
);
138 (Container
: in out List
;
139 New_Item
: Element_Type
;
140 Count
: Count_Type
:= 1)
142 Pre
=> Length
(Container
) + Count
<= Container
.Capacity
;
145 (Container
: in out List
;
146 New_Item
: Element_Type
;
147 Count
: Count_Type
:= 1)
149 Pre
=> Length
(Container
) + Count
<= Container
.Capacity
;
152 (Container
: in out List
;
153 Position
: in out Cursor
;
154 Count
: Count_Type
:= 1)
156 Pre
=> Has_Element
(Container
, Position
);
158 procedure Delete_First
159 (Container
: in out List
;
160 Count
: Count_Type
:= 1);
162 procedure Delete_Last
163 (Container
: in out List
;
164 Count
: Count_Type
:= 1);
166 procedure Reverse_Elements
(Container
: in out List
);
169 (Container
: in out List
;
172 Pre
=> Has_Element
(Container
, I
) and then Has_Element
(Container
, J
);
175 (Container
: in out List
;
178 Pre
=> Has_Element
(Container
, I
) and then Has_Element
(Container
, J
);
181 (Target
: in out List
;
183 Source
: in out List
)
185 Pre
=> Length
(Source
) + Length
(Target
) <= Target
.Capacity
186 and then (Has_Element
(Target
, Before
)
187 or else Before
= No_Element
);
190 (Target
: in out List
;
192 Source
: in out List
;
193 Position
: in out Cursor
)
195 Pre
=> Length
(Source
) + Length
(Target
) <= Target
.Capacity
196 and then (Has_Element
(Target
, Before
)
197 or else Before
= No_Element
)
198 and then Has_Element
(Source
, Position
);
201 (Container
: in out List
;
205 Pre
=> 2 * Length
(Container
) <= Container
.Capacity
206 and then (Has_Element
(Container
, Before
)
207 or else Before
= No_Element
)
208 and then Has_Element
(Container
, Position
);
210 function First
(Container
: List
) return Cursor
;
212 function First_Element
(Container
: List
) return Element_Type
with
213 Pre
=> not Is_Empty
(Container
);
215 function Last
(Container
: List
) return Cursor
;
217 function Last_Element
(Container
: List
) return Element_Type
with
218 Pre
=> not Is_Empty
(Container
);
220 function Next
(Container
: List
; Position
: Cursor
) return Cursor
with
221 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
223 procedure Next
(Container
: List
; Position
: in out Cursor
) with
224 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
226 function Previous
(Container
: List
; Position
: Cursor
) return Cursor
with
227 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
229 procedure Previous
(Container
: List
; Position
: in out Cursor
) with
230 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
235 Position
: Cursor
:= No_Element
) return Cursor
237 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
239 function Reverse_Find
242 Position
: Cursor
:= No_Element
) return Cursor
244 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
248 Item
: Element_Type
) return Boolean;
250 function Has_Element
(Container
: List
; Position
: Cursor
) return Boolean;
253 with function "<" (Left
, Right
: Element_Type
) return Boolean is <>;
254 package Generic_Sorting
is
256 function Is_Sorted
(Container
: List
) return Boolean;
258 procedure Sort
(Container
: in out List
);
260 procedure Merge
(Target
, Source
: in out List
);
264 function Strict_Equal
(Left
, Right
: List
) return Boolean;
265 -- Strict_Equal returns True if the containers are physically equal, i.e.
266 -- they are structurally equal (function "=" returns True) and that they
267 -- have the same set of cursors.
269 function Left
(Container
: List
; Position
: Cursor
) return List
with
270 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
271 function Right
(Container
: List
; Position
: Cursor
) return List
with
272 Pre
=> Has_Element
(Container
, Position
) or else Position
= No_Element
;
273 -- Left returns a container containing all elements preceding Position
274 -- (excluded) in Container. Right returns a container containing all
275 -- elements following Position (included) in Container. These two new
276 -- functions can be used to express invariant properties in loops which
277 -- iterate over containers. Left returns the part of the container already
278 -- scanned and Right the part not scanned yet.
282 type Node_Type
is record
283 Prev
: Count_Type
'Base := -1;
285 Element
: Element_Type
;
288 function "=" (L
, R
: Node_Type
) return Boolean is abstract;
290 type Node_Array
is array (Count_Type
range <>) of Node_Type
;
291 function "=" (L
, R
: Node_Array
) return Boolean is abstract;
293 type List
(Capacity
: Count_Type
) is tagged record
294 Nodes
: Node_Array
(1 .. Capacity
) := (others => <>);
295 Free
: Count_Type
'Base := -1;
296 Length
: Count_Type
:= 0;
297 First
: Count_Type
:= 0;
298 Last
: Count_Type
:= 0;
301 type Cursor
is record
302 Node
: Count_Type
:= 0;
305 Empty_List
: constant List
:= (0, others => <>);
307 No_Element
: constant Cursor
:= (Node
=> 0);
309 end Ada
.Containers
.Formal_Doubly_Linked_Lists
;