1------------------------------------------------------------------------------ 2-- -- 3-- GNAT LIBRARY COMPONENTS -- 4-- -- 5-- A D A . C O N T A I N E R S . F O R M A L _ V E C T O R S -- 6-- -- 7-- S p e c -- 8-- -- 9-- Copyright (C) 2004-2013, 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-- 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 32-- This spec is derived from package Ada.Containers.Bounded_Vectors in the Ada 33-- 2012 RM. The modifications are meant to facilitate formal proofs by making 34-- it easier to express properties, and by making the specification of this 35-- 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-- content of a container: Element, Next, Query_Element, Previous, Iterate, 42-- Has_Element, Reverse_Iterate. 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 : Vector) return Boolean; 51-- function First_To_Previous (Container : Vector; Current : Cursor) 52-- return Vector; 53-- function Current_To_Last (Container : Vector; Current : Cursor) 54-- return Vector; 55 56-- See detailed specifications for these subprograms 57 58with Ada.Containers; 59use Ada.Containers; 60 61generic 62 type Index_Type is range <>; 63 type Element_Type is private; 64 65 with function "=" (Left, Right : Element_Type) return Boolean is <>; 66 67package Ada.Containers.Formal_Vectors is 68 pragma Annotate (GNATprove, External_Axiomatization); 69 pragma Pure; 70 71 subtype Extended_Index is Index_Type'Base 72 range Index_Type'First - 1 .. 73 Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1; 74 75 No_Index : constant Extended_Index := Extended_Index'First; 76 77 subtype Capacity_Range is 78 Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1); 79 80 type Vector (Capacity : Capacity_Range) is private with 81 Iterable => (First => First, 82 Next => Next, 83 Has_Element => Has_Element, 84 Element => Element); 85 86 type Cursor is private; 87 pragma Preelaborable_Initialization (Cursor); 88 89 Empty_Vector : constant Vector; 90 91 No_Element : constant Cursor; 92 93 function "=" (Left, Right : Vector) return Boolean with 94 Global => null; 95 96 function To_Vector 97 (New_Item : Element_Type; 98 Length : Count_Type) return Vector 99 with 100 Global => null; 101 102 function "&" (Left, Right : Vector) return Vector with 103 Global => null, 104 Pre => Capacity_Range'Last - Length (Left) >= Length (Right); 105 106 function "&" (Left : Vector; Right : Element_Type) return Vector with 107 Global => null, 108 Pre => Length (Left) < Capacity_Range'Last; 109 110 function "&" (Left : Element_Type; Right : Vector) return Vector with 111 Global => null, 112 Pre => Length (Right) < Capacity_Range'Last; 113 114 function "&" (Left, Right : Element_Type) return Vector with 115 Global => null, 116 Pre => Capacity_Range'Last >= 2; 117 118 function Capacity (Container : Vector) return Count_Type with 119 Global => null; 120 121 procedure Reserve_Capacity 122 (Container : in out Vector; 123 Capacity : Count_Type) 124 with 125 Global => null, 126 Pre => Capacity <= Container.Capacity; 127 128 function Length (Container : Vector) return Count_Type with 129 Global => null; 130 131 procedure Set_Length 132 (Container : in out Vector; 133 New_Length : Count_Type) 134 with 135 Global => null, 136 Pre => New_Length <= Length (Container); 137 138 function Is_Empty (Container : Vector) return Boolean with 139 Global => null; 140 141 procedure Clear (Container : in out Vector) with 142 Global => null; 143 144 procedure Assign (Target : in out Vector; Source : Vector) with 145 Global => null, 146 Pre => Length (Source) <= Target.Capacity; 147 148 function Copy 149 (Source : Vector; 150 Capacity : Count_Type := 0) return Vector 151 with 152 Global => null, 153 Pre => Length (Source) <= Capacity and then Capacity in Capacity_Range; 154 155 function To_Cursor 156 (Container : Vector; 157 Index : Extended_Index) return Cursor 158 with 159 Global => null; 160 161 function To_Index (Position : Cursor) return Extended_Index with 162 Global => null; 163 164 function Element 165 (Container : Vector; 166 Index : Index_Type) return Element_Type 167 with 168 Global => null, 169 Pre => First_Index (Container) <= Index 170 and then Index <= Last_Index (Container); 171 172 function Element 173 (Container : Vector; 174 Position : Cursor) return Element_Type 175 with 176 Global => null, 177 Pre => Has_Element (Container, Position); 178 179 procedure Replace_Element 180 (Container : in out Vector; 181 Index : Index_Type; 182 New_Item : Element_Type) 183 with 184 Global => null, 185 Pre => First_Index (Container) <= Index 186 and then Index <= Last_Index (Container); 187 188 procedure Replace_Element 189 (Container : in out Vector; 190 Position : Cursor; 191 New_Item : Element_Type) 192 with 193 Global => null, 194 Pre => Has_Element (Container, Position); 195 196 procedure Move (Target : in out Vector; Source : in out Vector) with 197 Global => null, 198 Pre => Length (Source) <= Target.Capacity; 199 200 procedure Insert 201 (Container : in out Vector; 202 Before : Extended_Index; 203 New_Item : Vector) 204 with 205 Global => null, 206 Pre => First_Index (Container) <= Before 207 and then Before <= Last_Index (Container) + 1 208 and then Length (Container) < Container.Capacity; 209 210 procedure Insert 211 (Container : in out Vector; 212 Before : Cursor; 213 New_Item : Vector) 214 with 215 Global => null, 216 Pre => Length (Container) < Container.Capacity 217 and then (Has_Element (Container, Before) 218 or else Before = No_Element); 219 220 procedure Insert 221 (Container : in out Vector; 222 Before : Cursor; 223 New_Item : Vector; 224 Position : out Cursor) 225 with 226 Global => null, 227 Pre => Length (Container) < Container.Capacity 228 and then (Has_Element (Container, Before) 229 or else Before = No_Element); 230 231 procedure Insert 232 (Container : in out Vector; 233 Before : Extended_Index; 234 New_Item : Element_Type; 235 Count : Count_Type := 1) 236 with 237 Global => null, 238 Pre => First_Index (Container) <= Before 239 and then Before <= Last_Index (Container) + 1 240 and then Length (Container) + Count <= Container.Capacity; 241 242 procedure Insert 243 (Container : in out Vector; 244 Before : Cursor; 245 New_Item : Element_Type; 246 Count : Count_Type := 1) 247 with 248 Global => null, 249 Pre => Length (Container) + Count <= Container.Capacity 250 and then (Has_Element (Container, Before) 251 or else Before = No_Element); 252 253 procedure Insert 254 (Container : in out Vector; 255 Before : Cursor; 256 New_Item : Element_Type; 257 Position : out Cursor; 258 Count : Count_Type := 1) 259 with 260 Global => null, 261 Pre => Length (Container) + Count <= Container.Capacity 262 and then (Has_Element (Container, Before) 263 or else Before = No_Element); 264 265 procedure Prepend 266 (Container : in out Vector; 267 New_Item : Vector) 268 with 269 Global => null, 270 Pre => Length (Container) < Container.Capacity; 271 272 procedure Prepend 273 (Container : in out Vector; 274 New_Item : Element_Type; 275 Count : Count_Type := 1) 276 with 277 Global => null, 278 Pre => Length (Container) + Count <= Container.Capacity; 279 280 procedure Append 281 (Container : in out Vector; 282 New_Item : Vector) 283 with 284 Global => null, 285 Pre => Length (Container) < Container.Capacity; 286 287 procedure Append 288 (Container : in out Vector; 289 New_Item : Element_Type; 290 Count : Count_Type := 1) 291 with 292 Global => null, 293 Pre => Length (Container) + Count <= Container.Capacity; 294 295 procedure Delete 296 (Container : in out Vector; 297 Index : Extended_Index; 298 Count : Count_Type := 1) 299 with 300 Global => null, 301 Pre => First_Index (Container) <= Index 302 and then Index <= Last_Index (Container) + 1; 303 304 procedure Delete 305 (Container : in out Vector; 306 Position : in out Cursor; 307 Count : Count_Type := 1) 308 with 309 Global => null, 310 Pre => Has_Element (Container, Position); 311 312 procedure Delete_First 313 (Container : in out Vector; 314 Count : Count_Type := 1) 315 with 316 Global => null; 317 318 procedure Delete_Last 319 (Container : in out Vector; 320 Count : Count_Type := 1) 321 with 322 Global => null; 323 324 procedure Reverse_Elements (Container : in out Vector) with 325 Global => null; 326 327 procedure Swap (Container : in out Vector; I, J : Index_Type) with 328 Global => null, 329 Pre => First_Index (Container) <= I 330 and then I <= Last_Index (Container) 331 and then First_Index (Container) <= J 332 and then J <= Last_Index (Container); 333 334 procedure Swap (Container : in out Vector; I, J : Cursor) with 335 Global => null, 336 Pre => Has_Element (Container, I) and then Has_Element (Container, J); 337 338 function First_Index (Container : Vector) return Index_Type with 339 Global => null; 340 341 function First (Container : Vector) return Cursor with 342 Global => null; 343 344 function First_Element (Container : Vector) return Element_Type with 345 Global => null, 346 Pre => not Is_Empty (Container); 347 348 function Last_Index (Container : Vector) return Extended_Index with 349 Global => null; 350 351 function Last (Container : Vector) return Cursor with 352 Global => null; 353 354 function Last_Element (Container : Vector) return Element_Type with 355 Global => null, 356 Pre => not Is_Empty (Container); 357 358 function Next (Container : Vector; Position : Cursor) return Cursor with 359 Global => null, 360 Pre => Has_Element (Container, Position) or else Position = No_Element; 361 362 procedure Next (Container : Vector; Position : in out Cursor) with 363 Global => null, 364 Pre => Has_Element (Container, Position) or else Position = No_Element; 365 366 function Previous (Container : Vector; Position : Cursor) return Cursor with 367 Global => null, 368 Pre => Has_Element (Container, Position) or else Position = No_Element; 369 370 procedure Previous (Container : Vector; Position : in out Cursor) with 371 Global => null, 372 Pre => Has_Element (Container, Position) or else Position = No_Element; 373 374 function Find_Index 375 (Container : Vector; 376 Item : Element_Type; 377 Index : Index_Type := Index_Type'First) return Extended_Index 378 with 379 Global => null; 380 381 function Find 382 (Container : Vector; 383 Item : Element_Type; 384 Position : Cursor := No_Element) return Cursor 385 with 386 Global => null, 387 Pre => Has_Element (Container, Position) or else Position = No_Element; 388 389 function Reverse_Find_Index 390 (Container : Vector; 391 Item : Element_Type; 392 Index : Index_Type := Index_Type'Last) return Extended_Index 393 with 394 Global => null; 395 396 function Reverse_Find 397 (Container : Vector; 398 Item : Element_Type; 399 Position : Cursor := No_Element) return Cursor 400 with 401 Global => null, 402 Pre => Has_Element (Container, Position) or else Position = No_Element; 403 404 function Contains 405 (Container : Vector; 406 Item : Element_Type) return Boolean 407 with 408 Global => null; 409 410 function Has_Element (Container : Vector; Position : Cursor) return Boolean 411 with 412 Global => null; 413 414 generic 415 with function "<" (Left, Right : Element_Type) return Boolean is <>; 416 package Generic_Sorting is 417 418 function Is_Sorted (Container : Vector) return Boolean with 419 Global => null; 420 421 procedure Sort (Container : in out Vector) with 422 Global => null; 423 424 procedure Merge (Target : in out Vector; Source : in out Vector) with 425 Global => null; 426 427 end Generic_Sorting; 428 429 function Strict_Equal (Left, Right : Vector) return Boolean with 430 Global => null; 431 -- Strict_Equal returns True if the containers are physically equal, i.e. 432 -- they are structurally equal (function "=" returns True) and that they 433 -- have the same set of cursors. 434 435 function First_To_Previous 436 (Container : Vector; 437 Current : Cursor) return Vector 438 with 439 Global => null, 440 Pre => Has_Element (Container, Current) or else Current = No_Element; 441 function Current_To_Last 442 (Container : Vector; 443 Current : Cursor) return Vector 444 with 445 Global => null, 446 Pre => Has_Element (Container, Current) or else Current = No_Element; 447 -- First_To_Previous returns a container containing all elements preceding 448 -- Current (excluded) in Container. Current_To_Last returns a container 449 -- containing all elements following Current (included) in Container. 450 -- These two new functions can be used to express invariant properties in 451 -- loops which iterate over containers. First_To_Previous returns the part 452 -- of the container already scanned and Current_To_Last the part not 453 -- scanned yet. 454 455private 456 457 pragma Inline (First_Index); 458 pragma Inline (Last_Index); 459 pragma Inline (Element); 460 pragma Inline (First_Element); 461 pragma Inline (Last_Element); 462 pragma Inline (Replace_Element); 463 pragma Inline (Contains); 464 pragma Inline (Next); 465 pragma Inline (Previous); 466 467 type Elements_Array is array (Count_Type range <>) of Element_Type; 468 function "=" (L, R : Elements_Array) return Boolean is abstract; 469 470 type Vector (Capacity : Capacity_Range) is record 471 Elements : Elements_Array (1 .. Capacity); 472 Last : Extended_Index := No_Index; 473 end record; 474 475 type Cursor is record 476 Valid : Boolean := True; 477 Index : Index_Type := Index_Type'First; 478 end record; 479 480 Empty_Vector : constant Vector := (Capacity => 0, others => <>); 481 482 No_Element : constant Cursor := (Valid => False, Index => Index_Type'First); 483 484end Ada.Containers.Formal_Vectors; 485