a-cfdlli.ads, [...]: Minor reformatting.

2011-08-02  Robert Dewar  <dewar@adacore.com>

	* a-cfdlli.ads, a-cfhase.ads, a-cforma.ads, a-cfhama.ads,
	a-cforse.ads, a-cofove.ads: Minor reformatting.

From-SVN: r177112

gcc/ada/ChangeLog

+2011-08-02  Robert Dewar  <dewar@adacore.com>
+
+	* a-cfdlli.ads, a-cfhase.ads, a-cforma.ads, a-cfhama.ads,
+	a-cforse.ads, a-cofove.ads: Minor reformatting.
+
 2011-08-02  Claire Dross  <dross@adacore.com>
 
 	* a-cfdlli.ads, a-cfhase.ads, a-cforma.ads, a-cfhama.ads, a-cforse.ads,

gcc/ada/a-cfdlli.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2010, Free Software Foundation, Inc.              --
+--          Copyright (C) 2004-2010, 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,19 +29,21 @@
 -- <http://www.gnu.org/licenses/>.                                          --
 ------------------------------------------------------------------------------
 
---  The specification of this package is derived from the specification
---  of package Ada.Containers.Bounded_Doubly_Linked_Lists in the Ada 2012 RM.
---  The changes are
+--  This spec is derived from Ada.Containers.Bounded_Doubly_Linked_Lists 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: Element, Next, Previous, Query_Element,
---    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,
+--    contents of a container: Next, Previous, Query_Element, Has_Element,
+--    Iterate, Reverse_Iterate, Element. 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.
 
---    There are two new functions
+--    There are two new functions:
 
 --      function Left  (Container : List; Position : Cursor) return List;
 --      function Right (Container : List; Position : Cursor) return List;
@@ -54,7 +56,7 @@
 --      scanned and Right the part not scanned yet.
 
 private with Ada.Streams;
-with Ada.Containers; use Ada.Containers;
+with Ada.Containers;
 
 generic
    type Element_Type is private;
@@ -288,10 +290,9 @@ private
 
    for List'Write use Write;
 
-   type Cursor is
-      record
-         Node      : Count_Type := 0;
-      end record;
+   type Cursor is record
+      Node : Count_Type := 0;
+   end record;
 
    procedure Read
      (Stream : not null access Root_Stream_Type'Class;

gcc/ada/a-cfhama.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2010, Free Software Foundation, Inc.              --
+--          Copyright (C) 2004-2010, 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,19 +29,20 @@
 -- <http://www.gnu.org/licenses/>.                                          --
 ------------------------------------------------------------------------------
 
---  The specification of this package is derived from the specification
---  of package Ada.Containers.Bounded_Hashed_Maps in the Ada 2012 RM.
---  The changes are
+--  This spec is derived from package Ada.Containers.Bounded_Hashed_Maps 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,
---    Has_Element, Iterate, Equivalent_Keys. 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.
+--    contents of a container: Key, Element, Next, Query_Element, Has_Element,
+--    Iterate, Equivalent_Keys. 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.
 
---    There are two new functions
+--    There are two new functions:
 
 --      function Left  (Container : Map; Position : Cursor) return Map;
 --      function Right (Container : Map; Position : Cursor) return Map;
@@ -70,6 +71,7 @@ package Ada.Containers.Formal_Hashed_Maps is
 
    type Map (Capacity : Count_Type; Modulus : Hash_Type) is tagged private;
    --  pragma Preelaborable_Initialization (Map);
+   --  why is this commented out???
 
    type Cursor is private;
    pragma Preelaborable_Initialization (Cursor);
@@ -98,8 +100,9 @@ package Ada.Containers.Formal_Hashed_Maps is
    --  ???
    --  capacity=0 means use container.length as cap of tgt
    --  modulos=0 means use default_modulous(container.length)
-   function Copy (Source   : Map;
-                  Capacity : Count_Type := 0) return Map;
+   function Copy
+     (Source   : Map;
+      Capacity : Count_Type := 0) return Map;
 
    function Key (Container : Map; Position : Cursor) return Key_Type;
 
@@ -114,13 +117,13 @@ package Ada.Containers.Formal_Hashed_Maps is
      (Container : in out Map;
       Position  : Cursor;
       Process   : not null access
-        procedure (Key : Key_Type; Element : Element_Type));
+                    procedure (Key : Key_Type; Element : Element_Type));
 
    procedure Update_Element
      (Container : in out Map;
       Position  : Cursor;
       Process   : not null access
-        procedure (Key : Key_Type; Element : in out Element_Type));
+                    procedure (Key : Key_Type; Element : in out Element_Type));
 
    procedure Move (Target : in out Map; Source : in out Map);
 
