gcc/ada/libgnat/a-cofuve.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT LIBRARY COMPONENTS                          --
   4 --                                                                          --
   5 --                    ADA.CONTAINERS.FUNCTIONAL_VECTORS                     --
   6 --                                                                          --
   7 --                                 S p e c                                  --
   8 --                                                                          --
   9 --          Copyright (C) 2016-2017, 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 pragma Ada_2012;
  33 private with Ada.Containers.Functional_Base;
  34
  35 generic
  36    type Index_Type is (<>);
  37    --  To avoid Constraint_Error being raised at run time, Index_Type'Base
  38    --  should have at least one more element at the low end than Index_Type.
  39
  40    type Element_Type (<>) is private;
  41
  42 package Ada.Containers.Functional_Vectors with SPARK_Mode is
  43
  44    subtype Extended_Index is Index_Type'Base range
  45      Index_Type'Pred (Index_Type'First) .. Index_Type'Last;
  46    --  Index_Type with one more element at the low end of the range.
  47    --  This type is never used but it forces GNATprove to check that there is
  48    --  room for one more element at the low end of Index_Type.
  49
  50    type Sequence is private
  51      with Default_Initial_Condition => Length (Sequence) = 0,
  52      Iterable => (First       => Iter_First,
  53                   Has_Element => Iter_Has_Element,
  54                   Next        => Iter_Next,
  55                   Element     => Get);
  56    --  Sequences are empty when default initialized.
  57    --  Quantification over sequences can be done using the regular
  58    --  quantification over its range or directly on its elements with "for of".
  59
  60    -----------------------
  61    --  Basic operations --
  62    -----------------------
  63
  64    --  Sequences are axiomatized using Length and Get, providing respectively
  65    --  the length of a sequence and an accessor to its Nth element:
  66
  67    function Length (Container : Sequence) return Count_Type with
  68    --  Length of a sequence
  69
  70      Global => null,
  71      Post   =>
  72        (Index_Type'Pos (Index_Type'First) - 1) + Length'Result <=
  73          Index_Type'Pos (Index_Type'Last);
  74
  75    function Get
  76      (Container : Sequence;
  77       Position  : Extended_Index) return Element_Type
  78    --  Access the Element at position Position in Container
  79
  80    with
  81      Global => null,
  82      Pre    => Position in Index_Type'First .. Last (Container);
  83
  84    function Last (Container : Sequence) return Extended_Index with
  85    --  Last index of a sequence
  86
  87      Global => null,
  88      Post =>
  89        Last'Result =
  90          Index_Type'Val ((Index_Type'Pos (Index_Type'First) - 1) +
  91            Length (Container));
  92    pragma Annotate (GNATprove, Inline_For_Proof, Last);
  93
  94    function First return Extended_Index is (Index_Type'First);
  95    --  First index of a sequence
  96
  97    ------------------------
  98    -- Property Functions --
  99    ------------------------
 100
 101    function "=" (Left : Sequence; Right : Sequence) return Boolean with
 102    --  Extensional equality over sequences
 103
 104      Global => null,
 105      Post   =>
 106        "="'Result =
 107          (Length (Left) = Length (Right)
 108            and then (for all N in Index_Type'First .. Last (Left) =>
 109                       Get (Left, N) = Get (Right, N)));
 110    pragma Annotate (GNATprove, Inline_For_Proof, "=");
 111
 112    function "<" (Left : Sequence; Right : Sequence) return Boolean with
 113    --  Left is a strict subsequence of Right
 114
 115      Global => null,
 116      Post   =>
 117        "<"'Result =
 118          (Length (Left) < Length (Right)
 119            and then (for all N in Index_Type'First .. Last (Left) =>
 120                       Get (Left, N) = Get (Right, N)));
 121    pragma Annotate (GNATprove, Inline_For_Proof, "<");
 122
 123    function "<=" (Left : Sequence; Right : Sequence) return Boolean with
 124    --  Left is a subsequence of Right
 125
 126      Global => null,
 127      Post   =>
 128        "<="'Result =
 129          (Length (Left) <= Length (Right)
 130            and then (for all N in Index_Type'First .. Last (Left) =>
 131                       Get (Left, N) = Get (Right, N)));
 132    pragma Annotate (GNATprove, Inline_For_Proof, "<=");
 133
 134    function Contains
 135      (Container : Sequence;
 136       Fst       : Index_Type;
 137       Lst       : Extended_Index;
 138       Item      : Element_Type) return Boolean
 139    --  Returns True if Item occurs in the range from Fst to Lst of Container
 140
 141    with
 142      Global => null,
 143      Pre    => Lst <= Last (Container),
 144      Post   =>
 145        Contains'Result =
 146          (for some I in Fst .. Lst => Get (Container, I) = Item);
 147    pragma Annotate (GNATprove, Inline_For_Proof, Contains);
 148
 149    function Constant_Range
 150      (Container : Sequence;
 151       Fst       : Index_Type;
 152       Lst       : Extended_Index;
 153       Item      : Element_Type) return Boolean
 154    --  Returns True if every element of the range from Fst to Lst of Container
 155    --  is equal to Item.
 156
 157    with
 158      Global => null,
 159      Pre    => Lst <= Last (Container),
 160      Post   =>
 161        Constant_Range'Result =
 162          (for all I in Fst .. Lst => Get (Container, I) = Item);
 163    pragma Annotate (GNATprove, Inline_For_Proof, Constant_Range);
 164
 165    function Equal_Except
 166      (Left     : Sequence;
 167       Right    : Sequence;
 168       Position : Index_Type) return Boolean
 169    --  Returns True is Left and Right are the same except at position Position
 170
 171    with
 172      Global => null,
 173      Pre    => Position <= Last (Left),
 174      Post   =>
 175        Equal_Except'Result =
 176          (Length (Left) = Length (Right)
 177            and then (for all I in Index_Type'First .. Last (Left) =>
 178                       (if I /= Position then Get (Left, I) = Get (Right, I))));
 179    pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except);
 180
 181    function Equal_Except
 182      (Left  : Sequence;
 183       Right : Sequence;
 184       X     : Index_Type;
 185       Y     : Index_Type) return Boolean
 186    --  Returns True is Left and Right are the same except at positions X and Y
 187
 188    with
 189      Global => null,
 190      Pre    => X <= Last (Left) and Y <= Last (Left),
 191      Post   =>
 192        Equal_Except'Result =
 193          (Length (Left) = Length (Right)
 194            and then (for all I in Index_Type'First .. Last (Left) =>
 195                       (if I /= X and I /= Y then
 196                           Get (Left, I) = Get (Right, I))));
 197    pragma Annotate (GNATprove, Inline_For_Proof, Equal_Except);
 198
 199    function Range_Equal
 200      (Left  : Sequence;
 201       Right : Sequence;
 202       Fst   : Index_Type;
 203       Lst   : Extended_Index) return Boolean
 204    --  Returns True if the ranges from Fst to Lst contain the same elements in
 205    --  Left and Right.
 206
 207    with
 208      Global => null,
 209      Pre    => Lst <= Last (Left) and Lst <= Last (Right),
 210      Post   =>
 211        Range_Equal'Result =
 212          (for all I in Fst .. Lst => Get (Left, I) = Get (Right, I));
 213    pragma Annotate (GNATprove, Inline_For_Proof, Range_Equal);
 214
 215    function Range_Shifted
 216      (Left   : Sequence;
 217       Right  : Sequence;
 218       Fst    : Index_Type;
 219       Lst    : Extended_Index;
 220       Offset : Count_Type'Base) return Boolean
 221    --  Returns True if the range from Fst to Lst in Left contains the same
 222    --  elements as the range from Fst + Offset to Lst + Offset in Right.
 223
 224    with
 225      Global => null,
 226      Pre    =>
 227        Lst <= Last (Left)
 228          and then
 229            (if Offset < 0 then
 230               Index_Type'Pos (Index_Type'Base'First) - Offset <=
 231               Index_Type'Pos (Index_Type'First))
 232          and then
 233            (if Fst <= Lst then
 234               Offset in
 235                 Index_Type'Pos (Index_Type'First) - Index_Type'Pos (Fst) ..
 236                   (Index_Type'Pos (Index_Type'First) - 1) + Length (Right) -
 237                    Index_Type'Pos (Lst)),
 238      Post   =>
 239        Range_Shifted'Result =
 240          ((for all I in Fst .. Lst =>
 241             Get (Left, I) =
 242             Get (Right, Index_Type'Val (Index_Type'Pos (I) + Offset)))
 243           and
 244             (for all I in Index_Type'Val (Index_Type'Pos (Fst) + Offset) ..
 245                Index_Type'Val (Index_Type'Pos (Lst) + Offset)
 246              =>
 247                Get (Left, Index_Type'Val (Index_Type'Pos (I) - Offset)) =
 248                Get (Right, I)));
 249    pragma Annotate (GNATprove, Inline_For_Proof, Range_Shifted);
 250
 251    ----------------------------
 252    -- Construction Functions --
 253    ----------------------------
 254
 255    --  For better efficiency of both proofs and execution, avoid using
 256    --  construction functions in annotations and rather use property functions.
 257
 258    function Set
 259      (Container : Sequence;
 260       Position  : Index_Type;
 261       New_Item  : Element_Type) return Sequence
 262    --  Returns a new sequence which contains the same elements as Container
 263    --  except for the one at position Position which is replaced by New_Item.
 264
 265    with
 266      Global => null,
 267      Pre    => Position in Index_Type'First .. Last (Container),
 268      Post   =>
 269        Get (Set'Result, Position) = New_Item
 270          and then Equal_Except (Container, Set'Result, Position);
 271
 272    function Add (Container : Sequence; New_Item : Element_Type) return Sequence
 273    --  Returns a new sequence which contains the same elements as Container
 274    --  plus New_Item at the end.
 275
 276    with
 277      Global => null,
 278      Pre    =>
 279        Length (Container) < Count_Type'Last
 280          and then Last (Container) < Index_Type'Last,
 281      Post   =>
 282        Length (Add'Result) = Length (Container) + 1
 283          and then Get (Add'Result, Last (Add'Result)) = New_Item
 284          and then Container <= Add'Result;
 285
 286    function Add
 287      (Container : Sequence;
 288       Position  : Index_Type;
 289       New_Item  : Element_Type) return Sequence
 290    with
 291    --  Returns a new sequence which contains the same elements as Container
 292    --  except that New_Item has been inserted at position Position.
 293
 294      Global => null,
 295      Pre    =>
 296        Length (Container) < Count_Type'Last
 297          and then Last (Container) < Index_Type'Last
 298          and then Position <= Extended_Index'Succ (Last (Container)),
 299      Post   =>
 300        Length (Add'Result) = Length (Container) + 1
 301          and then Get (Add'Result, Position) = New_Item
 302          and then Range_Equal
 303                     (Left  => Container,
 304                      Right =>  Add'Result,
 305                      Fst   => Index_Type'First,
 306                      Lst   => Index_Type'Pred (Position))
 307          and then Range_Shifted
 308                     (Left   => Container,
 309                      Right  => Add'Result,
 310                      Fst    => Position,
 311                      Lst    => Last (Container),
 312                      Offset => 1);
 313
 314    function Remove
 315      (Container : Sequence;
 316       Position : Index_Type) return Sequence
 317    --  Returns a new sequence which contains the same elements as Container
 318    --  except that the element at position Position has been removed.
 319
 320    with
 321      Global => null,
 322      Pre    => Position in Index_Type'First .. Last (Container),
 323      Post   =>
 324        Length (Remove'Result) = Length (Container) - 1
 325          and then Range_Equal
 326                     (Left  => Container,
 327                      Right => Remove'Result,
 328                      Fst   => Index_Type'First,
 329                      Lst   => Index_Type'Pred (Position))
 330          and then Range_Shifted
 331                     (Left   => Remove'Result,
 332                      Right  => Container,
 333                      Fst    => Position,
 334                      Lst    => Last (Remove'Result),
 335                      Offset => 1);
 336
 337    ---------------------------
 338    --  Iteration Primitives --
 339    ---------------------------
 340
 341    function Iter_First (Container : Sequence) return Extended_Index with
 342      Global => null;
 343
 344    function Iter_Has_Element
 345      (Container : Sequence;
 346       Position  : Extended_Index) return Boolean
 347    with
 348      Global => null,
 349      Post   =>
 350        Iter_Has_Element'Result =
 351          (Position in Index_Type'First .. Last (Container));
 352    pragma Annotate (GNATprove, Inline_For_Proof, Iter_Has_Element);
 353
 354    function Iter_Next
 355      (Container : Sequence;
 356       Position  : Extended_Index) return Extended_Index
 357    with
 358      Global => null,
 359      Pre    => Iter_Has_Element (Container, Position);
 360
 361 private
 362
 363    pragma SPARK_Mode (Off);
 364
 365    package Containers is new Ada.Containers.Functional_Base
 366      (Index_Type   => Index_Type,
 367       Element_Type => Element_Type);
 368
 369    type Sequence is record
 370       Content : Containers.Container;
 371    end record;
 372
 373    function Iter_First (Container : Sequence) return Extended_Index is
 374      (Index_Type'First);
 375
 376    function Iter_Next
 377      (Container : Sequence;
 378       Position  : Extended_Index) return Extended_Index
 379    is
 380      (if Position = Extended_Index'Last then
 381          Extended_Index'First
 382       else
 383          Extended_Index'Succ (Position));
 384
 385    function Iter_Has_Element
 386      (Container : Sequence;
 387       Position  : Extended_Index) return Boolean
 388    is
 389      (Position in Index_Type'First ..
 390        (Index_Type'Val
 391          ((Index_Type'Pos (Index_Type'First) - 1) + Length (Container))));
 392
 393 end Ada.Containers.Functional_Vectors;