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 to facilitate formal proofs by making it
  34 --  easier to express properties.
  35
  36 --  The modifications are:
  37
  38 --    A parameter for the container is added to every function reading the
  39 --    content of a container: Element, Next, Query_Element, Previous, Iterate,
  40 --    Has_Element, Reverse_Iterate. This change is motivated by the need
  41 --    to have cursors which are valid on different containers (typically a
  42 --    container C and its previous version C'Old) for expressing properties,
  43 --    which is not possible if cursors encapsulate an access to the underlying
  44 --    container.
  45
  46 --    There are two new functions:
  47
  48 --      function Left  (Container : Vector; Position : Cursor) return Vector;
  49 --      function Right (Container : Vector; Position : Cursor) return Vector;
  50
  51 --      Left returns a container containing all elements preceding Position
  52 --      (excluded) in Container. Right returns a container containing all
  53 --      elements following Position (included) in Container. These two new
  54 --      functions are useful to express invariant properties in loops which
  55 --      iterate over containers. Left returns the part of the container already
  56 --      scanned and Right the part not scanned yet.
  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 Pure;
  69
  70    subtype Extended_Index is Index_Type'Base
  71    range Index_Type'First - 1 ..
  72      Index_Type'Min (Index_Type'Base'Last - 1, Index_Type'Last) + 1;
  73
  74    No_Index : constant Extended_Index := Extended_Index'First;
  75
  76    type Vector (Capacity : Count_Type) is private;
  77
  78    type Cursor is private;
  79    pragma Preelaborable_Initialization (Cursor);
  80
  81    Empty_Vector : constant Vector;
  82
  83    No_Element : constant Cursor;
  84
  85    function "=" (Left, Right : Vector) return Boolean;
  86
  87    function To_Vector
  88      (New_Item : Element_Type;
  89       Length   : Count_Type) return Vector;
  90
  91    function "&" (Left, Right : Vector) return Vector;
  92
  93    function "&" (Left : Vector; Right : Element_Type) return Vector;
  94
  95    function "&" (Left : Element_Type; Right : Vector) return Vector;
  96
  97    function "&" (Left, Right : Element_Type) return Vector;
  98
  99    function Capacity (Container : Vector) return Count_Type;
 100
 101    procedure Reserve_Capacity
 102      (Container : in out Vector;
 103       Capacity  : Count_Type)
 104    with
 105      Pre => Capacity <= Container.Capacity;
 106
 107    function Length (Container : Vector) return Count_Type;
 108
 109    procedure Set_Length
 110      (Container : in out Vector;
 111       New_Length    : Count_Type)
 112    with
 113      Pre => New_Length <= Length (Container);
 114
 115    function Is_Empty (Container : Vector) return Boolean;
 116
 117    procedure Clear (Container : in out Vector);
 118
 119    procedure Assign (Target : in out Vector; Source : Vector) with
 120      Pre => Length (Source) <= Target.Capacity;
 121
 122    function Copy
 123      (Source   : Vector;
 124       Capacity : Count_Type := 0) return Vector
 125    with
 126      Pre => Length (Source) <= Capacity;
 127
 128    function To_Cursor
 129      (Container : Vector;
 130       Index     : Extended_Index) return Cursor;
 131
 132    function To_Index (Position : Cursor) return Extended_Index;
 133
 134    function Element
 135      (Container : Vector;
 136       Index     : Index_Type) return Element_Type
 137    with
 138      Pre => First_Index (Container) <= Index
 139               and then Index <= Last_Index (Container);
 140
 141    function Element
 142      (Container : Vector;
 143       Position  : Cursor) return Element_Type
 144    with
 145      Pre => Has_Element (Container, Position);
 146
 147    procedure Replace_Element
 148      (Container : in out Vector;
 149       Index     : Index_Type;
 150       New_Item  : Element_Type)
 151    with
 152      Pre => First_Index (Container) <= Index
 153               and then Index <= Last_Index (Container);
 154
 155    procedure Replace_Element
 156      (Container : in out Vector;
 157       Position  : Cursor;
 158       New_Item  : Element_Type)
 159    with
 160      Pre => Has_Element (Container, Position);
 161
 162    procedure Move (Target : in out Vector; Source : in out Vector) with
 163      Pre => Length (Source) <= Target.Capacity;
 164
 165    procedure Insert
 166      (Container : in out Vector;
 167       Before    : Extended_Index;
 168       New_Item  : Vector)
 169    with
 170      Pre => First_Index (Container) <= Before
 171               and then Before <= Last_Index (Container) + 1
 172               and then Length (Container) < Container.Capacity;
 173
 174    procedure Insert
 175      (Container : in out Vector;
 176       Before    : Cursor;
 177       New_Item  : Vector)
 178    with
 179      Pre => Length (Container) < Container.Capacity
 180               and then (Has_Element (Container, Before)
 181                          or else Before = No_Element);
 182
 183    procedure Insert
 184      (Container : in out Vector;
 185       Before    : Cursor;
 186       New_Item  : Vector;
 187       Position  : out Cursor)
 188    with
 189      Pre => Length (Container) < Container.Capacity
 190               and then (Has_Element (Container, Before)
 191                          or else Before = No_Element);
 192
 193    procedure Insert
 194      (Container : in out Vector;
 195       Before    : Extended_Index;
 196       New_Item  : Element_Type;
 197       Count     : Count_Type := 1)
 198    with
 199      Pre => First_Index (Container) <= Before
 200               and then Before <= Last_Index (Container) + 1
 201               and then Length (Container) + Count <= Container.Capacity;
 202
 203    procedure Insert
 204      (Container : in out Vector;
 205       Before    : Cursor;
 206       New_Item  : Element_Type;
 207       Count     : Count_Type := 1)
 208    with
 209      Pre => Length (Container) + Count <= Container.Capacity
 210               and then (Has_Element (Container, Before)
 211                          or else Before = No_Element);
 212
 213    procedure Insert
 214      (Container : in out Vector;
 215       Before    : Cursor;
 216       New_Item  : Element_Type;
 217       Position  : out Cursor;
 218       Count     : Count_Type := 1)
 219    with
 220      Pre => Length (Container) + Count <= Container.Capacity
 221               and then (Has_Element (Container, Before)
 222                          or else Before = No_Element);
 223
 224    procedure Prepend
 225      (Container : in out Vector;
 226       New_Item  : Vector)
 227    with
 228      Pre => Length (Container) < Container.Capacity;
 229
 230    procedure Prepend
 231      (Container : in out Vector;
 232       New_Item  : Element_Type;
 233       Count     : Count_Type := 1)
 234    with
 235      Pre => Length (Container) + Count <= Container.Capacity;
 236
 237    procedure Append
 238      (Container : in out Vector;
 239       New_Item  : Vector)
 240    with
 241      Pre => Length (Container) < Container.Capacity;
 242
 243    procedure Append
 244      (Container : in out Vector;
 245       New_Item  : Element_Type;
 246       Count     : Count_Type := 1)
 247    with
 248      Pre => Length (Container) + Count <= Container.Capacity;
 249
 250    procedure Delete
 251      (Container : in out Vector;
 252       Index     : Extended_Index;
 253       Count     : Count_Type := 1)
 254    with
 255      Pre => First_Index (Container) <= Index
 256               and then Index <= Last_Index (Container) + 1;
 257
 258    procedure Delete
 259      (Container : in out Vector;
 260       Position  : in out Cursor;
 261       Count     : Count_Type := 1)
 262    with
 263      Pre => Has_Element (Container, Position);
 264
 265    procedure Delete_First
 266      (Container : in out Vector;
 267       Count     : Count_Type := 1);
 268
 269    procedure Delete_Last
 270      (Container : in out Vector;
 271       Count     : Count_Type := 1);
 272
 273    procedure Reverse_Elements (Container : in out Vector);
 274
 275    procedure Swap (Container : in out Vector; I, J : Index_Type) with
 276      Pre => First_Index (Container) <= I and then I <= Last_Index (Container)
 277               and then First_Index (Container) <= J
 278               and then J <= Last_Index (Container);
 279
 280    procedure Swap (Container : in out Vector; I, J : Cursor) with
 281      Pre => Has_Element (Container, I) and then Has_Element (Container, J);
 282
 283    function First_Index (Container : Vector) return Index_Type;
 284
 285    function First (Container : Vector) return Cursor;
 286
 287    function First_Element (Container : Vector) return Element_Type with
 288      Pre => not Is_Empty (Container);
 289
 290    function Last_Index (Container : Vector) return Extended_Index;
 291
 292    function Last (Container : Vector) return Cursor;
 293
 294    function Last_Element (Container : Vector) return Element_Type with
 295      Pre => not Is_Empty (Container);
 296
 297    function Next (Container : Vector; Position : Cursor) return Cursor with
 298      Pre => Has_Element (Container, Position) or else Position = No_Element;
 299
 300    procedure Next (Container : Vector; Position : in out Cursor) with
 301      Pre => Has_Element (Container, Position) or else Position = No_Element;
 302
 303    function Previous (Container : Vector; Position : Cursor) return Cursor with
 304      Pre => Has_Element (Container, Position) or else Position = No_Element;
 305
 306    procedure Previous (Container : Vector; Position : in out Cursor) with
 307      Pre => Has_Element (Container, Position) or else Position = No_Element;
 308
 309    function Find_Index
 310      (Container : Vector;
 311       Item      : Element_Type;
 312       Index     : Index_Type := Index_Type'First) return Extended_Index;
 313
 314    function Find
 315      (Container : Vector;
 316       Item      : Element_Type;
 317       Position  : Cursor := No_Element) return Cursor
 318    with
 319      Pre => Has_Element (Container, Position) or else Position = No_Element;
 320
 321    function Reverse_Find_Index
 322      (Container : Vector;
 323       Item      : Element_Type;
 324       Index     : Index_Type := Index_Type'Last) return Extended_Index;
 325
 326    function Reverse_Find
 327      (Container : Vector;
 328       Item      : Element_Type;
 329       Position  : Cursor := No_Element) return Cursor
 330    with
 331      Pre => Has_Element (Container, Position) or else Position = No_Element;
 332
 333    function Contains
 334      (Container : Vector;
 335       Item      : Element_Type) return Boolean;
 336
 337    function Has_Element (Container : Vector; Position : Cursor) return Boolean;
 338
 339    generic
 340       with function "<" (Left, Right : Element_Type) return Boolean is <>;
 341    package Generic_Sorting is
 342
 343       function Is_Sorted (Container : Vector) return Boolean;
 344
 345       procedure Sort (Container : in out Vector);
 346
 347       procedure Merge (Target : in out Vector; Source : in out Vector);
 348
 349    end Generic_Sorting;
 350
 351    function Left (Container : Vector; Position : Cursor) return Vector with
 352      Pre => Has_Element (Container, Position) or else Position = No_Element;
 353
 354    function Right (Container : Vector; Position : Cursor) return Vector with
 355      Pre => Has_Element (Container, Position) or else Position = No_Element;
 356
 357 private
 358
 359    pragma Inline (First_Index);
 360    pragma Inline (Last_Index);
 361    pragma Inline (Element);
 362    pragma Inline (First_Element);
 363    pragma Inline (Last_Element);
 364    pragma Inline (Replace_Element);
 365    pragma Inline (Contains);
 366    pragma Inline (Next);
 367    pragma Inline (Previous);
 368
 369    type Elements_Array is array (Count_Type range <>) of Element_Type;
 370    function "=" (L, R : Elements_Array) return Boolean is abstract;
 371
 372    type Vector (Capacity : Count_Type) is record
 373       Elements : Elements_Array (1 .. Capacity);
 374       Last     : Extended_Index := No_Index;
 375    end record;
 376
 377    type Cursor is record
 378       Valid : Boolean    := True;
 379       Index : Index_Type := Index_Type'First;
 380    end record;
 381
 382    Empty_Vector : constant Vector := (Capacity => 0, others => <>);
 383
 384    No_Element : constant Cursor := (Valid => False, Index => Index_Type'First);
 385
 386 end Ada.Containers.Formal_Vectors;