@@ -190,8 +193,8 @@ package Ada.Containers.Formal_Hashed_Maps is
 
    procedure Iterate
      (Container : Map;
-      Process   :
-        not null access procedure (Container : Map; Position : Cursor));
+      Process   : not null access
+                    procedure (Container : Map; Position : Cursor));
 
    function Default_Modulus (Capacity : Count_Type) return Hash_Type;
 
@@ -259,10 +262,9 @@ private
    type Map_Access is access all Map;
    for Map_Access'Storage_Size use 0;
 
-   type Cursor is
-      record
-         Node      : Count_Type;
-      end record;
+   type Cursor is record
+      Node : Count_Type;
+   end record;
 
    procedure Read
      (Stream : not null access Root_Stream_Type'Class;

gcc/ada/a-cfhase.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2010, Free Software Foundation, Inc.              --
+--          Copyright (C) 2004-2010, 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,19 +29,21 @@
 -- <http://www.gnu.org/licenses/>.                                          --
 ------------------------------------------------------------------------------
 
---  The specification of this package is derived from the specification
---  of package Ada.Containers.Bounded_Hashed_Sets in the Ada 2012 RM.
---  The changes are
+--  This spec is derived from package Ada.Containers.Bounded_Hashed_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: Element, Next, Query_Element, Has_Element,
---    Key, Iterate, Equivalent_Elements. 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,
+--    content of a container: Element, Next, Query_Element, Has_Element, Key,
+--    Iterate, Equivalent_Elements. 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.
 
---    There are two new functions
+--    There are two new functions:
 
 --      function Left  (Container : Set; Position : Cursor) return Set;
 --      function Right (Container : Set; Position : Cursor) return Set;
@@ -230,7 +232,7 @@ package Ada.Containers.Formal_Hashed_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;
 
@@ -251,9 +253,8 @@ private
          Has_Element : Boolean := False;
       end record;
 
-   package HT_Types is
-     new Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types
-     (Node_Type);
+   package HT_Types is new
+     Ada.Containers.Hash_Tables.Generic_Bounded_Hash_Table_Types (Node_Type);
 
    type HT_Access is access all HT_Types.Hash_Table_Type;
 
@@ -272,10 +273,9 @@ private
    use HT_Types;
    use Ada.Streams;
 
-   type Cursor is
-      record
-         Node      : Count_Type;
-      end record;
+   type Cursor is record
+      Node : Count_Type;
+   end record;
 
    procedure Write
      (Stream : not null access Root_Stream_Type'Class;

gcc/ada/a-cforma.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2010, Free Software Foundation, Inc.              --
+--          Copyright (C) 2004-2010, 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,20 +29,22 @@
 -- <http://www.gnu.org/licenses/>.                                          --
 ------------------------------------------------------------------------------
 
---  The specification of this package is derived from the specification
---  of package Ada.Containers.Bounded_Ordered_Maps in the Ada 2012 RM.
---  The changes are
+--  This spec is derived from package Ada.Containers.Bounded_Ordered_Maps 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.
+--    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 two new functions
+--    There are two new functions:
 
 --      function Left  (Container : Map; Position : Cursor) return Map;
 --      function Right (Container : Map; Position : Cursor) return Map;
@@ -56,7 +58,7 @@
 
 private with Ada.Containers.Red_Black_Trees;
 private with Ada.Streams;
-with Ada.Containers; use Ada.Containers;
+with Ada.Containers;
 
 generic
    type Key_Type is private;
@@ -105,13 +107,13 @@ package Ada.Containers.Formal_Ordered_Maps is
      (Container : in out Map;
       Position  : Cursor;
       Process   : not null access
-        procedure (Key : Key_Type; Element : Element_Type));
+                    procedure (Key : Key_Type; Element : Element_Type));
 
    procedure Update_Element
      (Container : in out Map;
       Position  : Cursor;
       Process   : not null access
-        procedure (Key : Key_Type; Element : in out Element_Type));
+                    procedure (Key : Key_Type; Element : in out Element_Type));
 
    procedure Move (Target : in out Map; Source : in out Map);
 
