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