gcc/ada/a-cofuse.ads

   1 ------------------------------------------------------------------------------
   2 --                                                                          --
   3 --                         GNAT LIBRARY COMPONENTS                          --
   4 --                                                                          --
   5 --                      ADA.CONTAINERS.FUNCTIONAL_SETS                      --
   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 Element_Type (<>) is private;
  37
  38    with function Equivalent_Elements
  39      (Left  : Element_Type;
  40       Right : Element_Type) return Boolean is "=";
  41
  42    Enable_Handling_Of_Equivalence : Boolean := True;
  43    --  This constant should only be set to False when no particular handling
  44    --  of equivalence over elements is needed, that is, Equivalent_Elements
  45    --  defines an element uniquely.
  46
  47 package Ada.Containers.Functional_Sets with SPARK_Mode is
  48
  49    type Set is private with
  50      Default_Initial_Condition => Is_Empty (Set),
  51      Iterable                  => (First       => Iter_First,
  52                                    Next        => Iter_Next,
  53                                    Has_Element => Iter_Has_Element,
  54                                    Element     => Iter_Element);
  55    --  Sets are empty when default initialized.
  56    --  "For in" quantification over sets should not be used.
  57    --  "For of" quantification over sets iterates over elements.
  58    --  Note that, for proof, "for of" quantification is understood modulo
  59    --  equivalence (the range of quantification comprises all the elements that
  60    --  are equivalent to any element of the set).
  61
  62    -----------------------
  63    --  Basic operations --
  64    -----------------------
  65
  66    --  Sets are axiomatized using Contains, which encodes whether an element is
  67    --  contained in a set. The length of a set is also added to protect Add
  68    --  against overflows but it is not actually modeled.
  69
  70    function Contains (Container : Set; Item : Element_Type) return Boolean with
  71    --  Return True if Item is contained in Container
  72
  73      Global => null,
  74      Post   =>
  75        (if Enable_Handling_Of_Equivalence then
  76
  77           --  Contains returns the same result on all equivalent elements
  78
  79           (if (for some E of Container => Equivalent_Elements (E, Item)) then
  80               Contains'Result));
  81
  82    function Length (Container : Set) return Count_Type with
  83      Global => null;
  84    --  Return the number of elements in Container
  85
  86    ------------------------
  87    -- Property Functions --
  88    ------------------------
  89
  90    function "<=" (Left : Set; Right : Set) return Boolean with
  91    --  Set inclusion
  92
  93      Global => null,
  94      Post   => "<="'Result = (for all Item of Left => Contains (Right, Item));
  95
  96    function "=" (Left : Set; Right : Set) return Boolean with
  97    --  Extensional equality over sets
  98
  99      Global => null,
 100      Post   => "="'Result = (Left <= Right and Right <= Left);
 101
 102    pragma Warnings (Off, "unused variable ""Item""");
 103    function Is_Empty (Container : Set) return Boolean with
 104    --  A set is empty if it contains no element
 105
 106      Global => null,
 107      Post   =>
 108        Is_Empty'Result = (for all Item of Container => False)
 109          and Is_Empty'Result = (Length (Container) = 0);
 110    pragma Warnings (On, "unused variable ""Item""");
 111
 112    function Included_Except
 113      (Left  : Set;
 114       Right : Set;
 115       Item  : Element_Type) return Boolean
 116    --  Return True if Left contains only elements of Right except possibly
 117    --  Item.
 118
 119    with
 120      Global => null,
 121      Post   =>
 122        Included_Except'Result =
 123          (for all E of Left =>
 124            Contains (Right, E) or Equivalent_Elements (E, Item));
 125
 126    function Includes_Intersection
 127      (Container : Set;
 128       Left      : Set;
 129       Right     : Set) return Boolean
 130    with
 131    --  Return True if every element of the intersection of Left and Right is
 132    --  in Container.
 133
 134      Global => null,
 135      Post   =>
 136        Includes_Intersection'Result =
 137          (for all Item of Left =>
 138            (if Contains (Right, Item) then Contains (Container, Item)));
 139
 140    function Included_In_Union
 141      (Container : Set;
 142       Left      : Set;
 143       Right     : Set) return Boolean
 144    with
 145    --  Return True if every element of Container is the union of Left and Right
 146
 147      Global => null,
 148      Post   =>
 149        Included_In_Union'Result =
 150          (for all Item of Container =>
 151            Contains (Left, Item) or Contains (Right, Item));
 152
 153    function Is_Singleton
 154      (Container : Set;
 155       New_Item  : Element_Type) return Boolean
 156    with
 157    --  Return True Container only contains New_Item
 158
 159      Global => null,
 160      Post   =>
 161        Is_Singleton'Result =
 162          (for all Item of Container => Equivalent_Elements (Item, New_Item));
 163
 164    function Not_In_Both
 165      (Container : Set;
 166       Left      : Set;
 167       Right     : Set) return Boolean
 168    --  Return True if there are no elements in Container that are in Left and
 169    --  Right.
 170
 171    with
 172      Global => null,
 173      Post   =>
 174        Not_In_Both'Result =
 175          (for all Item of Container =>
 176             not Contains (Left, Item) or not Contains (Right, Item));
 177
 178    function No_Overlap (Left : Set; Right : Set) return Boolean with
 179    --  Return True if there are no equivalent elements in Left and Right
 180
 181      Global => null,
 182      Post   =>
 183        No_Overlap'Result =
 184          (for all Item of Left => not Contains (Right, Item));
 185
 186    function Num_Overlaps (Left : Set; Right : Set) return Count_Type with
 187    --  Number of elements that are both in Left and Right
 188
 189      Global => null,
 190      Post   =>
 191        Num_Overlaps'Result = Length (Intersection (Left, Right))
 192          and (if Left <= Right then Num_Overlaps'Result = Length (Left)
 193               else Num_Overlaps'Result < Length (Left))
 194          and (if Right <= Left then Num_Overlaps'Result = Length (Right)
 195               else Num_Overlaps'Result < Length (Right))
 196          and (Num_Overlaps'Result = 0) = No_Overlap (Left, Right);
 197
 198    ----------------------------
 199    -- Construction Functions --
 200    ----------------------------
 201
 202    --  For better efficiency of both proofs and execution, avoid using
 203    --  construction functions in annotations and rather use property functions.
 204
 205    function Add (Container : Set; Item : Element_Type) return Set with
 206    --  Return a new set containing all the elements of Container plus E
 207
 208      Global => null,
 209      Pre    =>
 210        not Contains (Container, Item)
 211        and Length (Container) < Count_Type'Last,
 212      Post   =>
 213        Length (Add'Result) = Length (Container) + 1
 214          and Contains (Add'Result, Item)
 215          and Container <= Add'Result
 216          and Included_Except (Add'Result, Container, Item);
 217
 218    function Remove (Container : Set; Item : Element_Type) return Set with
 219    --  Return a new set containing all the elements of Container except E
 220
 221      Global => null,
 222      Pre    => Contains (Container, Item),
 223      Post   =>
 224        Length (Remove'Result) = Length (Container) - 1
 225          and not Contains (Remove'Result, Item)
 226          and Remove'Result <= Container
 227          and Included_Except (Container, Remove'Result, Item);
 228
 229    function Intersection (Left : Set; Right : Set) return Set with
 230    --  Returns the intersection of Left and Right
 231
 232      Global => null,
 233      Post   =>
 234        Intersection'Result <= Left
 235          and Intersection'Result <= Right
 236          and Includes_Intersection (Intersection'Result, Left, Right);
 237
 238    function Union (Left : Set; Right : Set) return Set with
 239    --  Returns the union of Left and Right
 240
 241      Global => null,
 242      Pre    =>
 243        Length (Left) - Num_Overlaps (Left, Right) <=
 244          Count_Type'Last - Length (Right),
 245      Post   =>
 246        Length (Union'Result) =
 247          Length (Left) - Num_Overlaps (Left, Right) + Length (Right)
 248            and Left <= Union'Result
 249            and Right <= Union'Result
 250            and Included_In_Union (Union'Result, Left, Right);
 251
 252    ---------------------------
 253    --  Iteration Primitives --
 254    ---------------------------
 255
 256    type Private_Key is private;
 257
 258    function Iter_First (Container : Set) return Private_Key with
 259      Global => null;
 260
 261    function Iter_Has_Element
 262      (Container : Set;
 263       Key       : Private_Key) return Boolean
 264    with
 265      Global => null;
 266
 267    function Iter_Next
 268      (Container : Set;
 269       Key       : Private_Key) return Private_Key
 270    with
 271      Global => null,
 272      Pre    => Iter_Has_Element (Container, Key);
 273
 274    function Iter_Element
 275      (Container : Set;
 276       Key       : Private_Key) return Element_Type
 277    with
 278      Global => null,
 279      Pre    => Iter_Has_Element (Container, Key);
 280    pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Contains);
 281
 282 private
 283
 284    pragma SPARK_Mode (Off);
 285
 286    subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
 287
 288    function "="
 289      (Left  : Element_Type;
 290       Right : Element_Type) return Boolean renames Equivalent_Elements;
 291
 292    package Containers is new Ada.Containers.Functional_Base
 293      (Element_Type => Element_Type,
 294       Index_Type   => Positive_Count_Type);
 295
 296    type Set is record
 297       Content : Containers.Container;
 298    end record;
 299
 300    type Private_Key is new Count_Type;
 301
 302    function Iter_First (Container : Set) return Private_Key is (1);
 303
 304    function Iter_Has_Element
 305      (Container : Set;
 306       Key       : Private_Key) return Boolean
 307    is
 308      (Count_Type (Key) in 1 .. Containers.Length (Container.Content));
 309
 310    function Iter_Next
 311      (Container : Set;
 312       Key       : Private_Key) return Private_Key
 313    is
 314      (if Key = Private_Key'Last then 0 else Key + 1);
 315
 316    function Iter_Element
 317      (Container : Set;
 318       Key       : Private_Key) return Element_Type
 319    is
 320      (Containers.Get (Container.Content, Count_Type (Key)));
 321
 322 end Ada.Containers.Functional_Sets;