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 Left  (Container : Vector; Position : Cursor) return Vector;
  52 --      function Right (Container : Vector; Position : Cursor) return Vector;
  53
  54 --    See detailed specifications for these subprograms
  55
  56 with Ada.Containers;
  57 use Ada.Containers;
  58
  59 generic
  60    type Index_Type is range <>;
  61    type Element_Type is private;
  62
  63    with function "=" (Left, Right : Element_Type) return Boolean is <>;
  64
  65 package Ada.Containers.Formal_Vectors is
  66    pragma Annotate (GNATprove, External_Axiomatization);
  67    pragma Pure;
  68
  69    subtype Extended_Index is Index_Type'Base
  70    range Index_Type'First - 1 ..
  71      Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
  72
  73    No_Index : constant Extended_Index := Extended_Index'First;
  74
  75    subtype Capacity_Range is
  76      Count_Type range 0 .. Count_Type (Index_Type'Last - Index_Type'First + 1);
  77
  78    type Vector (Capacity : Capacity_Range) is private with
  79      Iterable => (First       => First,
  80                   Next        => Next,
  81                   Has_Element => Has_Element,
  82                   Element     => Element);
  83
  84    type Cursor is private;
  85    pragma Preelaborable_Initialization (Cursor);
  86
  87    Empty_Vector : constant Vector;
  88
  89    No_Element : constant Cursor;
  90
  91    function "=" (Left, Right : Vector) return Boolean with
  92      Global => null;
  93
  94    function To_Vector
  95      (New_Item : Element_Type;
  96       Length   : Count_Type) return Vector
  97    with
  98      Global => null;
  99
 100    function "&" (Left, Right : Vector) return Vector with
 101      Global => null,
 102      Pre    => Capacity_Range'Last - Length (Left) >= Length (Right);
 103
 104    function "&" (Left : Vector; Right : Element_Type) return Vector with
 105      Global => null,
 106      Pre    => Length (Left) < Capacity_Range'Last;
 107
 108    function "&" (Left : Element_Type; Right : Vector) return Vector with
 109      Global => null,
 110      Pre    => Length (Right) < Capacity_Range'Last;
 111
 112    function "&" (Left, Right : Element_Type) return Vector with
 113      Global => null,
 114      Pre    => Capacity_Range'Last >= 2;
 115
 116    function Capacity (Container : Vector) return Count_Type with
 117      Global => null;
 118
 119    procedure Reserve_Capacity
 120      (Container : in out Vector;
 121       Capacity  : Count_Type)
 122    with
 123      Global => null,
 124      Pre    => Capacity <= Container.Capacity;
 125
 126    function Length (Container : Vector) return Count_Type with
 127      Global => null;
 128
 129    procedure Set_Length
 130      (Container : in out Vector;
 131       New_Length    : Count_Type)
 132    with
 133      Global => null,
 134      Pre    => New_Length <= Length (Container);
 135
 136    function Is_Empty (Container : Vector) return Boolean with
 137      Global => null;
 138
 139    procedure Clear (Container : in out Vector) with
 140      Global => null;
 141
 142    procedure Assign (Target : in out Vector; Source : Vector) with
 143      Global => null,
 144      Pre    => Length (Source) <= Target.Capacity;
 145
 146    function Copy
 147      (Source   : Vector;
 148       Capacity : Count_Type := 0) return Vector
 149    with
 150      Global => null,
 151      Pre    => Length (Source) <= Capacity and then Capacity in Capacity_Range;
 152
 153    function To_Cursor
 154      (Container : Vector;
 155       Index     : Extended_Index) return Cursor
 156    with
 157      Global => null;
 158
 159    function To_Index (Position : Cursor) return Extended_Index with
 160      Global => null;
 161
 162    function Element
 163      (Container : Vector;
 164       Index     : Index_Type) return Element_Type
 165    with
 166      Global => null,
 167      Pre    => First_Index (Container) <= Index
 168                  and then Index <= Last_Index (Container);
 169
 170    function Element
 171      (Container : Vector;
 172       Position  : Cursor) return Element_Type
 173    with
 174      Global => null,
 175      Pre    => Has_Element (Container, Position);
 176
 177    procedure Replace_Element
 178      (Container : in out Vector;
 179       Index     : Index_Type;
 180       New_Item  : Element_Type)
 181    with
 182      Global => null,
 183      Pre    => First_Index (Container) <= Index
 184                  and then Index <= Last_Index (Container);
 185
 186    procedure Replace_Element
 187      (Container : in out Vector;
 188       Position  : Cursor;
 189       New_Item  : Element_Type)
 190    with
 191      Global => null,
 192      Pre    => Has_Element (Container, Position);
 193
 194    procedure Move (Target : in out Vector; Source : in out Vector) with
 195      Global => null,
 196      Pre    => Length (Source) <= Target.Capacity;
 197
 198    procedure Insert
 199      (Container : in out Vector;
 200       Before    : Extended_Index;
 201       New_Item  : Vector)
 202    with
 203      Global => null,
 204      Pre    => First_Index (Container) <= Before
 205                  and then Before <= Last_Index (Container) + 1
 206                  and then Length (Container) < Container.Capacity;
 207
 208    procedure Insert
 209      (Container : in out Vector;
 210       Before    : Cursor;
 211       New_Item  : Vector)
 212    with
 213      Global => null,
 214      Pre    => Length (Container) < Container.Capacity
 215                  and then (Has_Element (Container, Before)
 216                             or else Before = No_Element);
 217
 218    procedure Insert
 219      (Container : in out Vector;
 220       Before    : Cursor;
 221       New_Item  : Vector;
 222       Position  : out Cursor)
 223    with
 224      Global => null,
 225      Pre    => Length (Container) < Container.Capacity
 226                  and then (Has_Element (Container, Before)
 227                             or else Before = No_Element);
 228
 229    procedure Insert
 230      (Container : in out Vector;
 231       Before    : Extended_Index;
 232       New_Item  : Element_Type;
 233       Count     : Count_Type := 1)
 234    with
 235      Global => null,
 236      Pre    => First_Index (Container) <= Before
 237                  and then Before <= Last_Index (Container) + 1
 238                  and then Length (Container) + Count <= Container.Capacity;
 239
 240    procedure Insert
 241      (Container : in out Vector;
 242       Before    : Cursor;
 243       New_Item  : Element_Type;
 244       Count     : Count_Type := 1)
 245    with
 246      Global => null,
 247      Pre    => Length (Container) + Count <= Container.Capacity
 248                  and then (Has_Element (Container, Before)
 249                             or else Before = No_Element);
 250
 251    procedure Insert
 252      (Container : in out Vector;
 253       Before    : Cursor;
 254       New_Item  : Element_Type;
 255       Position  : out Cursor;
 256       Count     : Count_Type := 1)
 257    with
 258      Global => null,
 259      Pre    => Length (Container) + Count <= Container.Capacity
 260                  and then (Has_Element (Container, Before)
 261                             or else Before = No_Element);
 262
 263    procedure Prepend
 264      (Container : in out Vector;
 265       New_Item  : Vector)
 266    with
 267      Global => null,
 268      Pre    => Length (Container) < Container.Capacity;
 269
 270    procedure Prepend
 271      (Container : in out Vector;
 272       New_Item  : Element_Type;
 273       Count     : Count_Type := 1)
 274    with
 275      Global => null,
 276      Pre    => Length (Container) + Count <= Container.Capacity;
 277
 278    procedure Append
 279      (Container : in out Vector;
 280       New_Item  : Vector)
 281    with
 282      Global => null,
 283      Pre    => Length (Container) < Container.Capacity;
 284
 285    procedure Append
 286      (Container : in out Vector;
 287       New_Item  : Element_Type;
 288       Count     : Count_Type := 1)
 289    with
 290      Global => null,
 291      Pre    => Length (Container) + Count <= Container.Capacity;
 292
 293    procedure Delete
 294      (Container : in out Vector;
 295       Index     : Extended_Index;
 296       Count     : Count_Type := 1)
 297    with
 298      Global => null,
 299      Pre    => First_Index (Container) <= Index
 300                  and then Index <= Last_Index (Container) + 1;
 301
 302    procedure Delete
 303      (Container : in out Vector;
 304       Position  : in out Cursor;
 305       Count     : Count_Type := 1)
 306    with
 307      Global => null,
 308      Pre    => Has_Element (Container, Position);
 309
 310    procedure Delete_First
 311      (Container : in out Vector;
 312       Count     : Count_Type := 1)
 313    with
 314      Global => null;
 315
 316    procedure Delete_Last
 317      (Container : in out Vector;
 318       Count     : Count_Type := 1)
 319    with
 320      Global => null;
 321
 322    procedure Reverse_Elements (Container : in out Vector) with
 323      Global => null;
 324
 325    procedure Swap (Container : in out Vector; I, J : Index_Type) with
 326      Global => null,
 327      Pre    => First_Index (Container) <= I
 328                  and then I <= Last_Index (Container)
 329                  and then First_Index (Container) <= J
 330                  and then J <= Last_Index (Container);
 331
 332    procedure Swap (Container : in out Vector; I, J : Cursor) with
 333      Global => null,
 334      Pre    => Has_Element (Container, I) and then Has_Element (Container, J);
 335
 336    function First_Index (Container : Vector) return Index_Type with
 337      Global => null;
 338
 339    function First (Container : Vector) return Cursor with
 340      Global => null;
 341
 342    function First_Element (Container : Vector) return Element_Type with
 343      Global => null,
 344      Pre    => not Is_Empty (Container);
 345
 346    function Last_Index (Container : Vector) return Extended_Index with
 347      Global => null;
 348
 349    function Last (Container : Vector) return Cursor with
 350      Global => null;
 351
 352    function Last_Element (Container : Vector) return Element_Type with
 353      Global => null,
 354      Pre    => not Is_Empty (Container);
 355
 356    function Next (Container : Vector; Position : Cursor) return Cursor with
 357      Global => null,
 358      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 359
 360    procedure Next (Container : Vector; Position : in out Cursor) with
 361      Global => null,
 362      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 363
 364    function Previous (Container : Vector; Position : Cursor) return Cursor with
 365      Global => null,
 366      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 367
 368    procedure Previous (Container : Vector; Position : in out Cursor) with
 369      Global => null,
 370      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 371
 372    function Find_Index
 373      (Container : Vector;
 374       Item      : Element_Type;
 375       Index     : Index_Type := Index_Type'First) return Extended_Index
 376    with
 377      Global => null;
 378
 379    function Find
 380      (Container : Vector;
 381       Item      : Element_Type;
 382       Position  : Cursor := No_Element) return Cursor
 383    with
 384      Global => null,
 385      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 386
 387    function Reverse_Find_Index
 388      (Container : Vector;
 389       Item      : Element_Type;
 390       Index     : Index_Type := Index_Type'Last) return Extended_Index
 391    with
 392      Global => null;
 393
 394    function Reverse_Find
 395      (Container : Vector;
 396       Item      : Element_Type;
 397       Position  : Cursor := No_Element) return Cursor
 398    with
 399      Global => null,
 400      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 401
 402    function Contains
 403      (Container : Vector;
 404       Item      : Element_Type) return Boolean
 405    with
 406      Global => null;
 407
 408    function Has_Element (Container : Vector; Position : Cursor) return Boolean
 409    with
 410      Global => null;
 411
 412    generic
 413       with function "<" (Left, Right : Element_Type) return Boolean is <>;
 414    package Generic_Sorting is
 415
 416       function Is_Sorted (Container : Vector) return Boolean with
 417         Global => null;
 418
 419       procedure Sort (Container : in out Vector) with
 420         Global => null;
 421
 422       procedure Merge (Target : in out Vector; Source : in out Vector) with
 423         Global => null;
 424
 425    end Generic_Sorting;
 426
 427    function Strict_Equal (Left, Right : Vector) return Boolean with
 428      Global => null;
 429    --  Strict_Equal returns True if the containers are physically equal, i.e.
 430    --  they are structurally equal (function "=" returns True) and that they
 431    --  have the same set of cursors.
 432
 433    function Left (Container : Vector; Position : Cursor) return Vector with
 434      Global => null,
 435      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 436    function Right (Container : Vector; Position : Cursor) return Vector with
 437      Global => null,
 438      Pre    => Has_Element (Container, Position) or else Position = No_Element;
 439    --  Left returns a container containing all elements preceding Position
 440    --  (excluded) in Container. Right returns a container containing all
 441    --  elements following Position (included) in Container. These two new
 442    --  functions can be used to express invariant properties in loops which
 443    --  iterate over containers. Left returns the part of the container already
 444    --  scanned and Right the part not scanned yet.
 445
 446 private
 447
 448    pragma Inline (First_Index);
 449    pragma Inline (Last_Index);
 450    pragma Inline (Element);
 451    pragma Inline (First_Element);
 452    pragma Inline (Last_Element);
 453    pragma Inline (Replace_Element);
 454    pragma Inline (Contains);
 455    pragma Inline (Next);
 456    pragma Inline (Previous);
 457
 458    type Elements_Array is array (Count_Type range <>) of Element_Type;
 459    function "=" (L, R : Elements_Array) return Boolean is abstract;
 460
 461    type Vector (Capacity : Capacity_Range) is record
 462       Elements : Elements_Array (1 .. Capacity);
 463       Last     : Extended_Index := No_Index;
 464    end record;
 465
 466    type Cursor is record
 467       Valid : Boolean    := True;
 468       Index : Index_Type := Index_Type'First;
 469    end record;
 470
 471    Empty_Vector : constant Vector := (Capacity => 0, others => <>);
 472
 473    No_Element : constant Cursor := (Valid => False, Index => Index_Type'First);
 474
 475 end Ada.Containers.Formal_Vectors;