diff gcc/ada/libgnat/a-cofuma.ads @ 111:04ced10e8804

gcc 7
author kono
date Fri, 27 Oct 2017 22:46:09 +0900
parents
children 84e7813d76e9
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/gcc/ada/libgnat/a-cofuma.ads	Fri Oct 27 22:46:09 2017 +0900
@@ -0,0 +1,361 @@
+------------------------------------------------------------------------------
+--                                                                          --
+--                         GNAT LIBRARY COMPONENTS                          --
+--                                                                          --
+--                      ADA.CONTAINERS.FUNCTIONAL_MAPS                      --
+--                                                                          --
+--                                 S p e c                                  --
+--                                                                          --
+--          Copyright (C) 2016-2017, Free Software Foundation, Inc.         --
+--                                                                          --
+-- This specification is derived from the Ada Reference Manual for use with --
+-- GNAT. The copyright notice above, and the license provisions that follow --
+-- apply solely to the  contents of the part following the private keyword. --
+--                                                                          --
+-- GNAT is free software;  you can  redistribute it  and/or modify it under --
+-- terms of the  GNU General Public License as published  by the Free Soft- --
+-- ware  Foundation;  either version 3,  or (at your option) any later ver- --
+-- sion.  GNAT is distributed in the hope that it will be useful, but WITH- --
+-- OUT ANY WARRANTY;  without even the  implied warranty of MERCHANTABILITY --
+-- or FITNESS FOR A PARTICULAR PURPOSE.                                     --
+--                                                                          --
+-- As a special exception under Section 7 of GPL version 3, you are granted --
+-- additional permissions described in the GCC Runtime Library Exception,   --
+-- version 3.1, as published by the Free Software Foundation.               --
+--                                                                          --
+-- You should have received a copy of the GNU General Public License and    --
+-- a copy of the GCC Runtime Library Exception along with this program;     --
+-- see the files COPYING3 and COPYING.RUNTIME respectively.  If not, see    --
+-- <http://www.gnu.org/licenses/>.                                          --
+------------------------------------------------------------------------------
+
+pragma Ada_2012;
+private with Ada.Containers.Functional_Base;
+
+generic
+   type Key_Type (<>) is private;
+   type Element_Type (<>)  is private;
+
+   with function Equivalent_Keys
+     (Left  : Key_Type;
+      Right : Key_Type) return Boolean is "=";
+
+   Enable_Handling_Of_Equivalence : Boolean := True;
+   --  This constant should only be set to False when no particular handling
+   --  of equivalence over keys is needed, that is, Equivalent_Keys defines a
+   --  key uniquely.
+
+package Ada.Containers.Functional_Maps with SPARK_Mode is
+
+   type Map is private with
+     Default_Initial_Condition => Is_Empty (Map) and Length (Map) = 0,
+     Iterable                  => (First       => Iter_First,
+                                   Next        => Iter_Next,
+                                   Has_Element => Iter_Has_Element,
+                                   Element     => Iter_Element);
+   --  Maps are empty when default initialized.
+   --  "For in" quantification over maps should not be used.
+   --  "For of" quantification over maps iterates over keys.
+   --  Note that, for proof, "for of" quantification is understood modulo
+   --  equivalence (the range of quantification comprises all the keys that are
+   --  equivalent to any key of the map).
+
+   -----------------------
+   --  Basic operations --
+   -----------------------
+
+   --  Maps are axiomatized using Has_Key and Get, encoding respectively the
+   --  presence of a key in a map and an accessor to elements associated with
+   --  its keys. The length of a map is also added to protect Add against
+   --  overflows but it is not actually modeled.
+
+   function Has_Key (Container : Map; Key : Key_Type) return Boolean with
+   --  Return True if Key is present in Container
+
+     Global => null,
+     Post   =>
+       (if Enable_Handling_Of_Equivalence then
+
+          --  Has_Key returns the same result on all equivalent keys
+
+          (if (for some K of Container => Equivalent_Keys (K, Key)) then
+              Has_Key'Result));
+
+   function Get (Container : Map; Key : Key_Type) return Element_Type with
+   --  Return the element associated with Key in Container
+
+     Global => null,
+     Pre    => Has_Key (Container, Key),
+     Post   =>
+       (if Enable_Handling_Of_Equivalence then
+
+          --  Get returns the same result on all equivalent keys
+
+          Get'Result = W_Get (Container, Witness (Container, Key))
+            and (for all K of Container =>
+                  (Equivalent_Keys (K, Key) =
+                    (Witness (Container, Key) = Witness (Container, K)))));
+
+   function Length (Container : Map) return Count_Type with
+     Global => null;
+   --  Return the number of mappings in Container
+
+   ------------------------
+   -- Property Functions --
+   ------------------------
+
+   function "<=" (Left : Map; Right : Map) return Boolean with
+   --  Map inclusion
+
+     Global => null,
+     Post   =>
+       "<="'Result =
+         (for all Key of Left =>
+           Has_Key (Right, Key) and then Get (Right, Key) = Get (Left, Key));
+
+   function "=" (Left : Map; Right : Map) return Boolean with
+   --  Extensional equality over maps
+
+     Global => null,
+     Post   =>
+       "="'Result =
+         ((for all Key of Left =>
+            Has_Key (Right, Key)
+              and then Get (Right, Key) = Get (Left, Key))
+              and (for all Key of Right => Has_Key (Left, Key)));
+
+   pragma Warnings (Off, "unused variable ""Key""");
+   function Is_Empty (Container : Map) return Boolean with
+   --  A map is empty if it contains no key
+
+     Global => null,
+     Post   => Is_Empty'Result = (for all Key of Container => False);
+   pragma Warnings (On, "unused variable ""Key""");
+
+   function Keys_Included (Left : Map; Right : Map) return Boolean
+   --  Returns True if every Key of Left is in Right
+
+   with
+     Global => null,
+     Post   =>
+       Keys_Included'Result = (for all Key of Left => Has_Key (Right, Key));
+
+   function Same_Keys (Left : Map; Right : Map) return Boolean
+   --  Returns True if Left and Right have the same keys
+
+   with
+     Global => null,
+     Post   =>
+       Same_Keys'Result =
+         (Keys_Included (Left, Right)
+           and Keys_Included (Left => Right, Right => Left));
+   pragma Annotate (GNATprove, Inline_For_Proof, Same_Keys);
+
+   function Keys_Included_Except
+     (Left    : Map;
+      Right   : Map;
+      New_Key : Key_Type) return Boolean
+   --  Returns True if Left contains only keys of Right and possibly New_Key
+
+   with
+     Global => null,
+     Post   =>
+       Keys_Included_Except'Result =
+         (for all Key of Left =>
+           (if not Equivalent_Keys (Key, New_Key) then
+               Has_Key (Right, Key)));
+
+   function Keys_Included_Except
+     (Left  : Map;
+      Right : Map;
+      X     : Key_Type;
+      Y     : Key_Type) return Boolean
+   --  Returns True if Left contains only keys of Right and possibly X and Y
+
+   with
+     Global => null,
+     Post   =>
+       Keys_Included_Except'Result =
+         (for all Key of Left =>
+           (if not Equivalent_Keys (Key, X)
+              and not Equivalent_Keys (Key, Y)
+            then
+               Has_Key (Right, Key)));
+
+   function Elements_Equal_Except
+     (Left    : Map;
+      Right   : Map;
+      New_Key : Key_Type) return Boolean
+   --  Returns True if all the keys of Left are mapped to the same elements in
+   --  Left and Right except New_Key.
+
+   with
+     Global => null,
+     Post   =>
+       Elements_Equal_Except'Result =
+         (for all Key of Left =>
+           (if not Equivalent_Keys (Key, New_Key) then
+               Has_Key (Right, Key)
+                 and then Get (Left, Key) = Get (Right, Key)));
+
+   function Elements_Equal_Except
+     (Left  : Map;
+      Right : Map;
+      X     : Key_Type;
+      Y     : Key_Type) return Boolean
+   --  Returns True if all the keys of Left are mapped to the same elements in
+   --  Left and Right except X and Y.
+
+   with
+     Global => null,
+     Post   =>
+       Elements_Equal_Except'Result =
+         (for all Key of Left =>
+           (if not Equivalent_Keys (Key, X)
+              and not Equivalent_Keys (Key, Y)
+            then
+               Has_Key (Right, Key)
+                 and then Get (Left, Key) = Get (Right, Key)));
+
+   ----------------------------
+   -- Construction Functions --
+   ----------------------------
+
+   --  For better efficiency of both proofs and execution, avoid using
+   --  construction functions in annotations and rather use property functions.
+
+   function Add
+     (Container : Map;
+      New_Key   : Key_Type;
+      New_Item  : Element_Type) return Map
+   --  Returns Container augmented with the mapping Key -> New_Item
+
+   with
+     Global => null,
+     Pre    =>
+       not Has_Key (Container, New_Key)
+         and Length (Container) < Count_Type'Last,
+     Post   =>
+       Length (Container) + 1 = Length (Add'Result)
+         and Has_Key (Add'Result, New_Key)
+         and Get (Add'Result, New_Key) = New_Item
+         and Container <= Add'Result
+         and Keys_Included_Except (Add'Result, Container, New_Key);
+
+   function Set
+     (Container : Map;
+      Key       : Key_Type;
+      New_Item  : Element_Type) return Map
+   --  Returns Container, where the element associated with Key has been
+   --  replaced by New_Item.
+
+   with
+     Global => null,
+     Pre    => Has_Key (Container, Key),
+     Post   =>
+       Length (Container) = Length (Set'Result)
+         and Get (Set'Result, Key) = New_Item
+         and Same_Keys (Container, Set'Result)
+         and Elements_Equal_Except (Container, Set'Result, Key);
+
+   ------------------------------
+   --  Handling of Equivalence --
+   ------------------------------
+
+   --  These functions are used to specify that Get returns the same value on
+   --  equivalent keys. They should not be used directly in user code.
+
+   function Has_Witness (Container : Map; Witness : Count_Type) return Boolean
+   with
+     Ghost,
+     Global => null;
+   --  Returns True if there is a key with witness Witness in Container
+
+   function Witness (Container : Map; Key : Key_Type) return Count_Type with
+   --  Returns the witness of Key in Container
+
+     Ghost,
+     Global => null,
+     Pre    => Has_Key (Container, Key),
+     Post   => Has_Witness (Container, Witness'Result);
+
+   function W_Get (Container : Map; Witness : Count_Type) return Element_Type
+   with
+   --  Returns the element associated with a witness in Container
+
+     Ghost,
+     Global => null,
+     Pre    => Has_Witness (Container, Witness);
+
+   ---------------------------
+   --  Iteration Primitives --
+   ---------------------------
+
+   type Private_Key is private;
+
+   function Iter_First (Container : Map) return Private_Key with
+     Global => null;
+
+   function Iter_Has_Element
+     (Container : Map;
+      Key       : Private_Key) return Boolean
+   with
+     Global => null;
+
+   function Iter_Next (Container : Map; Key : Private_Key) return Private_Key
+   with
+     Global => null,
+     Pre    => Iter_Has_Element (Container, Key);
+
+   function Iter_Element (Container : Map; Key : Private_Key) return Key_Type
+   with
+     Global => null,
+     Pre    => Iter_Has_Element (Container, Key);
+   pragma Annotate (GNATprove, Iterable_For_Proof, "Contains", Has_Key);
+
+private
+
+   pragma SPARK_Mode (Off);
+
+   function "="
+     (Left  : Key_Type;
+      Right : Key_Type) return Boolean renames Equivalent_Keys;
+
+   subtype Positive_Count_Type is Count_Type range 1 .. Count_Type'Last;
+
+   package Element_Containers is new Ada.Containers.Functional_Base
+     (Element_Type => Element_Type,
+      Index_Type   => Positive_Count_Type);
+
+   package Key_Containers is new Ada.Containers.Functional_Base
+     (Element_Type => Key_Type,
+      Index_Type   => Positive_Count_Type);
+
+   type Map is record
+      Keys     : Key_Containers.Container;
+      Elements : Element_Containers.Container;
+   end record;
+
+   type Private_Key is new Count_Type;
+
+   function Iter_First (Container : Map) return Private_Key is (1);
+
+   function Iter_Has_Element
+     (Container : Map;
+      Key       : Private_Key) return Boolean
+   is
+     (Count_Type (Key) in 1 .. Key_Containers.Length (Container.Keys));
+
+   function Iter_Next
+     (Container : Map;
+      Key       : Private_Key) return Private_Key
+   is
+     (if Key = Private_Key'Last then 0 else Key + 1);
+
+   function Iter_Element
+     (Container : Map;
+      Key       : Private_Key) return Key_Type
+   is
+     (Key_Containers.Get (Container.Keys, Count_Type (Key)));
+
+end Ada.Containers.Functional_Maps;