2011-12-05 Bob Duff <duff@adacore.com>

[pf3gnuchains/gcc-fork.git] / gcc / ada / a-cforse.ads

diff --git a/gcc/ada/a-cforse.ads b/gcc/ada/a-cforse.ads
index 92c4e93..03203cd 100644 (file)
--- a/gcc/ada/a-cforse.ads
+++ b/gcc/ada/a-cforse.ads
@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2010, Free Software Foundation, Inc.              --
+--          Copyright (C) 2004-2011, 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 --
@@ -29,12 +29,32 @@
 -- <http://www.gnu.org/licenses/>.                                          --
 ------------------------------------------------------------------------------
 
+--  This spec is derived from package Ada.Containers.Bounded_Ordered_Sets in
+--  the Ada 2012 RM. The modifications are to facilitate formal proofs by
+--  making it easier to express properties.
+
+--  The modifications are:
+
+--    A parameter for the container is added to every function reading the
+--    content of a container: Key, Element, Next, Query_Element, Previous,
+--    Has_Element, Iterate, Reverse_Iterate. This change is motivated by the
+--    need to have cursors which are valid on different containers (typically
+--    a container C and its previous version C'Old) for expressing properties,
+--    which is not possible if cursors encapsulate an access to the underlying
+--    container. The operators "<" and ">" that could not be modified that way
+--    have been removed.
+
+--    There are three new functions:
+
+--      function Strict_Equal (Left, Right : Set) return Boolean;
+--      function Left  (Container : Set; Position : Cursor) return Set;
+--      function Right (Container : Set; Position : Cursor) return Set;
+
+--    See detailed specifications for these subprograms
+
 private with Ada.Containers.Red_Black_Trees;
 private with Ada.Streams;
 
-with Ada.Containers;
-use Ada.Containers;
-
 generic
    type Element_Type is private;
 
@@ -47,6 +67,7 @@ package Ada.Containers.Formal_Ordered_Sets is
    function Equivalent_Elements (Left, Right : Element_Type) return Boolean;
 
    type Set (Capacity : Count_Type) is tagged private;
+   --  why is this commented out ???
    --  pragma Preelaborable_Initialization (Set);
 
    type Cursor is private;
@@ -181,8 +202,8 @@ package Ada.Containers.Formal_Ordered_Sets is
 
    procedure Reverse_Iterate
      (Container : Set;
-      Process   :
-        not null access procedure (Container : Set; Position : Cursor));
+      Process   : not null access
+                    procedure (Container : Set; Position : Cursor));
 
    generic
       type Key_Type (<>) is private;
@@ -220,15 +241,23 @@ package Ada.Containers.Formal_Ordered_Sets is
         (Container : in out Set;
          Position  : Cursor;
          Process   : not null access
-           procedure (Element : in out Element_Type));
+                       procedure (Element : in out Element_Type));
 
    end Generic_Keys;
 
    function Strict_Equal (Left, Right : Set) return Boolean;
+   --  Strict_Equal returns True if the containers are physically equal, i.e.
+   --  they are structurally equal (function "=" returns True) and that they
+   --  have the same set of cursors.
 
-   function Left (Container : Set; Position : Cursor) return Set;
-
+   function Left  (Container : Set; Position : Cursor) return Set;
    function Right (Container : Set; Position : Cursor) return Set;
+   --  Left returns a container containing all elements preceding Position
+   --  (excluded) in Container. Right returns a container containing all
+   --  elements following Position (included) in Container. These two new
+   --  functions can be used to express invariant properties in loops which
+   --  iterate over containers. Left returns the part of the container already
+   --  scanned and Right the part not scanned yet.
 
 private
 
@@ -237,27 +266,18 @@ private
 
    type Node_Type is record
       Has_Element : Boolean := False;
-      Parent  : Count_Type;
-      Left    : Count_Type;
-      Right   : Count_Type;
+      Parent  : Count_Type := 0;
+      Left    : Count_Type := 0;
+      Right   : Count_Type := 0;
       Color   : Red_Black_Trees.Color_Type;
       Element : Element_Type;
    end record;
 
-   type Kind is (Plain, Part);
-
    package Tree_Types is
      new Red_Black_Trees.Generic_Bounded_Tree_Types (Node_Type);
 
-   type Tree_Type_Access is access all Tree_Types.Tree_Type;
-
-   type Set (Capacity : Count_Type) is tagged record
-      Tree   : Tree_Type_Access := new Tree_Types.Tree_Type (Capacity);
-      K      : Kind := Plain;
-      Length : Count_Type := 0;
-      First  : Count_Type := 0;
-      Last   : Count_Type := 0;
-   end record;
+   type Set (Capacity : Count_Type) is
+     new Tree_Types.Tree_Type (Capacity) with null record;
 
    use Red_Black_Trees;
    use Ada.Streams;
@@ -266,7 +286,7 @@ private
    for Set_Access'Storage_Size use 0;
 
    type Cursor is record
-      Node      : Count_Type;
+      Node : Count_Type;
    end record;
 
    procedure Write
@@ -295,7 +315,6 @@ private
 
    for Set'Read use Read;
 
-   Empty_Set : constant Set :=
-                 (Capacity => 0, others => <>);
+   Empty_Set : constant Set := (Capacity => 0, others => <>);
 
 end Ada.Containers.Formal_Ordered_Sets;