@@ -192,8 +194,8 @@ package Ada.Containers.Formal_Ordered_Maps is
 
    procedure Reverse_Iterate
      (Container : Map;
-      Process   :
-        not null access procedure (Container : Map; Position : Cursor));
+      Process   : not null access
+                    procedure (Container : Map; Position : Cursor));
 
    function Strict_Equal (Left, Right : Map) return Boolean;
 
@@ -243,7 +245,7 @@ private
    for Map_Access'Storage_Size use 0;
 
    type Cursor is record
-      Node      : Node_Access;
+      Node : Node_Access;
    end record;
 
    procedure Write

gcc/ada/a-cforse.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2010, Free Software Foundation, Inc.              --
+--          Copyright (C) 2004-2010, 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,20 +29,22 @@
 -- <http://www.gnu.org/licenses/>.                                          --
 ------------------------------------------------------------------------------
 
---  The specification of this package is derived from the specification
---  of package Ada.Containers.Bounded_Ordered_Sets in the Ada 2012 RM.
---  The changes are
+--  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.
+--    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 two new functions
+--    There are two new functions:
 
 --      function Left  (Container : Set; Position : Cursor) return Set;
 --      function Right (Container : Set; Position : Cursor) return Set;
@@ -58,7 +60,6 @@ private with Ada.Containers.Red_Black_Trees;
 private with Ada.Streams;
 
 with Ada.Containers;
-use Ada.Containers;
 
 generic
    type Element_Type is private;
@@ -206,8 +207,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;
@@ -245,7 +246,7 @@ 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;
 
@@ -291,7 +292,7 @@ private
    for Set_Access'Storage_Size use 0;
 
    type Cursor is record
-      Node      : Count_Type;
+      Node : Count_Type;
    end record;
 
    procedure Write
@@ -320,7 +321,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;

gcc/ada/a-cofove.ads

@@ -6,7 +6,7 @@
 --                                                                          --
 --                                 S p e c                                  --
 --                                                                          --
---          Copyright (C) 2010, Free Software Foundation, Inc.              --
+--          Copyright (C) 2004-2010, 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,19 +29,21 @@
 -- <http://www.gnu.org/licenses/>.                                          --
 ------------------------------------------------------------------------------
 
---  The specification of this package is derived from the specification
---  of package Ada.Containers.Bounded_Ordered_Maps in the Ada 2012 RM.
---  The changes are
+--  This spec is derived from package Ada.Containers.Bounded_Vectors 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: 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.
+--    content of a container: Element, Next, Query_Element, Previous, Iterate,
+--    Has_Element, 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.
 
---    There are two new functions
+--    There are two new functions:
 
 --      function Left  (Container : Vector; Position : Cursor) return Vector;
 --      function Right (Container : Vector; Position : Cursor) return Vector;
@@ -323,13 +325,13 @@ package Ada.Containers.Formal_Vectors is
 
    procedure Iterate
      (Container : Vector;
-      Process   :
-        not null access procedure (Container : Vector; Position : Cursor));
+      Process   : not null access
+                    procedure (Container : Vector; Position : Cursor));
 
    procedure Reverse_Iterate
      (Container : Vector;
-      Process   :
-        not null access procedure (Container : Vector; Position : Cursor));
+      Process   : not null access
+                    procedure (Container : Vector; Position : Cursor));
 
    generic
       with function "<" (Left, Right : Element_Type) return Boolean is <>;
@@ -397,8 +399,8 @@ private
    for Vector'Read use Read;
 
    type Cursor is record
-      Valid     : Boolean := True;
-      Index     : Index_Type := Index_Type'First;
+      Valid : Boolean := True;
+      Index : Index_Type := Index_Type'First;
    end record;
 
    procedure Write