1------------------------------------------------------------------------------ 2-- -- 3-- GNAT LIBRARY COMPONENTS -- 4-- -- 5-- ADA.CONTAINERS.FORMAL_DOUBLY_LINKED_LISTS -- 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 32with Ada.Containers.Functional_Vectors; 33with Ada.Containers.Functional_Maps; 34 35generic 36 type Element_Type is private; 37 38package Ada.Containers.Formal_Doubly_Linked_Lists with 39 SPARK_Mode 40is 41 pragma Annotate (CodePeer, Skip_Analysis); 42 43 type List (Capacity : Count_Type) is private with 44 Iterable => (First => First, 45 Next => Next, 46 Has_Element => Has_Element, 47 Element => Element), 48 Default_Initial_Condition => Is_Empty (List); 49 pragma Preelaborable_Initialization (List); 50 51 type Cursor is record 52 Node : Count_Type := 0; 53 end record; 54 55 No_Element : constant Cursor := Cursor'(Node => 0); 56 57 Empty_List : constant List; 58 59 function Length (Container : List) return Count_Type with 60 Global => null, 61 Post => Length'Result <= Container.Capacity; 62 63 pragma Unevaluated_Use_Of_Old (Allow); 64 65 package Formal_Model with Ghost is 66 subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last; 67 68 package M is new Ada.Containers.Functional_Vectors 69 (Index_Type => Positive_Count_Type, 70 Element_Type => Element_Type); 71 72 function "=" 73 (Left : M.Sequence; 74 Right : M.Sequence) return Boolean renames M."="; 75 76 function "<" 77 (Left : M.Sequence; 78 Right : M.Sequence) return Boolean renames M."<"; 79 80 function "<=" 81 (Left : M.Sequence; 82 Right : M.Sequence) return Boolean renames M."<="; 83 84 function M_Elements_In_Union 85 (Container : M.Sequence; 86 Left : M.Sequence; 87 Right : M.Sequence) return Boolean 88 -- The elements of Container are contained in either Left or Right 89 with 90 Global => null, 91 Post => 92 M_Elements_In_Union'Result = 93 (for all I in 1 .. M.Length (Container) => 94 (for some J in 1 .. M.Length (Left) => 95 Element (Container, I) = Element (Left, J)) 96 or (for some J in 1 .. M.Length (Right) => 97 Element (Container, I) = Element (Right, J))); 98 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_In_Union); 99 100 function M_Elements_Included 101 (Left : M.Sequence; 102 L_Fst : Positive_Count_Type := 1; 103 L_Lst : Count_Type; 104 Right : M.Sequence; 105 R_Fst : Positive_Count_Type := 1; 106 R_Lst : Count_Type) return Boolean 107 -- The elements of the slice from L_Fst to L_Lst in Left are contained 108 -- in the slide from R_Fst to R_Lst in Right. 109 with 110 Global => null, 111 Pre => L_Lst <= M.Length (Left) and R_Lst <= M.Length (Right), 112 Post => 113 M_Elements_Included'Result = 114 (for all I in L_Fst .. L_Lst => 115 (for some J in R_Fst .. R_Lst => 116 Element (Left, I) = Element (Right, J))); 117 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Included); 118 119 function M_Elements_Reversed 120 (Left : M.Sequence; 121 Right : M.Sequence) return Boolean 122 -- Right is Left in reverse order 123 with 124 Global => null, 125 Post => 126 M_Elements_Reversed'Result = 127 (M.Length (Left) = M.Length (Right) 128 and (for all I in 1 .. M.Length (Left) => 129 Element (Left, I) = 130 Element (Right, M.Length (Left) - I + 1)) 131 and (for all I in 1 .. M.Length (Left) => 132 Element (Right, I) = 133 Element (Left, M.Length (Left) - I + 1))); 134 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Reversed); 135 136 function M_Elements_Swapped 137 (Left : M.Sequence; 138 Right : M.Sequence; 139 X : Positive_Count_Type; 140 Y : Positive_Count_Type) return Boolean 141 -- Elements stored at X and Y are reversed in Left and Right 142 with 143 Global => null, 144 Pre => X <= M.Length (Left) and Y <= M.Length (Left), 145 Post => 146 M_Elements_Swapped'Result = 147 (M.Length (Left) = M.Length (Right) 148 and Element (Left, X) = Element (Right, Y) 149 and Element (Left, Y) = Element (Right, X) 150 and M.Equal_Except (Left, Right, X, Y)); 151 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Swapped); 152 153 package P is new Ada.Containers.Functional_Maps 154 (Key_Type => Cursor, 155 Element_Type => Positive_Count_Type, 156 Equivalent_Keys => "=", 157 Enable_Handling_Of_Equivalence => False); 158 159 function "=" 160 (Left : P.Map; 161 Right : P.Map) return Boolean renames P."="; 162 163 function "<=" 164 (Left : P.Map; 165 Right : P.Map) return Boolean renames P."<="; 166 167 function P_Positions_Shifted 168 (Small : P.Map; 169 Big : P.Map; 170 Cut : Positive_Count_Type; 171 Count : Count_Type := 1) return Boolean 172 with 173 Global => null, 174 Post => 175 P_Positions_Shifted'Result = 176 177 -- Big contains all cursors of Small 178 179 (P.Keys_Included (Small, Big) 180 181 -- Cursors located before Cut are not moved, cursors located 182 -- after are shifted by Count. 183 184 and (for all I of Small => 185 (if P.Get (Small, I) < Cut then 186 P.Get (Big, I) = P.Get (Small, I) 187 else 188 P.Get (Big, I) - Count = P.Get (Small, I))) 189 190 -- New cursors of Big (if any) are between Cut and Cut - 1 + 191 -- Count. 192 193 and (for all I of Big => 194 P.Has_Key (Small, I) 195 or P.Get (Big, I) - Count in Cut - Count .. Cut - 1)); 196 197 function P_Positions_Swapped 198 (Left : P.Map; 199 Right : P.Map; 200 X : Cursor; 201 Y : Cursor) return Boolean 202 -- Left and Right contain the same cursors, but the positions of X and Y 203 -- are reversed. 204 with 205 Ghost, 206 Global => null, 207 Post => 208 P_Positions_Swapped'Result = 209 (P.Same_Keys (Left, Right) 210 and P.Elements_Equal_Except (Left, Right, X, Y) 211 and P.Has_Key (Left, X) 212 and P.Has_Key (Left, Y) 213 and P.Get (Left, X) = P.Get (Right, Y) 214 and P.Get (Left, Y) = P.Get (Right, X)); 215 216 function P_Positions_Truncated 217 (Small : P.Map; 218 Big : P.Map; 219 Cut : Positive_Count_Type; 220 Count : Count_Type := 1) return Boolean 221 with 222 Ghost, 223 Global => null, 224 Post => 225 P_Positions_Truncated'Result = 226 227 -- Big contains all cursors of Small at the same position 228 229 (Small <= Big 230 231 -- New cursors of Big (if any) are between Cut and Cut - 1 + 232 -- Count. 233 234 and (for all I of Big => 235 P.Has_Key (Small, I) 236 or P.Get (Big, I) - Count in Cut - Count .. Cut - 1)); 237 238 function Mapping_Preserved 239 (M_Left : M.Sequence; 240 M_Right : M.Sequence; 241 P_Left : P.Map; 242 P_Right : P.Map) return Boolean 243 with 244 Ghost, 245 Global => null, 246 Post => 247 (if Mapping_Preserved'Result then 248 249 -- Left and Right contain the same cursors 250 251 P.Same_Keys (P_Left, P_Right) 252 253 -- Mappings from cursors to elements induced by M_Left, P_Left 254 -- and M_Right, P_Right are the same. 255 256 and (for all C of P_Left => 257 M.Get (M_Left, P.Get (P_Left, C)) = 258 M.Get (M_Right, P.Get (P_Right, C)))); 259 260 function Model (Container : List) return M.Sequence with 261 -- The high-level model of a list is a sequence of elements. Cursors are 262 -- not represented in this model. 263 264 Ghost, 265 Global => null, 266 Post => M.Length (Model'Result) = Length (Container); 267 pragma Annotate (GNATprove, Iterable_For_Proof, "Model", Model); 268 269 function Positions (Container : List) return P.Map with 270 -- The Positions map is used to model cursors. It only contains valid 271 -- cursors and map them to their position in the container. 272 273 Ghost, 274 Global => null, 275 Post => 276 not P.Has_Key (Positions'Result, No_Element) 277 278 -- Positions of cursors are smaller than the container's length. 279 280 and then 281 (for all I of Positions'Result => 282 P.Get (Positions'Result, I) in 1 .. Length (Container) 283 284 -- No two cursors have the same position. Note that we do not 285 -- state that there is a cursor in the map for each position, as 286 -- it is rarely needed. 287 288 and then 289 (for all J of Positions'Result => 290 (if P.Get (Positions'Result, I) = P.Get (Positions'Result, J) 291 then I = J))); 292 293 procedure Lift_Abstraction_Level (Container : List) with 294 -- Lift_Abstraction_Level is a ghost procedure that does nothing but 295 -- assume that we can access to the same elements by iterating over 296 -- positions or cursors. 297 -- This information is not generally useful except when switching from 298 -- a low-level cursor-aware view of a container to a high-level 299 -- position-based view. 300 301 Ghost, 302 Global => null, 303 Post => 304 (for all Elt of Model (Container) => 305 (for some I of Positions (Container) => 306 M.Get (Model (Container), P.Get (Positions (Container), I)) = 307 Elt)); 308 309 function Element 310 (S : M.Sequence; 311 I : Count_Type) return Element_Type renames M.Get; 312 -- To improve readability of contracts, we rename the function used to 313 -- access an element in the model to Element. 314 315 end Formal_Model; 316 use Formal_Model; 317 318 function "=" (Left, Right : List) return Boolean with 319 Global => null, 320 Post => "="'Result = (Model (Left) = Model (Right)); 321 322 function Is_Empty (Container : List) return Boolean with 323 Global => null, 324 Post => Is_Empty'Result = (Length (Container) = 0); 325 326 procedure Clear (Container : in out List) with 327 Global => null, 328 Post => Length (Container) = 0; 329 330 procedure Assign (Target : in out List; Source : List) with 331 Global => null, 332 Pre => Target.Capacity >= Length (Source), 333 Post => Model (Target) = Model (Source); 334 335 function Copy (Source : List; Capacity : Count_Type := 0) return List with 336 Global => null, 337 Pre => Capacity = 0 or else Capacity >= Source.Capacity, 338 Post => 339 Model (Copy'Result) = Model (Source) 340 and Positions (Copy'Result) = Positions (Source) 341 and (if Capacity = 0 then 342 Copy'Result.Capacity = Source.Capacity 343 else 344 Copy'Result.Capacity = Capacity); 345 346 function Element 347 (Container : List; 348 Position : Cursor) return Element_Type 349 with 350 Global => null, 351 Pre => Has_Element (Container, Position), 352 Post => 353 Element'Result = 354 Element (Model (Container), P.Get (Positions (Container), Position)); 355 pragma Annotate (GNATprove, Inline_For_Proof, Element); 356 357 procedure Replace_Element 358 (Container : in out List; 359 Position : Cursor; 360 New_Item : Element_Type) 361 with 362 Global => null, 363 Pre => Has_Element (Container, Position), 364 Post => 365 Length (Container) = Length (Container)'Old 366 367 -- Cursors are preserved 368 369 and Positions (Container)'Old = Positions (Container) 370 371 -- The element at the position of Position in Container is New_Item 372 373 and Element 374 (Model (Container), 375 P.Get (Positions (Container), Position)) = New_Item 376 377 -- Other elements are preserved 378 379 and M.Equal_Except 380 (Model (Container)'Old, 381 Model (Container), 382 P.Get (Positions (Container), Position)); 383 384 procedure Move (Target : in out List; Source : in out List) with 385 Global => null, 386 Pre => Target.Capacity >= Length (Source), 387 Post => Model (Target) = Model (Source'Old) and Length (Source) = 0; 388 389 procedure Insert 390 (Container : in out List; 391 Before : Cursor; 392 New_Item : Element_Type) 393 with 394 Global => null, 395 Pre => 396 Length (Container) < Container.Capacity 397 and then (Has_Element (Container, Before) 398 or else Before = No_Element), 399 Post => Length (Container) = Length (Container)'Old + 1, 400 Contract_Cases => 401 (Before = No_Element => 402 403 -- Positions contains a new mapping from the last cursor of 404 -- Container to its length. 405 406 P.Get (Positions (Container), Last (Container)) = Length (Container) 407 408 -- Other cursors come from Container'Old 409 410 and P.Keys_Included_Except 411 (Left => Positions (Container), 412 Right => Positions (Container)'Old, 413 New_Key => Last (Container)) 414 415 -- Cursors of Container'Old keep the same position 416 417 and Positions (Container)'Old <= Positions (Container) 418 419 -- Model contains a new element New_Item at the end 420 421 and Element (Model (Container), Length (Container)) = New_Item 422 423 -- Elements of Container'Old are preserved 424 425 and Model (Container)'Old <= Model (Container), 426 427 others => 428 429 -- The elements of Container located before Before are preserved 430 431 M.Range_Equal 432 (Left => Model (Container)'Old, 433 Right => Model (Container), 434 Fst => 1, 435 Lst => P.Get (Positions (Container)'Old, Before) - 1) 436 437 -- Other elements are shifted by 1 438 439 and M.Range_Shifted 440 (Left => Model (Container)'Old, 441 Right => Model (Container), 442 Fst => P.Get (Positions (Container)'Old, Before), 443 Lst => Length (Container)'Old, 444 Offset => 1) 445 446 -- New_Item is stored at the previous position of Before in 447 -- Container. 448 449 and Element 450 (Model (Container), 451 P.Get (Positions (Container)'Old, Before)) = New_Item 452 453 -- A new cursor has been inserted at position Before in Container 454 455 and P_Positions_Shifted 456 (Positions (Container)'Old, 457 Positions (Container), 458 Cut => P.Get (Positions (Container)'Old, Before))); 459 460 procedure Insert 461 (Container : in out List; 462 Before : Cursor; 463 New_Item : Element_Type; 464 Count : Count_Type) 465 with 466 Global => null, 467 Pre => 468 Length (Container) <= Container.Capacity - Count 469 and then (Has_Element (Container, Before) 470 or else Before = No_Element), 471 Post => Length (Container) = Length (Container)'Old + Count, 472 Contract_Cases => 473 (Before = No_Element => 474 475 -- The elements of Container are preserved 476 477 M.Range_Equal 478 (Left => Model (Container)'Old, 479 Right => Model (Container), 480 Fst => 1, 481 Lst => Length (Container)'Old) 482 483 -- Container contains Count times New_Item at the end 484 485 and (if Count > 0 then 486 M.Constant_Range 487 (Container => Model (Container), 488 Fst => Length (Container)'Old + 1, 489 Lst => Length (Container), 490 Item => New_Item)) 491 492 -- Container contains Count times New_Item at the end 493 494 and M.Constant_Range 495 (Container => Model (Container), 496 Fst => Length (Container)'Old + 1, 497 Lst => Length (Container), 498 Item => New_Item) 499 500 -- A Count cursors have been inserted at the end of Container 501 502 and P_Positions_Truncated 503 (Positions (Container)'Old, 504 Positions (Container), 505 Cut => Length (Container)'Old + 1, 506 Count => Count), 507 508 others => 509 510 -- The elements of Container located before Before are preserved 511 512 M.Range_Equal 513 (Left => Model (Container)'Old, 514 Right => Model (Container), 515 Fst => 1, 516 Lst => P.Get (Positions (Container)'Old, Before) - 1) 517 518 -- Other elements are shifted by Count 519 520 and M.Range_Shifted 521 (Left => Model (Container)'Old, 522 Right => Model (Container), 523 Fst => P.Get (Positions (Container)'Old, Before), 524 Lst => Length (Container)'Old, 525 Offset => Count) 526 527 -- Container contains Count times New_Item after position Before 528 529 and M.Constant_Range 530 (Container => Model (Container), 531 Fst => P.Get (Positions (Container)'Old, Before), 532 Lst => 533 P.Get (Positions (Container)'Old, Before) - 1 + Count, 534 Item => New_Item) 535 536 -- Count cursors have been inserted at position Before in 537 -- Container. 538 539 and P_Positions_Shifted 540 (Positions (Container)'Old, 541 Positions (Container), 542 Cut => P.Get (Positions (Container)'Old, Before), 543 Count => Count)); 544 545 procedure Insert 546 (Container : in out List; 547 Before : Cursor; 548 New_Item : Element_Type; 549 Position : out Cursor) 550 with 551 Global => null, 552 Pre => 553 Length (Container) < Container.Capacity 554 and then (Has_Element (Container, Before) 555 or else Before = No_Element), 556 Post => 557 Length (Container) = Length (Container)'Old + 1 558 559 -- Positions is valid in Container and it is located either before 560 -- Before if it is valid in Container or at the end if it is 561 -- No_Element. 562 563 and P.Has_Key (Positions (Container), Position) 564 and (if Before = No_Element then 565 P.Get (Positions (Container), Position) = Length (Container) 566 else 567 P.Get (Positions (Container), Position) = 568 P.Get (Positions (Container)'Old, Before)) 569 570 -- The elements of Container located before Position are preserved 571 572 and M.Range_Equal 573 (Left => Model (Container)'Old, 574 Right => Model (Container), 575 Fst => 1, 576 Lst => P.Get (Positions (Container), Position) - 1) 577 578 -- Other elements are shifted by 1 579 580 and M.Range_Shifted 581 (Left => Model (Container)'Old, 582 Right => Model (Container), 583 Fst => P.Get (Positions (Container), Position), 584 Lst => Length (Container)'Old, 585 Offset => 1) 586 587 -- New_Item is stored at Position in Container 588 589 and Element 590 (Model (Container), 591 P.Get (Positions (Container), Position)) = New_Item 592 593 -- A new cursor has been inserted at position Position in Container 594 595 and P_Positions_Shifted 596 (Positions (Container)'Old, 597 Positions (Container), 598 Cut => P.Get (Positions (Container), Position)); 599 600 procedure Insert 601 (Container : in out List; 602 Before : Cursor; 603 New_Item : Element_Type; 604 Position : out Cursor; 605 Count : Count_Type) 606 with 607 Global => null, 608 Pre => 609 Length (Container) <= Container.Capacity - Count 610 and then (Has_Element (Container, Before) 611 or else Before = No_Element), 612 Post => Length (Container) = Length (Container)'Old + Count, 613 Contract_Cases => 614 (Count = 0 => 615 Position = Before 616 and Model (Container) = Model (Container)'Old 617 and Positions (Container) = Positions (Container)'Old, 618 619 others => 620 621 -- Positions is valid in Container and it is located either before 622 -- Before if it is valid in Container or at the end if it is 623 -- No_Element. 624 625 P.Has_Key (Positions (Container), Position) 626 and (if Before = No_Element then 627 P.Get (Positions (Container), Position) = 628 Length (Container)'Old + 1 629 else 630 P.Get (Positions (Container), Position) = 631 P.Get (Positions (Container)'Old, Before)) 632 633 -- The elements of Container located before Position are preserved 634 635 and M.Range_Equal 636 (Left => Model (Container)'Old, 637 Right => Model (Container), 638 Fst => 1, 639 Lst => P.Get (Positions (Container), Position) - 1) 640 641 -- Other elements are shifted by Count 642 643 and M.Range_Shifted 644 (Left => Model (Container)'Old, 645 Right => Model (Container), 646 Fst => P.Get (Positions (Container), Position), 647 Lst => Length (Container)'Old, 648 Offset => Count) 649 650 -- Container contains Count times New_Item after position Position 651 652 and M.Constant_Range 653 (Container => Model (Container), 654 Fst => P.Get (Positions (Container), Position), 655 Lst => 656 P.Get (Positions (Container), Position) - 1 + Count, 657 Item => New_Item) 658 659 -- Count cursor have been inserted at Position in Container 660 661 and P_Positions_Shifted 662 (Positions (Container)'Old, 663 Positions (Container), 664 Cut => P.Get (Positions (Container), Position), 665 Count => Count)); 666 667 procedure Prepend (Container : in out List; New_Item : Element_Type) with 668 Global => null, 669 Pre => Length (Container) < Container.Capacity, 670 Post => 671 Length (Container) = Length (Container)'Old + 1 672 673 -- Elements are shifted by 1 674 675 and M.Range_Shifted 676 (Left => Model (Container)'Old, 677 Right => Model (Container), 678 Fst => 1, 679 Lst => Length (Container)'Old, 680 Offset => 1) 681 682 -- New_Item is the first element of Container 683 684 and Element (Model (Container), 1) = New_Item 685 686 -- A new cursor has been inserted at the beginning of Container 687 688 and P_Positions_Shifted 689 (Positions (Container)'Old, 690 Positions (Container), 691 Cut => 1); 692 693 procedure Prepend 694 (Container : in out List; 695 New_Item : Element_Type; 696 Count : Count_Type) 697 with 698 Global => null, 699 Pre => Length (Container) <= Container.Capacity - Count, 700 Post => 701 Length (Container) = Length (Container)'Old + Count 702 703 -- Elements are shifted by Count 704 705 and M.Range_Shifted 706 (Left => Model (Container)'Old, 707 Right => Model (Container), 708 Fst => 1, 709 Lst => Length (Container)'Old, 710 Offset => Count) 711 712 -- Container starts with Count times New_Item 713 714 and M.Constant_Range 715 (Container => Model (Container), 716 Fst => 1, 717 Lst => Count, 718 Item => New_Item) 719 720 -- Count cursors have been inserted at the beginning of Container 721 722 and P_Positions_Shifted 723 (Positions (Container)'Old, 724 Positions (Container), 725 Cut => 1, 726 Count => Count); 727 728 procedure Append (Container : in out List; New_Item : Element_Type) with 729 Global => null, 730 Pre => Length (Container) < Container.Capacity, 731 Post => 732 Length (Container) = Length (Container)'Old + 1 733 734 -- Positions contains a new mapping from the last cursor of Container 735 -- to its length. 736 737 and P.Get (Positions (Container), Last (Container)) = 738 Length (Container) 739 740 -- Other cursors come from Container'Old 741 742 and P.Keys_Included_Except 743 (Left => Positions (Container), 744 Right => Positions (Container)'Old, 745 New_Key => Last (Container)) 746 747 -- Cursors of Container'Old keep the same position 748 749 and Positions (Container)'Old <= Positions (Container) 750 751 -- Model contains a new element New_Item at the end 752 753 and Element (Model (Container), Length (Container)) = New_Item 754 755 -- Elements of Container'Old are preserved 756 757 and Model (Container)'Old <= Model (Container); 758 759 procedure Append 760 (Container : in out List; 761 New_Item : Element_Type; 762 Count : Count_Type) 763 with 764 Global => null, 765 Pre => Length (Container) <= Container.Capacity - Count, 766 Post => 767 Length (Container) = Length (Container)'Old + Count 768 769 -- The elements of Container are preserved 770 771 and Model (Container)'Old <= Model (Container) 772 773 -- Container contains Count times New_Item at the end 774 775 and (if Count > 0 then 776 M.Constant_Range 777 (Container => Model (Container), 778 Fst => Length (Container)'Old + 1, 779 Lst => Length (Container), 780 Item => New_Item)) 781 782 -- Count cursors have been inserted at the end of Container 783 784 and P_Positions_Truncated 785 (Positions (Container)'Old, 786 Positions (Container), 787 Cut => Length (Container)'Old + 1, 788 Count => Count); 789 790 procedure Delete (Container : in out List; Position : in out Cursor) with 791 Global => null, 792 Pre => Has_Element (Container, Position), 793 Post => 794 Length (Container) = Length (Container)'Old - 1 795 796 -- Position is set to No_Element 797 798 and Position = No_Element 799 800 -- The elements of Container located before Position are preserved. 801 802 and M.Range_Equal 803 (Left => Model (Container)'Old, 804 Right => Model (Container), 805 Fst => 1, 806 Lst => P.Get (Positions (Container)'Old, Position'Old) - 1) 807 808 -- The elements located after Position are shifted by 1 809 810 and M.Range_Shifted 811 (Left => Model (Container), 812 Right => Model (Container)'Old, 813 Fst => P.Get (Positions (Container)'Old, Position'Old), 814 Lst => Length (Container), 815 Offset => 1) 816 817 -- Position has been removed from Container 818 819 and P_Positions_Shifted 820 (Positions (Container), 821 Positions (Container)'Old, 822 Cut => P.Get (Positions (Container)'Old, Position'Old)); 823 824 procedure Delete 825 (Container : in out List; 826 Position : in out Cursor; 827 Count : Count_Type) 828 with 829 Global => null, 830 Pre => Has_Element (Container, Position), 831 Post => 832 Length (Container) in 833 Length (Container)'Old - Count .. Length (Container)'Old 834 835 -- Position is set to No_Element 836 837 and Position = No_Element 838 839 -- The elements of Container located before Position are preserved. 840 841 and M.Range_Equal 842 (Left => Model (Container)'Old, 843 Right => Model (Container), 844 Fst => 1, 845 Lst => P.Get (Positions (Container)'Old, Position'Old) - 1), 846 847 Contract_Cases => 848 849 -- All the elements after Position have been erased 850 851 (Length (Container) - Count < P.Get (Positions (Container), Position) => 852 Length (Container) = 853 P.Get (Positions (Container)'Old, Position'Old) - 1 854 855 -- At most Count cursors have been removed at the end of Container 856 857 and P_Positions_Truncated 858 (Positions (Container), 859 Positions (Container)'Old, 860 Cut => P.Get (Positions (Container)'Old, Position'Old), 861 Count => Count), 862 863 others => 864 Length (Container) = Length (Container)'Old - Count 865 866 -- Other elements are shifted by Count 867 868 and M.Range_Shifted 869 (Left => Model (Container), 870 Right => Model (Container)'Old, 871 Fst => P.Get (Positions (Container)'Old, Position'Old), 872 Lst => Length (Container), 873 Offset => Count) 874 875 -- Count cursors have been removed from Container at Position 876 877 and P_Positions_Shifted 878 (Positions (Container), 879 Positions (Container)'Old, 880 Cut => P.Get (Positions (Container)'Old, Position'Old), 881 Count => Count)); 882 883 procedure Delete_First (Container : in out List) with 884 Global => null, 885 Pre => not Is_Empty (Container), 886 Post => 887 Length (Container) = Length (Container)'Old - 1 888 889 -- The elements of Container are shifted by 1 890 891 and M.Range_Shifted 892 (Left => Model (Container), 893 Right => Model (Container)'Old, 894 Fst => 1, 895 Lst => Length (Container), 896 Offset => 1) 897 898 -- The first cursor of Container has been removed 899 900 and P_Positions_Shifted 901 (Positions (Container), 902 Positions (Container)'Old, 903 Cut => 1); 904 905 procedure Delete_First (Container : in out List; Count : Count_Type) with 906 Global => null, 907 Contract_Cases => 908 909 -- All the elements of Container have been erased 910 911 (Length (Container) <= Count => 912 Length (Container) = 0, 913 914 others => 915 Length (Container) = Length (Container)'Old - Count 916 917 -- Elements of Container are shifted by Count 918 919 and M.Range_Shifted 920 (Left => Model (Container), 921 Right => Model (Container)'Old, 922 Fst => 1, 923 Lst => Length (Container), 924 Offset => Count) 925 926 -- The first Count cursors have been removed from Container 927 928 and P_Positions_Shifted 929 (Positions (Container), 930 Positions (Container)'Old, 931 Cut => 1, 932 Count => Count)); 933 934 procedure Delete_Last (Container : in out List) with 935 Global => null, 936 Pre => not Is_Empty (Container), 937 Post => 938 Length (Container) = Length (Container)'Old - 1 939 940 -- The elements of Container are preserved 941 942 and Model (Container) <= Model (Container)'Old 943 944 -- The last cursor of Container has been removed 945 946 and not P.Has_Key (Positions (Container), Last (Container)'Old) 947 948 -- Other cursors are still valid 949 950 and P.Keys_Included_Except 951 (Left => Positions (Container)'Old, 952 Right => Positions (Container)'Old, 953 New_Key => Last (Container)'Old) 954 955 -- The positions of other cursors are preserved 956 957 and Positions (Container) <= Positions (Container)'Old; 958 959 procedure Delete_Last (Container : in out List; Count : Count_Type) with 960 Global => null, 961 Contract_Cases => 962 963 -- All the elements of Container have been erased 964 965 (Length (Container) <= Count => 966 Length (Container) = 0, 967 968 others => 969 Length (Container) = Length (Container)'Old - Count 970 971 -- The elements of Container are preserved 972 973 and Model (Container) <= Model (Container)'Old 974 975 -- At most Count cursors have been removed at the end of Container 976 977 and P_Positions_Truncated 978 (Positions (Container), 979 Positions (Container)'Old, 980 Cut => Length (Container) + 1, 981 Count => Count)); 982 983 procedure Reverse_Elements (Container : in out List) with 984 Global => null, 985 Post => M_Elements_Reversed (Model (Container)'Old, Model (Container)); 986 987 procedure Swap 988 (Container : in out List; 989 I : Cursor; 990 J : Cursor) 991 with 992 Global => null, 993 Pre => Has_Element (Container, I) and then Has_Element (Container, J), 994 Post => 995 M_Elements_Swapped 996 (Model (Container)'Old, 997 Model (Container), 998 X => P.Get (Positions (Container)'Old, I), 999 Y => P.Get (Positions (Container)'Old, J)) 1000 1001 and Positions (Container) = Positions (Container)'Old; 1002 1003 procedure Swap_Links 1004 (Container : in out List; 1005 I : Cursor; 1006 J : Cursor) 1007 with 1008 Global => null, 1009 Pre => Has_Element (Container, I) and then Has_Element (Container, J), 1010 Post => 1011 M_Elements_Swapped 1012 (Model (Container'Old), 1013 Model (Container), 1014 X => P.Get (Positions (Container)'Old, I), 1015 Y => P.Get (Positions (Container)'Old, J)) 1016 and P_Positions_Swapped 1017 (Positions (Container)'Old, Positions (Container), I, J); 1018 1019 procedure Splice 1020 (Target : in out List; 1021 Before : Cursor; 1022 Source : in out List) 1023 -- Target and Source should not be aliased 1024 with 1025 Global => null, 1026 Pre => 1027 Length (Source) <= Target.Capacity - Length (Target) 1028 and then (Has_Element (Target, Before) 1029 or else Before = No_Element), 1030 Post => 1031 Length (Source) = 0 1032 and Length (Target) = Length (Target)'Old + Length (Source)'Old, 1033 Contract_Cases => 1034 (Before = No_Element => 1035 1036 -- The elements of Target are preserved 1037 1038 M.Range_Equal 1039 (Left => Model (Target)'Old, 1040 Right => Model (Target), 1041 Fst => 1, 1042 Lst => Length (Target)'Old) 1043 1044 -- The elements of Source are appended to target, the order is not 1045 -- specified. 1046 1047 and M_Elements_Included 1048 (Left => Model (Source)'Old, 1049 L_Lst => Length (Source)'Old, 1050 Right => Model (Target), 1051 R_Fst => Length (Target)'Old + 1, 1052 R_Lst => Length (Target)) 1053 1054 and M_Elements_Included 1055 (Left => Model (Target), 1056 L_Fst => Length (Target)'Old + 1, 1057 L_Lst => Length (Target), 1058 Right => Model (Source)'Old, 1059 R_Lst => Length (Source)'Old) 1060 1061 -- Cursors have been inserted at the end of Target 1062 1063 and P_Positions_Truncated 1064 (Positions (Target)'Old, 1065 Positions (Target), 1066 Cut => Length (Target)'Old + 1, 1067 Count => Length (Source)'Old), 1068 1069 others => 1070 1071 -- The elements of Target located before Before are preserved 1072 1073 M.Range_Equal 1074 (Left => Model (Target)'Old, 1075 Right => Model (Target), 1076 Fst => 1, 1077 Lst => P.Get (Positions (Target)'Old, Before) - 1) 1078 1079 -- The elements of Source are inserted before Before, the order is 1080 -- not specified. 1081 1082 and M_Elements_Included 1083 (Left => Model (Source)'Old, 1084 L_Lst => Length (Source)'Old, 1085 Right => Model (Target), 1086 R_Fst => P.Get (Positions (Target)'Old, Before), 1087 R_Lst => 1088 P.Get (Positions (Target)'Old, Before) - 1 + 1089 Length (Source)'Old) 1090 1091 and M_Elements_Included 1092 (Left => Model (Target), 1093 L_Fst => P.Get (Positions (Target)'Old, Before), 1094 L_Lst => 1095 P.Get (Positions (Target)'Old, Before) - 1 + 1096 Length (Source)'Old, 1097 Right => Model (Source)'Old, 1098 R_Lst => Length (Source)'Old) 1099 1100 -- Other elements are shifted by the length of Source 1101 1102 and M.Range_Shifted 1103 (Left => Model (Target)'Old, 1104 Right => Model (Target), 1105 Fst => P.Get (Positions (Target)'Old, Before), 1106 Lst => Length (Target)'Old, 1107 Offset => Length (Source)'Old) 1108 1109 -- Cursors have been inserted at position Before in Target 1110 1111 and P_Positions_Shifted 1112 (Positions (Target)'Old, 1113 Positions (Target), 1114 Cut => P.Get (Positions (Target)'Old, Before), 1115 Count => Length (Source)'Old)); 1116 1117 procedure Splice 1118 (Target : in out List; 1119 Before : Cursor; 1120 Source : in out List; 1121 Position : in out Cursor) 1122 -- Target and Source should not be aliased 1123 with 1124 Global => null, 1125 Pre => 1126 (Has_Element (Target, Before) or else Before = No_Element) 1127 and then Has_Element (Source, Position) 1128 and then Length (Target) < Target.Capacity, 1129 Post => 1130 Length (Target) = Length (Target)'Old + 1 1131 and Length (Source) = Length (Source)'Old - 1 1132 1133 -- The elements of Source located before Position are preserved 1134 1135 and M.Range_Equal 1136 (Left => Model (Source)'Old, 1137 Right => Model (Source), 1138 Fst => 1, 1139 Lst => P.Get (Positions (Source)'Old, Position'Old) - 1) 1140 1141 -- The elements located after Position are shifted by 1 1142 1143 and M.Range_Shifted 1144 (Left => Model (Source)'Old, 1145 Right => Model (Source), 1146 Fst => P.Get (Positions (Source)'Old, Position'Old) + 1, 1147 Lst => Length (Source)'Old, 1148 Offset => -1) 1149 1150 -- Position has been removed from Source 1151 1152 and P_Positions_Shifted 1153 (Positions (Source), 1154 Positions (Source)'Old, 1155 Cut => P.Get (Positions (Source)'Old, Position'Old)) 1156 1157 -- Positions is valid in Target and it is located either before 1158 -- Before if it is valid in Target or at the end if it is No_Element. 1159 1160 and P.Has_Key (Positions (Target), Position) 1161 and (if Before = No_Element then 1162 P.Get (Positions (Target), Position) = Length (Target) 1163 else 1164 P.Get (Positions (Target), Position) = 1165 P.Get (Positions (Target)'Old, Before)) 1166 1167 -- The elements of Target located before Position are preserved 1168 1169 and M.Range_Equal 1170 (Left => Model (Target)'Old, 1171 Right => Model (Target), 1172 Fst => 1, 1173 Lst => P.Get (Positions (Target), Position) - 1) 1174 1175 -- Other elements are shifted by 1 1176 1177 and M.Range_Shifted 1178 (Left => Model (Target)'Old, 1179 Right => Model (Target), 1180 Fst => P.Get (Positions (Target), Position), 1181 Lst => Length (Target)'Old, 1182 Offset => 1) 1183 1184 -- The element located at Position in Source is moved to Target 1185 1186 and Element (Model (Target), 1187 P.Get (Positions (Target), Position)) = 1188 Element (Model (Source)'Old, 1189 P.Get (Positions (Source)'Old, Position'Old)) 1190 1191 -- A new cursor has been inserted at position Position in Target 1192 1193 and P_Positions_Shifted 1194 (Positions (Target)'Old, 1195 Positions (Target), 1196 Cut => P.Get (Positions (Target), Position)); 1197 1198 procedure Splice 1199 (Container : in out List; 1200 Before : Cursor; 1201 Position : Cursor) 1202 with 1203 Global => null, 1204 Pre => 1205 (Has_Element (Container, Before) or else Before = No_Element) 1206 and then Has_Element (Container, Position), 1207 Post => Length (Container) = Length (Container)'Old, 1208 Contract_Cases => 1209 (Before = Position => 1210 Model (Container) = Model (Container)'Old 1211 and Positions (Container) = Positions (Container)'Old, 1212 1213 Before = No_Element => 1214 1215 -- The elements located before Position are preserved 1216 1217 M.Range_Equal 1218 (Left => Model (Container)'Old, 1219 Right => Model (Container), 1220 Fst => 1, 1221 Lst => P.Get (Positions (Container)'Old, Position) - 1) 1222 1223 -- The elements located after Position are shifted by 1 1224 1225 and M.Range_Shifted 1226 (Left => Model (Container)'Old, 1227 Right => Model (Container), 1228 Fst => P.Get (Positions (Container)'Old, Position) + 1, 1229 Lst => Length (Container)'Old, 1230 Offset => -1) 1231 1232 -- The last element of Container is the one that was previously at 1233 -- Position. 1234 1235 and Element (Model (Container), 1236 Length (Container)) = 1237 Element (Model (Container)'Old, 1238 P.Get (Positions (Container)'Old, Position)) 1239 1240 -- Cursors from Container continue designating the same elements 1241 1242 and Mapping_Preserved 1243 (M_Left => Model (Container)'Old, 1244 M_Right => Model (Container), 1245 P_Left => Positions (Container)'Old, 1246 P_Right => Positions (Container)), 1247 1248 others => 1249 1250 -- The elements located before Position and Before are preserved 1251 1252 M.Range_Equal 1253 (Left => Model (Container)'Old, 1254 Right => Model (Container), 1255 Fst => 1, 1256 Lst => 1257 Count_Type'Min 1258 (P.Get (Positions (Container)'Old, Position) - 1, 1259 P.Get (Positions (Container)'Old, Before) - 1)) 1260 1261 -- The elements located after Position and Before are preserved 1262 1263 and M.Range_Equal 1264 (Left => Model (Container)'Old, 1265 Right => Model (Container), 1266 Fst => 1267 Count_Type'Max 1268 (P.Get (Positions (Container)'Old, Position) + 1, 1269 P.Get (Positions (Container)'Old, Before) + 1), 1270 Lst => Length (Container)) 1271 1272 -- The elements located after Before and before Position are 1273 -- shifted by 1 to the right. 1274 1275 and M.Range_Shifted 1276 (Left => Model (Container)'Old, 1277 Right => Model (Container), 1278 Fst => P.Get (Positions (Container)'Old, Before) + 1, 1279 Lst => P.Get (Positions (Container)'Old, Position) - 1, 1280 Offset => 1) 1281 1282 -- The elements located after Position and before Before are 1283 -- shifted by 1 to the left. 1284 1285 and M.Range_Shifted 1286 (Left => Model (Container)'Old, 1287 Right => Model (Container), 1288 Fst => P.Get (Positions (Container)'Old, Position) + 1, 1289 Lst => P.Get (Positions (Container)'Old, Before) - 1, 1290 Offset => -1) 1291 1292 -- The element previously at Position is now before Before 1293 1294 and Element 1295 (Model (Container), 1296 P.Get (Positions (Container)'Old, Before)) = 1297 Element 1298 (Model (Container)'Old, 1299 P.Get (Positions (Container)'Old, Position)) 1300 1301 -- Cursors from Container continue designating the same elements 1302 1303 and Mapping_Preserved 1304 (M_Left => Model (Container)'Old, 1305 M_Right => Model (Container), 1306 P_Left => Positions (Container)'Old, 1307 P_Right => Positions (Container))); 1308 1309 function First (Container : List) return Cursor with 1310 Global => null, 1311 Contract_Cases => 1312 (Length (Container) = 0 => 1313 First'Result = No_Element, 1314 1315 others => 1316 Has_Element (Container, First'Result) 1317 and P.Get (Positions (Container), First'Result) = 1); 1318 1319 function First_Element (Container : List) return Element_Type with 1320 Global => null, 1321 Pre => not Is_Empty (Container), 1322 Post => First_Element'Result = M.Get (Model (Container), 1); 1323 1324 function Last (Container : List) return Cursor with 1325 Global => null, 1326 Contract_Cases => 1327 (Length (Container) = 0 => 1328 Last'Result = No_Element, 1329 1330 others => 1331 Has_Element (Container, Last'Result) 1332 and P.Get (Positions (Container), Last'Result) = 1333 Length (Container)); 1334 1335 function Last_Element (Container : List) return Element_Type with 1336 Global => null, 1337 Pre => not Is_Empty (Container), 1338 Post => 1339 Last_Element'Result = M.Get (Model (Container), Length (Container)); 1340 1341 function Next (Container : List; Position : Cursor) return Cursor with 1342 Global => null, 1343 Pre => 1344 Has_Element (Container, Position) or else Position = No_Element, 1345 Contract_Cases => 1346 (Position = No_Element 1347 or else P.Get (Positions (Container), Position) = Length (Container) 1348 => 1349 Next'Result = No_Element, 1350 1351 others => 1352 Has_Element (Container, Next'Result) 1353 and then P.Get (Positions (Container), Next'Result) = 1354 P.Get (Positions (Container), Position) + 1); 1355 1356 procedure Next (Container : List; Position : in out Cursor) with 1357 Global => null, 1358 Pre => 1359 Has_Element (Container, Position) or else Position = No_Element, 1360 Contract_Cases => 1361 (Position = No_Element 1362 or else P.Get (Positions (Container), Position) = Length (Container) 1363 => 1364 Position = No_Element, 1365 1366 others => 1367 Has_Element (Container, Position) 1368 and then P.Get (Positions (Container), Position) = 1369 P.Get (Positions (Container), Position'Old) + 1); 1370 1371 function Previous (Container : List; Position : Cursor) return Cursor with 1372 Global => null, 1373 Pre => 1374 Has_Element (Container, Position) or else Position = No_Element, 1375 Contract_Cases => 1376 (Position = No_Element 1377 or else P.Get (Positions (Container), Position) = 1 1378 => 1379 Previous'Result = No_Element, 1380 1381 others => 1382 Has_Element (Container, Previous'Result) 1383 and then P.Get (Positions (Container), Previous'Result) = 1384 P.Get (Positions (Container), Position) - 1); 1385 1386 procedure Previous (Container : List; Position : in out Cursor) with 1387 Global => null, 1388 Pre => 1389 Has_Element (Container, Position) or else Position = No_Element, 1390 Contract_Cases => 1391 (Position = No_Element 1392 or else P.Get (Positions (Container), Position) = 1 1393 => 1394 Position = No_Element, 1395 1396 others => 1397 Has_Element (Container, Position) 1398 and then P.Get (Positions (Container), Position) = 1399 P.Get (Positions (Container), Position'Old) - 1); 1400 1401 function Find 1402 (Container : List; 1403 Item : Element_Type; 1404 Position : Cursor := No_Element) return Cursor 1405 with 1406 Global => null, 1407 Pre => 1408 Has_Element (Container, Position) or else Position = No_Element, 1409 Contract_Cases => 1410 1411 -- If Item is not contained in Container after Position, Find returns 1412 -- No_Element. 1413 1414 (not M.Contains 1415 (Container => Model (Container), 1416 Fst => 1417 (if Position = No_Element then 1418 1 1419 else 1420 P.Get (Positions (Container), Position)), 1421 Lst => Length (Container), 1422 Item => Item) 1423 => 1424 Find'Result = No_Element, 1425 1426 -- Otherwise, Find returns a valid cursor in Container 1427 1428 others => 1429 P.Has_Key (Positions (Container), Find'Result) 1430 1431 -- The element designated by the result of Find is Item 1432 1433 and Element 1434 (Model (Container), 1435 P.Get (Positions (Container), Find'Result)) = Item 1436 1437 -- The result of Find is located after Position 1438 1439 and (if Position /= No_Element then 1440 P.Get (Positions (Container), Find'Result) >= 1441 P.Get (Positions (Container), Position)) 1442 1443 -- It is the first occurrence of Item in this slice 1444 1445 and not M.Contains 1446 (Container => Model (Container), 1447 Fst => 1448 (if Position = No_Element then 1449 1 1450 else 1451 P.Get (Positions (Container), Position)), 1452 Lst => 1453 P.Get (Positions (Container), Find'Result) - 1, 1454 Item => Item)); 1455 1456 function Reverse_Find 1457 (Container : List; 1458 Item : Element_Type; 1459 Position : Cursor := No_Element) return Cursor 1460 with 1461 Global => null, 1462 Pre => 1463 Has_Element (Container, Position) or else Position = No_Element, 1464 Contract_Cases => 1465 1466 -- If Item is not contained in Container before Position, Find returns 1467 -- No_Element. 1468 1469 (not M.Contains 1470 (Container => Model (Container), 1471 Fst => 1, 1472 Lst => 1473 (if Position = No_Element then 1474 Length (Container) 1475 else 1476 P.Get (Positions (Container), Position)), 1477 Item => Item) 1478 => 1479 Reverse_Find'Result = No_Element, 1480 1481 -- Otherwise, Find returns a valid cursor in Container 1482 1483 others => 1484 P.Has_Key (Positions (Container), Reverse_Find'Result) 1485 1486 -- The element designated by the result of Find is Item 1487 1488 and Element 1489 (Model (Container), 1490 P.Get (Positions (Container), Reverse_Find'Result)) = Item 1491 1492 -- The result of Find is located before Position 1493 1494 and (if Position /= No_Element then 1495 P.Get (Positions (Container), Reverse_Find'Result) <= 1496 P.Get (Positions (Container), Position)) 1497 1498 -- It is the last occurrence of Item in this slice 1499 1500 and not M.Contains 1501 (Container => Model (Container), 1502 Fst => 1503 P.Get (Positions (Container), 1504 Reverse_Find'Result) + 1, 1505 Lst => 1506 (if Position = No_Element then 1507 Length (Container) 1508 else 1509 P.Get (Positions (Container), Position)), 1510 Item => Item)); 1511 1512 function Contains 1513 (Container : List; 1514 Item : Element_Type) return Boolean 1515 with 1516 Global => null, 1517 Post => 1518 Contains'Result = M.Contains (Container => Model (Container), 1519 Fst => 1, 1520 Lst => Length (Container), 1521 Item => Item); 1522 1523 function Has_Element 1524 (Container : List; 1525 Position : Cursor) return Boolean 1526 with 1527 Global => null, 1528 Post => 1529 Has_Element'Result = P.Has_Key (Positions (Container), Position); 1530 pragma Annotate (GNATprove, Inline_For_Proof, Has_Element); 1531 1532 generic 1533 with function "<" (Left, Right : Element_Type) return Boolean is <>; 1534 1535 package Generic_Sorting with SPARK_Mode is 1536 1537 package Formal_Model with Ghost is 1538 function M_Elements_Sorted (Container : M.Sequence) return Boolean 1539 with 1540 Global => null, 1541 Post => 1542 M_Elements_Sorted'Result = 1543 (for all I in 1 .. M.Length (Container) => 1544 (for all J in I .. M.Length (Container) => 1545 Element (Container, I) = Element (Container, J) 1546 or Element (Container, I) < Element (Container, J))); 1547 pragma Annotate (GNATprove, Inline_For_Proof, M_Elements_Sorted); 1548 1549 end Formal_Model; 1550 use Formal_Model; 1551 1552 function Is_Sorted (Container : List) return Boolean with 1553 Global => null, 1554 Post => Is_Sorted'Result = M_Elements_Sorted (Model (Container)); 1555 1556 procedure Sort (Container : in out List) with 1557 Global => null, 1558 Post => 1559 Length (Container) = Length (Container)'Old 1560 and M_Elements_Sorted (Model (Container)) 1561 and M_Elements_Included 1562 (Left => Model (Container)'Old, 1563 L_Lst => Length (Container), 1564 Right => Model (Container), 1565 R_Lst => Length (Container)) 1566 and M_Elements_Included 1567 (Left => Model (Container), 1568 L_Lst => Length (Container), 1569 Right => Model (Container)'Old, 1570 R_Lst => Length (Container)); 1571 1572 procedure Merge (Target : in out List; Source : in out List) with 1573 -- Target and Source should not be aliased 1574 Global => null, 1575 Pre => Length (Source) <= Target.Capacity - Length (Target), 1576 Post => 1577 Length (Target) = Length (Target)'Old + Length (Source)'Old 1578 and Length (Source) = 0 1579 and (if M_Elements_Sorted (Model (Target)'Old) 1580 and M_Elements_Sorted (Model (Source)'Old) 1581 then 1582 M_Elements_Sorted (Model (Target))) 1583 and M_Elements_Included 1584 (Left => Model (Target)'Old, 1585 L_Lst => Length (Target)'Old, 1586 Right => Model (Target), 1587 R_Lst => Length (Target)) 1588 and M_Elements_Included 1589 (Left => Model (Source)'Old, 1590 L_Lst => Length (Source)'Old, 1591 Right => Model (Target), 1592 R_Lst => Length (Target)) 1593 and M_Elements_In_Union 1594 (Model (Target), 1595 Model (Source)'Old, 1596 Model (Target)'Old); 1597 end Generic_Sorting; 1598 1599private 1600 pragma SPARK_Mode (Off); 1601 1602 type Node_Type is record 1603 Prev : Count_Type'Base := -1; 1604 Next : Count_Type; 1605 Element : Element_Type; 1606 end record; 1607 1608 function "=" (L, R : Node_Type) return Boolean is abstract; 1609 1610 type Node_Array is array (Count_Type range <>) of Node_Type; 1611 function "=" (L, R : Node_Array) return Boolean is abstract; 1612 1613 type List (Capacity : Count_Type) is record 1614 Free : Count_Type'Base := -1; 1615 Length : Count_Type := 0; 1616 First : Count_Type := 0; 1617 Last : Count_Type := 0; 1618 Nodes : Node_Array (1 .. Capacity) := (others => <>); 1619 end record; 1620 1621 Empty_List : constant List := (0, others => <>); 1622 1623end Ada.Containers.Formal_Doubly_Linked_Lists; 1624