1------------------------------------------------------------------------------ 2-- -- 3-- GNAT LIBRARY COMPONENTS -- 4-- -- 5-- ADA.CONTAINERS.FORMAL_INDEFINITE_VECTORS -- 6-- -- 7-- S p e c -- 8-- -- 9-- Copyright (C) 2014-2018, 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-- Similar to Ada.Containers.Formal_Vectors. The main difference is that 33-- Element_Type may be indefinite (but not an unconstrained array). 34 35with Ada.Containers.Bounded_Holders; 36with Ada.Containers.Functional_Vectors; 37 38generic 39 type Index_Type is range <>; 40 type Element_Type (<>) is private; 41 Max_Size_In_Storage_Elements : Natural := 42 Element_Type'Max_Size_In_Storage_Elements; 43 -- Maximum size of Vector elements in bytes. This has the same meaning as 44 -- in Ada.Containers.Bounded_Holders, with the same restrictions. Note that 45 -- setting this too small can lead to erroneous execution; see comments in 46 -- Ada.Containers.Bounded_Holders. If Element_Type is class-wide, it is the 47 -- responsibility of clients to calculate the maximum size of all types in 48 -- the class. 49 50 Bounded : Boolean := True; 51 -- If True, the containers are bounded; the initial capacity is the maximum 52 -- size, and heap allocation will be avoided. If False, the containers can 53 -- grow via heap allocation. 54 55package Ada.Containers.Formal_Indefinite_Vectors with 56 SPARK_Mode => On 57is 58 pragma Annotate (CodePeer, Skip_Analysis); 59 60 subtype Extended_Index is Index_Type'Base 61 range Index_Type'First - 1 .. 62 Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1; 63 64 No_Index : constant Extended_Index := Extended_Index'First; 65 66 Last_Count : constant Count_Type := 67 (if Index_Type'Last < Index_Type'First then 68 0 69 elsif Index_Type'Last < -1 70 or else Index_Type'Pos (Index_Type'First) > 71 Index_Type'Pos (Index_Type'Last) - Count_Type'Last 72 then 73 Index_Type'Pos (Index_Type'Last) - 74 Index_Type'Pos (Index_Type'First) + 1 75 else 76 Count_Type'Last); 77 -- Maximal capacity of any vector. It is the minimum of the size of the 78 -- index range and the last possible Count_Type. 79 80 subtype Capacity_Range is Count_Type range 0 .. Last_Count; 81 82 type Vector (Capacity : Capacity_Range) is limited private with 83 Default_Initial_Condition => Is_Empty (Vector); 84 -- In the bounded case, Capacity is the capacity of the container, which 85 -- never changes. In the unbounded case, Capacity is the initial capacity 86 -- of the container, and operations such as Reserve_Capacity and Append can 87 -- increase the capacity. The capacity never shrinks, except in the case of 88 -- Clear. 89 -- 90 -- Note that all objects of type Vector are constrained, including in the 91 -- unbounded case; you can't assign from one object to another if the 92 -- Capacity is different. 93 94 function Length (Container : Vector) return Capacity_Range with 95 Global => null, 96 Post => Length'Result <= Capacity (Container); 97 98 pragma Unevaluated_Use_Of_Old (Allow); 99 100 package Formal_Model with Ghost is 101 102 package M is new Ada.Containers.Functional_Vectors 103 (Index_Type => Index_Type, 104 Element_Type => Element_Type); 105 106 function "=" 107 (Left : M.Sequence; 108 Right : M.Sequence) return Boolean renames M."="; 109 110 function "<" 111 (Left : M.Sequence; 112 Right : M.Sequence) return Boolean renames M."<"; 113 114 function "<=" 115 (Left : M.Sequence; 116 Right : M.Sequence) return Boolean renames M."<="; 117 118 function M_Elements_In_Union 119 (Container : M.Sequence; 120 Left : M.Sequence; 121 Right : M.Sequence) return Boolean 122 -- The elements of Container are contained in either Left or Right 123 with 124 Global => null, 125 Post => 126 M_Elements_In_Union'Result = 127 (for all I in Index_Type'First .. M.Last (Container) => 128 (for some J in Index_Type'First .. M.Last (Left) => 129 Element (Container, I) = Element (Left, J)) 130 or (for some J in Index_Type'First .. M.Last (Right) => 131 Element (Container, I) = Element (Right, J))); 132 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union); 133 134 function M_Elements_Included 135 (Left : M.Sequence; 136 L_Fst : Index_Type := Index_Type'First; 137 L_Lst : Extended_Index; 138 Right : M.Sequence; 139 R_Fst : Index_Type := Index_Type'First; 140 R_Lst : Extended_Index) return Boolean 141 -- The elements of the slice from L_Fst to L_Lst in Left are contained 142 -- in the slide from R_Fst to R_Lst in Right. 143 with 144 Global => null, 145 Pre => L_Lst <= M.Last (Left) and R_Lst <= M.Last (Right), 146 Post => 147 M_Elements_Included'Result = 148 (for all I in L_Fst .. L_Lst => 149 (for some J in R_Fst .. R_Lst => 150 Element (Left, I) = Element (Right, J))); 151 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Included); 152 153 function M_Elements_Reversed 154 (Left : M.Sequence; 155 Right : M.Sequence) return Boolean 156 -- Right is Left in reverse order 157 with 158 Global => null, 159 Post => 160 M_Elements_Reversed'Result = 161 (M.Length (Left) = M.Length (Right) 162 and (for all I in Index_Type'First .. M.Last (Left) => 163 Element (Left, I) = 164 Element (Right, M.Last (Left) - I + 1)) 165 and (for all I in Index_Type'First .. M.Last (Right) => 166 Element (Right, I) = 167 Element (Left, M.Last (Left) - I + 1))); 168 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed); 169 170 function M_Elements_Swapped 171 (Left : M.Sequence; 172 Right : M.Sequence; 173 X : Index_Type; 174 Y : Index_Type) return Boolean 175 -- Elements stored at X and Y are reversed in Left and Right 176 with 177 Global => null, 178 Pre => X <= M.Last (Left) and Y <= M.Last (Left), 179 Post => 180 M_Elements_Swapped'Result = 181 (M.Length (Left) = M.Length (Right) 182 and Element (Left, X) = Element (Right, Y) 183 and Element (Left, Y) = Element (Right, X) 184 and M.Equal_Except (Left, Right, X, Y)); 185 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped); 186 187 function Model (Container : Vector) return M.Sequence with 188 -- The high-level model of a vector is a sequence of elements. The 189 -- sequence really is similar to the vector itself. However, it is not 190 -- limited which allows usage of 'Old and 'Loop_Entry attributes. 191 192 Ghost, 193 Global => null, 194 Post => M.Length (Model'Result) = Length (Container); 195 196 function Element 197 (S : M.Sequence; 198 I : Index_Type) return Element_Type renames M.Get; 199 -- To improve readability of contracts, we rename the function used to 200 -- access an element in the model to Element. 201 202 end Formal_Model; 203 use Formal_Model; 204 205 function Empty_Vector return Vector with 206 Global => null, 207 Post => Length (Empty_Vector'Result) = 0; 208 209 function "=" (Left, Right : Vector) return Boolean with 210 Global => null, 211 Post => "="'Result = (Model (Left) = Model (Right)); 212 213 function To_Vector 214 (New_Item : Element_Type; 215 Length : Capacity_Range) return Vector 216 with 217 Global => null, 218 Post => 219 Formal_Indefinite_Vectors.Length (To_Vector'Result) = Length 220 and M.Constant_Range 221 (Container => Model (To_Vector'Result), 222 Fst => Index_Type'First, 223 Lst => Last_Index (To_Vector'Result), 224 Item => New_Item); 225 226 function Capacity (Container : Vector) return Capacity_Range with 227 Global => null, 228 Post => 229 Capacity'Result = 230 (if Bounded then 231 Container.Capacity 232 else 233 Capacity_Range'Last); 234 pragma Annotate (GNATprove, Inline_For_Proof, Capacity); 235 236 procedure Reserve_Capacity 237 (Container : in out Vector; 238 Capacity : Capacity_Range) 239 with 240 Global => null, 241 Pre => (if Bounded then Capacity <= Container.Capacity), 242 Post => Model (Container) = Model (Container)'Old; 243 244 function Is_Empty (Container : Vector) return Boolean with 245 Global => null, 246 Post => Is_Empty'Result = (Length (Container) = 0); 247 248 procedure Clear (Container : in out Vector) with 249 Global => null, 250 Post => Length (Container) = 0; 251 -- Note that this reclaims storage in the unbounded case. You need to call 252 -- this before a container goes out of scope in order to avoid storage 253 -- leaks. In addition, "X := ..." can leak unless you Clear(X) first. 254 255 procedure Assign (Target : in out Vector; Source : Vector) with 256 Global => null, 257 Pre => (if Bounded then Length (Source) <= Target.Capacity), 258 Post => Model (Target) = Model (Source); 259 260 function Copy 261 (Source : Vector; 262 Capacity : Capacity_Range := 0) return Vector 263 with 264 Global => null, 265 Pre => (if Bounded then (Capacity = 0 or Length (Source) <= Capacity)), 266 Post => 267 Model (Copy'Result) = Model (Source) 268 and (if Capacity = 0 then 269 Copy'Result.Capacity = Length (Source) 270 else 271 Copy'Result.Capacity = Capacity); 272 273 procedure Move (Target : in out Vector; Source : in out Vector) 274 with 275 Global => null, 276 Pre => (if Bounded then Length (Source) <= Capacity (Target)), 277 Post => Model (Target) = Model (Source)'Old and Length (Source) = 0; 278 279 function Element 280 (Container : Vector; 281 Index : Index_Type) return Element_Type 282 with 283 Global => null, 284 Pre => Index in First_Index (Container) .. Last_Index (Container), 285 Post => Element'Result = Element (Model (Container), Index); 286 pragma Annotate (GNATprove, Inline_For_Proof, Element); 287 288 procedure Replace_Element 289 (Container : in out Vector; 290 Index : Index_Type; 291 New_Item : Element_Type) 292 with 293 Global => null, 294 Pre => Index in First_Index (Container) .. Last_Index (Container), 295 Post => 296 Length (Container) = Length (Container)'Old 297 298 -- Container now has New_Item at index Index 299 300 and Element (Model (Container), Index) = New_Item 301 302 -- All other elements are preserved 303 304 and M.Equal_Except 305 (Left => Model (Container)'Old, 306 Right => Model (Container), 307 Position => Index); 308 309 procedure Insert 310 (Container : in out Vector; 311 Before : Extended_Index; 312 New_Item : Vector) 313 with 314 Global => null, 315 Pre => 316 Length (Container) <= Capacity (Container) - Length (New_Item) 317 and (Before in Index_Type'First .. Last_Index (Container) 318 or (Before /= No_Index 319 and then Before - 1 = Last_Index (Container))), 320 Post => 321 Length (Container) = Length (Container)'Old + Length (New_Item) 322 323 -- Elements located before Before in Container are preserved 324 325 and M.Range_Equal 326 (Left => Model (Container)'Old, 327 Right => Model (Container), 328 Fst => Index_Type'First, 329 Lst => Before - 1) 330 331 -- Elements of New_Item are inserted at position Before 332 333 and (if Length (New_Item) > 0 then 334 M.Range_Shifted 335 (Left => Model (New_Item), 336 Right => Model (Container), 337 Fst => Index_Type'First, 338 Lst => Last_Index (New_Item), 339 Offset => Count_Type (Before - Index_Type'First))) 340 341 -- Elements located after Before in Container are shifted 342 343 and M.Range_Shifted 344 (Left => Model (Container)'Old, 345 Right => Model (Container), 346 Fst => Before, 347 Lst => Last_Index (Container)'Old, 348 Offset => Length (New_Item)); 349 350 procedure Insert 351 (Container : in out Vector; 352 Before : Extended_Index; 353 New_Item : Element_Type) 354 with 355 Global => null, 356 Pre => 357 Length (Container) < Capacity (Container) 358 and then (Before in Index_Type'First .. Last_Index (Container) + 1), 359 Post => 360 Length (Container) = Length (Container)'Old + 1 361 362 -- Elements located before Before in Container are preserved 363 364 and M.Range_Equal 365 (Left => Model (Container)'Old, 366 Right => Model (Container), 367 Fst => Index_Type'First, 368 Lst => Before - 1) 369 370 -- Container now has New_Item at index Before 371 372 and Element (Model (Container), Before) = New_Item 373 374 -- Elements located after Before in Container are shifted by 1 375 376 and M.Range_Shifted 377 (Left => Model (Container)'Old, 378 Right => Model (Container), 379 Fst => Before, 380 Lst => Last_Index (Container)'Old, 381 Offset => 1); 382 383 procedure Insert 384 (Container : in out Vector; 385 Before : Extended_Index; 386 New_Item : Element_Type; 387 Count : Count_Type) 388 with 389 Global => null, 390 Pre => 391 Length (Container) <= Capacity (Container) - Count 392 and (Before in Index_Type'First .. Last_Index (Container) 393 or (Before /= No_Index 394 and then Before - 1 = Last_Index (Container))), 395 Post => 396 Length (Container) = Length (Container)'Old + Count 397 398 -- Elements located before Before in Container are preserved 399 400 and M.Range_Equal 401 (Left => Model (Container)'Old, 402 Right => Model (Container), 403 Fst => Index_Type'First, 404 Lst => Before - 1) 405 406 -- New_Item is inserted Count times at position Before 407 408 and (if Count > 0 then 409 M.Constant_Range 410 (Container => Model (Container), 411 Fst => Before, 412 Lst => Before + Index_Type'Base (Count - 1), 413 Item => New_Item)) 414 415 -- Elements located after Before in Container are shifted 416 417 and M.Range_Shifted 418 (Left => Model (Container)'Old, 419 Right => Model (Container), 420 Fst => Before, 421 Lst => Last_Index (Container)'Old, 422 Offset => Count); 423 424 procedure Prepend (Container : in out Vector; New_Item : Vector) with 425 Global => null, 426 Pre => Length (Container) <= Capacity (Container) - Length (New_Item), 427 Post => 428 Length (Container) = Length (Container)'Old + Length (New_Item) 429 430 -- Elements of New_Item are inserted at the beginning of Container 431 432 and M.Range_Equal 433 (Left => Model (New_Item), 434 Right => Model (Container), 435 Fst => Index_Type'First, 436 Lst => Last_Index (New_Item)) 437 438 -- Elements of Container are shifted 439 440 and M.Range_Shifted 441 (Left => Model (Container)'Old, 442 Right => Model (Container), 443 Fst => Index_Type'First, 444 Lst => Last_Index (Container)'Old, 445 Offset => Length (New_Item)); 446 447 procedure Prepend (Container : in out Vector; New_Item : Element_Type) with 448 Global => null, 449 Pre => Length (Container) < Capacity (Container), 450 Post => 451 Length (Container) = Length (Container)'Old + 1 452 453 -- Container now has New_Item at Index_Type'First 454 455 and Element (Model (Container), Index_Type'First) = New_Item 456 457 -- Elements of Container are shifted by 1 458 459 and M.Range_Shifted 460 (Left => Model (Container)'Old, 461 Right => Model (Container), 462 Fst => Index_Type'First, 463 Lst => Last_Index (Container)'Old, 464 Offset => 1); 465 466 procedure Prepend 467 (Container : in out Vector; 468 New_Item : Element_Type; 469 Count : Count_Type) 470 with 471 Global => null, 472 Pre => Length (Container) <= Capacity (Container) - Count, 473 Post => 474 Length (Container) = Length (Container)'Old + Count 475 476 -- New_Item is inserted Count times at the beginning of Container 477 478 and M.Constant_Range 479 (Container => Model (Container), 480 Fst => Index_Type'First, 481 Lst => Index_Type'First + Index_Type'Base (Count - 1), 482 Item => New_Item) 483 484 -- Elements of Container are shifted 485 486 and M.Range_Shifted 487 (Left => Model (Container)'Old, 488 Right => Model (Container), 489 Fst => Index_Type'First, 490 Lst => Last_Index (Container)'Old, 491 Offset => Count); 492 493 procedure Append (Container : in out Vector; New_Item : Vector) with 494 Global => null, 495 Pre => 496 Length (Container) <= Capacity (Container) - Length (New_Item), 497 Post => 498 Length (Container) = Length (Container)'Old + Length (New_Item) 499 500 -- The elements of Container are preserved 501 502 and Model (Container)'Old <= Model (Container) 503 504 -- Elements of New_Item are inserted at the end of Container 505 506 and (if Length (New_Item) > 0 then 507 M.Range_Shifted 508 (Left => Model (New_Item), 509 Right => Model (Container), 510 Fst => Index_Type'First, 511 Lst => Last_Index (New_Item), 512 Offset => 513 Count_Type 514 (Last_Index (Container)'Old - Index_Type'First + 1))); 515 516 procedure Append (Container : in out Vector; New_Item : Element_Type) with 517 Global => null, 518 Pre => Length (Container) < Capacity (Container), 519 Post => 520 Length (Container) = Length (Container)'Old + 1 521 522 -- Elements of Container are preserved 523 524 and Model (Container)'Old < Model (Container) 525 526 -- Container now has New_Item at the end of Container 527 528 and Element 529 (Model (Container), Last_Index (Container)'Old + 1) = New_Item; 530 531 procedure Append 532 (Container : in out Vector; 533 New_Item : Element_Type; 534 Count : Count_Type) 535 with 536 Global => null, 537 Pre => Length (Container) <= Capacity (Container) - Count, 538 Post => 539 Length (Container) = Length (Container)'Old + Count 540 541 -- Elements of Container are preserved 542 543 and Model (Container)'Old <= Model (Container) 544 545 -- New_Item is inserted Count times at the end of Container 546 547 and (if Count > 0 then 548 M.Constant_Range 549 (Container => Model (Container), 550 Fst => Last_Index (Container)'Old + 1, 551 Lst => 552 Last_Index (Container)'Old + Index_Type'Base (Count), 553 Item => New_Item)); 554 555 procedure Delete (Container : in out Vector; Index : Extended_Index) with 556 Global => null, 557 Pre => Index in First_Index (Container) .. Last_Index (Container), 558 Post => 559 Length (Container) = Length (Container)'Old - 1 560 561 -- Elements located before Index in Container are preserved 562 563 and M.Range_Equal 564 (Left => Model (Container)'Old, 565 Right => Model (Container), 566 Fst => Index_Type'First, 567 Lst => Index - 1) 568 569 -- Elements located after Index in Container are shifted by 1 570 571 and M.Range_Shifted 572 (Left => Model (Container), 573 Right => Model (Container)'Old, 574 Fst => Index, 575 Lst => Last_Index (Container), 576 Offset => 1); 577 578 procedure Delete 579 (Container : in out Vector; 580 Index : Extended_Index; 581 Count : Count_Type) 582 with 583 Global => null, 584 Pre => 585 Index in First_Index (Container) .. Last_Index (Container), 586 Post => 587 Length (Container) in 588 Length (Container)'Old - Count .. Length (Container)'Old 589 590 -- The elements of Container located before Index are preserved. 591 592 and M.Range_Equal 593 (Left => Model (Container)'Old, 594 Right => Model (Container), 595 Fst => Index_Type'First, 596 Lst => Index - 1), 597 598 Contract_Cases => 599 600 -- All the elements after Position have been erased 601 602 (Length (Container) - Count <= Count_Type (Index - Index_Type'First) => 603 Length (Container) = Count_Type (Index - Index_Type'First), 604 605 others => 606 Length (Container) = Length (Container)'Old - Count 607 608 -- Other elements are shifted by Count 609 610 and M.Range_Shifted 611 (Left => Model (Container), 612 Right => Model (Container)'Old, 613 Fst => Index, 614 Lst => Last_Index (Container), 615 Offset => Count)); 616 617 procedure Delete_First (Container : in out Vector) with 618 Global => null, 619 Pre => Length (Container) > 0, 620 Post => 621 Length (Container) = Length (Container)'Old - 1 622 623 -- Elements of Container are shifted by 1 624 625 and M.Range_Shifted 626 (Left => Model (Container), 627 Right => Model (Container)'Old, 628 Fst => Index_Type'First, 629 Lst => Last_Index (Container), 630 Offset => 1); 631 632 procedure Delete_First (Container : in out Vector; Count : Count_Type) with 633 Global => null, 634 Contract_Cases => 635 636 -- All the elements of Container have been erased 637 638 (Length (Container) <= Count => Length (Container) = 0, 639 640 others => 641 Length (Container) = Length (Container)'Old - Count 642 643 -- Elements of Container are shifted by Count 644 645 and M.Range_Shifted 646 (Left => Model (Container), 647 Right => Model (Container)'Old, 648 Fst => Index_Type'First, 649 Lst => Last_Index (Container), 650 Offset => Count)); 651 652 procedure Delete_Last (Container : in out Vector) with 653 Global => null, 654 Pre => Length (Container) > 0, 655 Post => 656 Length (Container) = Length (Container)'Old - 1 657 658 -- Elements of Container are preserved 659 660 and Model (Container) < Model (Container)'Old; 661 662 procedure Delete_Last (Container : in out Vector; Count : Count_Type) with 663 Global => null, 664 Contract_Cases => 665 666 -- All the elements after Position have been erased 667 668 (Length (Container) <= Count => Length (Container) = 0, 669 670 others => 671 Length (Container) = Length (Container)'Old - Count 672 673 -- The elements of Container are preserved 674 675 and Model (Container) <= Model (Container)'Old); 676 677 procedure Reverse_Elements (Container : in out Vector) with 678 Global => null, 679 Post => M_Elements_Reversed (Model (Container)'Old, Model (Container)); 680 681 procedure Swap 682 (Container : in out Vector; 683 I : Index_Type; 684 J : Index_Type) 685 with 686 Global => null, 687 Pre => 688 I in First_Index (Container) .. Last_Index (Container) 689 and then J in First_Index (Container) .. Last_Index (Container), 690 Post => 691 M_Elements_Swapped (Model (Container)'Old, Model (Container), I, J); 692 693 function First_Index (Container : Vector) return Index_Type with 694 Global => null, 695 Post => First_Index'Result = Index_Type'First; 696 pragma Annotate (GNATprove, Inline_For_Proof, First_Index); 697 698 function First_Element (Container : Vector) return Element_Type with 699 Global => null, 700 Pre => not Is_Empty (Container), 701 Post => 702 First_Element'Result = Element (Model (Container), Index_Type'First); 703 pragma Annotate (GNATprove, Inline_For_Proof, First_Element); 704 705 function Last_Index (Container : Vector) return Extended_Index with 706 Global => null, 707 Post => Last_Index'Result = M.Last (Model (Container)); 708 pragma Annotate (GNATprove, Inline_For_Proof, Last_Index); 709 710 function Last_Element (Container : Vector) return Element_Type with 711 Global => null, 712 Pre => not Is_Empty (Container), 713 Post => 714 Last_Element'Result = 715 Element (Model (Container), Last_Index (Container)); 716 pragma Annotate (GNATprove, Inline_For_Proof, Last_Element); 717 718 function Find_Index 719 (Container : Vector; 720 Item : Element_Type; 721 Index : Index_Type := Index_Type'First) return Extended_Index 722 with 723 Global => null, 724 Contract_Cases => 725 726 -- If Item is not contained in Container after Index, Find_Index 727 -- returns No_Index. 728 729 (Index > Last_Index (Container) 730 or else not M.Contains 731 (Container => Model (Container), 732 Fst => Index, 733 Lst => Last_Index (Container), 734 Item => Item) 735 => 736 Find_Index'Result = No_Index, 737 738 -- Otherwise, Find_Index returns a valid index greater than Index 739 740 others => 741 Find_Index'Result in Index .. Last_Index (Container) 742 743 -- The element at this index in Container is Item 744 745 and Element (Model (Container), Find_Index'Result) = Item 746 747 -- It is the first occurrence of Item after Index in Container 748 749 and not M.Contains 750 (Container => Model (Container), 751 Fst => Index, 752 Lst => Find_Index'Result - 1, 753 Item => Item)); 754 755 function Reverse_Find_Index 756 (Container : Vector; 757 Item : Element_Type; 758 Index : Index_Type := Index_Type'Last) return Extended_Index 759 with 760 Global => null, 761 Contract_Cases => 762 763 -- If Item is not contained in Container before Index, 764 -- Reverse_Find_Index returns No_Index. 765 766 (not M.Contains 767 (Container => Model (Container), 768 Fst => Index_Type'First, 769 Lst => (if Index <= Last_Index (Container) then Index 770 else Last_Index (Container)), 771 Item => Item) 772 => 773 Reverse_Find_Index'Result = No_Index, 774 775 -- Otherwise, Reverse_Find_Index returns a valid index smaller than 776 -- Index 777 778 others => 779 Reverse_Find_Index'Result in Index_Type'First .. Index 780 and Reverse_Find_Index'Result <= Last_Index (Container) 781 782 -- The element at this index in Container is Item 783 784 and Element (Model (Container), Reverse_Find_Index'Result) = Item 785 786 -- It is the last occurrence of Item before Index in Container 787 788 and not M.Contains 789 (Container => Model (Container), 790 Fst => Reverse_Find_Index'Result + 1, 791 Lst => 792 (if Index <= Last_Index (Container) then 793 Index 794 else 795 Last_Index (Container)), 796 Item => Item)); 797 798 function Contains 799 (Container : Vector; 800 Item : Element_Type) return Boolean 801 with 802 Global => null, 803 Post => 804 Contains'Result = 805 M.Contains 806 (Container => Model (Container), 807 Fst => Index_Type'First, 808 Lst => Last_Index (Container), 809 Item => Item); 810 811 function Has_Element 812 (Container : Vector; 813 Position : Extended_Index) return Boolean 814 with 815 Global => null, 816 Post => 817 Has_Element'Result = 818 (Position in Index_Type'First .. Last_Index (Container)); 819 pragma Annotate (GNATprove, Inline_For_Proof, Has_Element); 820 821 generic 822 with function "<" (Left, Right : Element_Type) return Boolean is <>; 823 package Generic_Sorting with SPARK_Mode is 824 825 package Formal_Model with Ghost is 826 827 function M_Elements_Sorted (Container : M.Sequence) return Boolean 828 with 829 Global => null, 830 Post => 831 M_Elements_Sorted'Result = 832 (for all I in Index_Type'First .. M.Last (Container) => 833 (for all J in I .. M.Last (Container) => 834 Element (Container, I) = Element (Container, J) 835 or Element (Container, I) < Element (Container, J))); 836 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted); 837 838 end Formal_Model; 839 use Formal_Model; 840 841 function Is_Sorted (Container : Vector) return Boolean with 842 Global => null, 843 Post => Is_Sorted'Result = M_Elements_Sorted (Model (Container)); 844 845 procedure Sort (Container : in out Vector) with 846 Global => null, 847 Post => 848 Length (Container) = Length (Container)'Old 849 and M_Elements_Sorted (Model (Container)) 850 and M_Elements_Included 851 (Left => Model (Container)'Old, 852 L_Lst => Last_Index (Container), 853 Right => Model (Container), 854 R_Lst => Last_Index (Container)) 855 and M_Elements_Included 856 (Left => Model (Container), 857 L_Lst => Last_Index (Container), 858 Right => Model (Container)'Old, 859 R_Lst => Last_Index (Container)); 860 861 procedure Merge (Target : in out Vector; Source : in out Vector) with 862 -- Target and Source should not be aliased 863 Global => null, 864 Pre => Length (Source) <= Capacity (Target) - Length (Target), 865 Post => 866 Length (Target) = Length (Target)'Old + Length (Source)'Old 867 and Length (Source) = 0 868 and (if M_Elements_Sorted (Model (Target)'Old) 869 and M_Elements_Sorted (Model (Source)'Old) 870 then 871 M_Elements_Sorted (Model (Target))) 872 and M_Elements_Included 873 (Left => Model (Target)'Old, 874 L_Lst => Last_Index (Target)'Old, 875 Right => Model (Target), 876 R_Lst => Last_Index (Target)) 877 and M_Elements_Included 878 (Left => Model (Source)'Old, 879 L_Lst => Last_Index (Source)'Old, 880 Right => Model (Target), 881 R_Lst => Last_Index (Target)) 882 and M_Elements_In_Union 883 (Model (Target), 884 Model (Source)'Old, 885 Model (Target)'Old); 886 end Generic_Sorting; 887 888private 889 pragma SPARK_Mode (Off); 890 891 pragma Inline (First_Index); 892 pragma Inline (Last_Index); 893 pragma Inline (Element); 894 pragma Inline (First_Element); 895 pragma Inline (Last_Element); 896 pragma Inline (Replace_Element); 897 pragma Inline (Contains); 898 899 -- The implementation method is to instantiate Bounded_Holders to get a 900 -- definite type for Element_Type. 901 902 package Holders is new Bounded_Holders 903 (Element_Type, Max_Size_In_Storage_Elements, "="); 904 use Holders; 905 906 subtype Array_Index is Capacity_Range range 1 .. Capacity_Range'Last; 907 type Elements_Array is array (Array_Index range <>) of Holder; 908 function "=" (L, R : Elements_Array) return Boolean is abstract; 909 910 type Elements_Array_Ptr is access all Elements_Array; 911 912 type Vector (Capacity : Capacity_Range) is limited record 913 914 -- In the bounded case, the elements are stored in Elements. In the 915 -- unbounded case, the elements are initially stored in Elements, until 916 -- we run out of room, then we switch to Elements_Ptr. 917 918 Last : Extended_Index := No_Index; 919 Elements_Ptr : Elements_Array_Ptr := null; 920 Elements : aliased Elements_Array (1 .. Capacity); 921 end record; 922 923 -- The primary reason Vector is limited is that in the unbounded case, once 924 -- Elements_Ptr is in use, assignment statements won't work. "X := Y;" will 925 -- cause X and Y to share state; that is, X.Elements_Ptr = Y.Elements_Ptr, 926 -- so for example "Append (X, ...);" will modify BOTH X and Y. That would 927 -- allow SPARK to "prove" things that are false. We could fix that by 928 -- making Vector a controlled type, and override Adjust to make a deep 929 -- copy, but finalization is not allowed in SPARK. 930 -- 931 -- Note that (unfortunately) this means that 'Old and 'Loop_Entry are not 932 -- allowed on Vectors. 933 934 function Empty_Vector return Vector is 935 ((Capacity => 0, others => <>)); 936 937end Ada.Containers.Formal_Indefinite_Vectors; 938