gcc/ada/a-cofove.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT LIBRARY COMPONENTS                          --
   4 --                                                                          --
   5 --         A D A . C O N T A I N E R S . F O R M A L _ V E C T O R S        --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 --          Copyright (C) 2004-2013, Free Software Foundation, Inc.         --
  10 --                                                                          --
  11 -- This specification is derived from the Ada Reference Manual for use with --
  12 -- GNAT. The copyright notice above, and the license provisions that follow --
  13 -- apply solely to the  contents of the part following the private keyword. --
  14 --                                                                          --
  15 -- GNAT is free software;  you can  redistribute it  and/or modify it under --
  16 -- terms of the  GNU General Public License as published  by the Free Soft- --
  17 -- ware  Foundation;  either version 3,  or (at your option) any later ver- --
  18 -- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
  19 -- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
  20 -- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
  21 --                                                                          --
  22 -- As a special exception under Section 7 of GPL version 3, you are granted --
  23 -- additional permissions described in the GCC Runtime Library Exception,   --
  24 -- version 3.1, as published by the Free Software Foundation.               --
  25 --                                                                          --
  26 -- You should have received a copy of the GNU General Public License and    --
  27 -- a copy of the GCC Runtime Library Exception along with this program;     --
  28 -- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
  29 -- <http://www.gnu.org/licenses/>.                                          --
  30 ------------------------------------------------------------------------------
  31
  32 --  This spec is derived from package Ada.Containers.Bounded_Vectors in the Ada
  33 --  2012 RM. The modifications are meant to facilitate formal proofs by making
  34 --  it easier to express properties, and by making the specification of this
  35 --  unit compatible with SPARK 2014. Note that the API of this unit may be
  36 --  subject to incompatible changes as SPARK 2014 evolves.
  37
  38 --  The modifications are:
  39
  40 --    A parameter for the container is added to every function reading the
  41 --    content of a container: Element, Next, Query_Element, Previous, Iterate,
  42 --    Has_Element, Reverse_Iterate. This change is motivated by the need
  43 --    to have cursors which are valid on different containers (typically a
  44 --    container C and its previous version C'Old) for expressing properties,
  45 --    which is not possible if cursors encapsulate an access to the underlying
  46 --    container.
  47
  48 --    There are three new functions:
  49
  50 --      function Strict_Equal (Left, Right : Vector) return Boolean;
  51 --      function First_To_Previous  (Container : Vector; Current : Cursor)
  52 --         return Vector;
  53 --      function Current_To_Last (Container : Vector; Current : Cursor)
  54 --         return Vector;
  55
  56 --    See detailed specifications for these subprograms
  57
  58 with Ada.Containers;
  59 use Ada.Containers;
  60
  61 generic
  62    type Index_Type is range <>;
  63    type Element_Type is private;
  64
  65    with function "=" (Left, Right : Element_Type) return Boolean is <>;
  66
  67 package Ada.Containers.Formal_Vectors is
  68    pragma Annotate (GNATprove, External_Axiomatization);
  69    pragma Pure;
  70
  71    subtype Extended_Index is Index_Type'Base
  72    range Index_Type'First - 1 ..
  73      Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
  74
  75    No_Index : constant Extended_Index := Extended_Index'First;
  76
  77    subtype Capacity_Range is
  78      Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1);
  79
  80    type Vector (Capacity : Capacity_Range) is private with
  81      Iterable => (First       => First,
  82                   Next        => Next,
  83                   Has_Element => Has_Element,
  84                   Element     => Element);
  85
  86    type Cursor is private;
  87    pragma Preelaborable_Initialization (Cursor);
  88
  89    Empty_Vector : constant Vector;
  90
  91    No_Element : constant Cursor;
  92
  93    function "=" (Left, Right : Vector) return Boolean with
  94      Global => null;
  95
  96    function To_Vector
  97      (New_Item : Element_Type;
  98       Length   : Count_Type) return Vector
  99    with
 100      Global => null;
 101
 102    function "&" (Left, Right : Vector) return Vector with
 103      Global => null,
 104      Pre    => Capacity_Range'Last - Length (Left) >= Length (Right);
 105
 106    function "&" (Left : Vector; Right : Element_Type) return Vector with
 107      Global => null,
 108      Pre    => Length (Left) < Capacity_Range'Last;
 109
 110    function "&" (Left : Element_Type; Right : Vector) return Vector with
 111      Global => null,
 112      Pre    => Length (Right) < Capacity_Range'Last;
 113
 114    function "&" (Left, Right : Element_Type) return Vector with
 115      Global => null,
 116      Pre    => Capacity_Range'Last >= 2;
 117
 118    function Capacity (Container : Vector) return Count_Type with
 119      Global => null;
 120
 121    procedure Reserve_Capacity
 122      (Container : in out Vector;
 123       Capacity  : Count_Type)
 124    with
 125      Global => null,
 126      Pre    => Capacity <= Container.Capacity;
 127
 128    function Length (Container : Vector) return Count_Type with
 129      Global => null;
 130
 131    procedure Set_Length
 132      (Container : in out Vector;
 133       New_Length    : Count_Type)
 134    with
 135      Global => null,
 136      Pre    => New_Length <= Length (Container);
 137
 138    function Is_Empty (Container : Vector) return Boolean with
 139      Global => null;
 140
 141    procedure Clear (Container : in out Vector) with
 142      Global => null;
 143
 144    procedure Assign (Target : in out Vector; Source : Vector) with
 145      Global => null,
 146      Pre    => Length (Source) <= Target.Capacity;
 147
 148    function Copy
 149      (Source   : Vector;
 150       Capacity : Count_Type := 0) return Vector
 151    with
 152      Global => null,
 153      Pre    => Length (Source) <= Capacity and then Capacity in Capacity_Range;
 154
 155    function To_Cursor
 156      (Container : Vector;
 157       Index     : Extended_Index) return Cursor
 158    with
 159      Global => null;
 160
 161    function To_Index (Position : Cursor) return Extended_Index with
 162      Global => null;
 163
 164    function Element
 165      (Container : Vector;
 166       Index     : Index_Type) return Element_Type
 167    with
 168      Global => null,
 169      Pre    => First_Index (Container) <= Index
 170                  and then Index <= Last_Index (Container);
 171
 172    function Element
 173      (Container : Vector;
 174       Position  : Cursor) return Element_Type
 175    with
 176      Global => null,
 177      Pre    => Has_Element (Container, Position);
 178
 179    procedure Replace_Element
 180      (Container : in out Vector;
 181       Index     : Index_Type;
 182       New_Item  : Element_Type)
 183    with
 184      Global => null,
 185      Pre    => First_Index (Container) <= Index
 186                  and then Index <= Last_Index (Container);
 187
 188    procedure Replace_Element
 189      (Container : in out Vector;
 190       Position  : Cursor;
 191       New_Item  : Element_Type)
 192    with
 193      Global => null,
 194      Pre    => Has_Element (Container, Position);
 195
 196    procedure Move (Target : in out Vector; Source : in out Vector) with
 197      Global => null,
 198      Pre    => Length (Source) <= Target.Capacity;
 199
 200    procedure Insert
 201      (Container : in out Vector;
 202       Before    : Extended_Index;
 203       New_Item  : Vector)
 204    with
 205      Global => null,
 206      Pre    => First_Index (Container) <= Before
 207                  and then Before <= Last_Index (Container) + 1
 208                  and then Length (Container) < Container.Capacity;
 209
 210    procedure Insert
 211      (Container : in out Vector;
 212       Before    : Cursor;
 213       New_Item  : Vector)
 214    with
 215      Global => null,
 216      Pre    => Length (Container) < Container.Capacity
 217                  and then (Has_Element (Container, Before)
 218                             or else Before = No_Element);
 219
 220    procedure Insert
 221      (Container : in out Vector;
 222       Before    : Cursor;
 223       New_Item  : Vector;
 224       Position  : out Cursor)
 225    with
 226      Global => null,
 227      Pre    => Length (Container) < Container.Capacity
 228                  and then (Has_Element (Container, Before)
 229                             or else Before = No_Element);
 230
 231    procedure Insert
 232      (Container : in out Vector;
 233       Before    : Extended_Index;
 234       New_Item  : Element_Type;
 235       Count     : Count_Type := 1)
 236    with
 237      Global => null,
 238      Pre    => First_Index (Container) <= Before
 239                  and then Before <= Last_Index (Container) + 1
 240                  and then Length (Container) + Count <= Container.Capacity;
 241
 242    procedure Insert
 243      (Container : in out Vector;
 244       Before    : Cursor;
 245       New_Item  : Element_Type;
 246       Count     : Count_Type := 1)
 247    with
 248      Global => null,
 249      Pre    => Length (Container) + Count <= Container.Capacity
 250                  and then (Has_Element (Container, Before)
 251                             or else Before = No_Element);
 252
 253    procedure Insert
 254      (Container : in out Vector;
 255       Before    : Cursor;
 256       New_Item  : Element_Type;
 257       Position  : out Cursor;
 258       Count     : Count_Type := 1)
 259    with
 260      Global => null,
 261      Pre    => Length (Container) + Count <= Container.Capacity
 262                  and then (Has_Element (Container, Before)
 263                             or else Before = No_Element);
 264
 265    procedure Prepend
 266      (Container : in out Vector;
 267       New_Item  : Vector)
 268    with
 269      Global => null,
 270      Pre    => Length (Container) < Container.Capacity;
 271
 272    procedure Prepend
 273      (Container : in out Vector;
 274       New_Item  : Element_Type;
 275       Count     : Count_Type := 1)
 276    with
 277      Global => null,
 278      Pre    => Length (Container) + Count <= Container.Capacity;
 279
 280    procedure Append
 281      (Container : in out Vector;
 282       New_Item  : Vector)
 283    with
 284      Global => null,
 285      Pre    => Length (Container) < Container.Capacity;
 286
 287    procedure Append
 288      (Container : in out Vector;
 289       New_Item  : Element_Type;
 290       Count     : Count_Type := 1)
 291    with
 292      Global => null,
 293      Pre    => Length (Container) + Count <= Container.Capacity;
 294
 295    procedure Delete
 296      (Container : in out Vector;
 297       Index     : Extended_Index;
 298       Count     : Count_Type := 1)
 299    with
 300      Global => null,
 301      Pre    => First_Index (Container) <= Index
 302                  and then Index <= Last_Index (Container) + 1;
 303
 304    procedure Delete
 305      (Container : in out Vector;
 306       Position  : in out Cursor;
 307       Count     : Count_Type := 1)
 308    with
 309      Global => null,
 310      Pre    => Has_Element (Container, Position);
 311
 312    procedure Delete_First
 313      (Container : in out Vector;
 314       Count     : Count_Type := 1)
 315    with
 316      Global => null;
 317
 318    procedure Delete_Last
 319      (Container : in out Vector;
 320       Count     : Count_Type := 1)
 321    with
 322      Global => null;
 323
 324    procedure Reverse_Elements (Container : in out Vector) with
 325      Global => null;
 326
 327    procedure Swap (Container : in out Vector; I, J : Index_Type) with
 328      Global => null,
 329      Pre    => First_Index (Container) <= I
 330                  and then I <= Last_Index (Container)
 331                  and then First_Index (Container) <= J
 332                  and then J <= Last_Index (Container);
 333
 334    procedure Swap (Container : in out Vector; I, J : Cursor) with
 335      Global => null,
 336      Pre    => Has_Element (Container, I) and then Has_Element (Container, J);
 337
 338    function First_Index (Container : Vector) return Index_Type with
 339      Global => null;
 340
 341    function First (Container : Vector) return Cursor with
 342      Global => null;
 343
 344    function First_Element (Container : Vector) return Element_Type with
 345      Global => null,
 346      Pre    => not Is_Empty (Container);
 347
 348    function Last_Index (Container : Vector) return Extended_Index with
 349      Global => null;
 350
 351    function Last (Container : Vector) return Cursor with
 352      Global => null;
 353
 354    function Last_Element (Container : Vector) return Element_Type with
 355      Global => null,
 356      Pre    => not Is_Empty (Container);
 357
 358    function Next (Container : Vector; Position : Cursor) return Cursor with
 359      Global => null,
 360      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 361
 362    procedure Next (Container : Vector; Position : in out Cursor) with
 363      Global => null,
 364      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 365
 366    function Previous (Container : Vector; Position : Cursor) return Cursor with
 367      Global => null,
 368      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 369
 370    procedure Previous (Container : Vector; Position : in out Cursor) with
 371      Global => null,
 372      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 373
 374    function Find_Index
 375      (Container : Vector;
 376       Item      : Element_Type;
 377       Index     : Index_Type := Index_Type'First) return Extended_Index
 378    with
 379      Global => null;
 380
 381    function Find
 382      (Container : Vector;
 383       Item      : Element_Type;
 384       Position  : Cursor := No_Element) return Cursor
 385    with
 386      Global => null,
 387      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 388
 389    function Reverse_Find_Index
 390      (Container : Vector;
 391       Item      : Element_Type;
 392       Index     : Index_Type := Index_Type'Last) return Extended_Index
 393    with
 394      Global => null;
 395
 396    function Reverse_Find
 397      (Container : Vector;
 398       Item      : Element_Type;
 399       Position  : Cursor := No_Element) return Cursor
 400    with
 401      Global => null,
 402      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 403
 404    function Contains
 405      (Container : Vector;
 406       Item      : Element_Type) return Boolean
 407    with
 408      Global => null;
 409
 410    function Has_Element (Container : Vector; Position : Cursor) return Boolean
 411    with
 412      Global => null;
 413
 414    generic
 415       with function "<" (Left, Right : Element_Type) return Boolean is <>;
 416    package Generic_Sorting is
 417
 418       function Is_Sorted (Container : Vector) return Boolean with
 419         Global => null;
 420
 421       procedure Sort (Container : in out Vector) with
 422         Global => null;
 423
 424       procedure Merge (Target : in out Vector; Source : in out Vector) with
 425         Global => null;
 426
 427    end Generic_Sorting;
 428
 429    function Strict_Equal (Left, Right : Vector) return Boolean with
 430      Global => null;
 431    --  Strict_Equal returns True if the containers are physically equal, i.e.
 432    --  they are structurally equal (function "=" returns True) and that they
 433    --  have the same set of cursors.
 434
 435    function First_To_Previous
 436      (Container : Vector;
 437       Current : Cursor) return Vector
 438    with
 439      Global => null,
 440      Pre    => Has_Element (Container, Current) or else Current = No_Element;
 441    function Current_To_Last
 442      (Container : Vector;
 443       Current : Cursor) return Vector
 444    with
 445      Global => null,
 446      Pre    => Has_Element (Container, Current) or else Current = No_Element;
 447    --  First_To_Previous returns a container containing all elements preceding
 448    --  Current (excluded) in Container. Current_To_Last returns a container
 449    --  containing all elements following Current (included) in Container.
 450    --  These two new functions can be used to express invariant properties in
 451    --  loops which iterate over containers. First_To_Previous returns the part
 452    --  of the container already scanned and Current_To_Last the part not
 453    --  scanned yet.
 454
 455 private
 456
 457    pragma Inline (First_Index);
 458    pragma Inline (Last_Index);
 459    pragma Inline (Element);
 460    pragma Inline (First_Element);
 461    pragma Inline (Last_Element);
 462    pragma Inline (Replace_Element);
 463    pragma Inline (Contains);
 464    pragma Inline (Next);
 465    pragma Inline (Previous);
 466
 467    type Elements_Array is array (Count_Type range <>) of Element_Type;
 468    function "=" (L, R : Elements_Array) return Boolean is abstract;
 469
 470    type Vector (Capacity : Capacity_Range) is record
 471       Elements : Elements_Array (1 .. Capacity);
 472       Last     : Extended_Index := No_Index;
 473    end record;
 474
 475    type Cursor is record
 476       Valid : Boolean    := True;
 477       Index : Index_Type := Index_Type'First;
 478    end record;
 479
 480    Empty_Vector : constant Vector := (Capacity => 0, others => <>);
 481
 482    No_Element : constant Cursor := (Valid => False, Index => Index_Type'First);
 483
 484 end Ada.Containers.Formal_Vectors;