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