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