+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,
-- --
-- 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 --
-- <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;
-- 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;
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;
-- --
-- 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 --
-- <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;
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);
-- ???
-- 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;
(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);
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;
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;
-- --
-- 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 --
-- <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;
(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;
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;
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;
-- --
-- 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 --
-- <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;
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;
(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);
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;
for Map_Access'Storage_Size use 0;
type Cursor is record
- Node : Node_Access;
+ Node : Node_Access;
end record;
procedure Write
-- --
-- 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 --
-- <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;
private with Ada.Streams;
with Ada.Containers;
-use Ada.Containers;
generic
type Element_Type is private;
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;
(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;
for Set_Access'Storage_Size use 0;
type Cursor is record
- Node : Count_Type;
+ Node : Count_Type;
end record;
procedure Write
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;
-- --
-- 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 --
-- <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;
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 <>;
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
projects / gcc.git / commitdiff