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