Mercurial > hg > CbC > CbC_gcc
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;