A.18.18 The Generic Package Containers.Indefinite_Holders
The language-defined generic package Containers.Indefinite_Holders
provides a private type Holder and a set of operations for that type.
A holder container holds a single element of an indefinite type.
A holder container allows the declaration of an object
that can be used like an uninitialized variable or component of an indefinite
type.
A holder container may be
empty. An empty
holder does not contain an element.
Static Semantics
The generic library
package Containers.Indefinite_Holders has the following declaration:
generic
type Element_Type (<>)
is private;
with function "=" (Left, Right : Element_Type)
return Boolean
is <>;
package Ada.Containers.Indefinite_Holders
with Preelaborate, Remote_Types,
Nonblocking, Global =>
in out synchronized is
type Holder
is tagged private
with Stable_Properties => (Is_Empty,
Tampering_With_The_Element_Prohibited),
Default_Initial_Condition => Is_Empty (Holder),
Preelaborable_Initialization;
Empty_Holder :
constant Holder;
function Equal_Element (Left, Right : Element_Type)
return Boolean
renames "=";
function "=" (Left, Right : Holder) return Boolean;
function Tampering_With_The_Element_Prohibited
(Container : Holder)
return Boolean
with Nonblocking, Global =>
null, Use_Formal =>
null;
function Empty
return Holder
is (Empty_Holder)
with Post =>
not Tampering_With_The_Element_Prohibited (Empty'Result)
and then Is_Empty (Empty'Result);
function To_Holder (New_Item : Element_Type)
return Holder
with Post =>
not Is_Empty (To_Holder'Result);
function Is_Empty (Container : Holder)
return Boolean
with Global =>
null, Use_Formal =>
null;
procedure Clear (Container :
in out Holder)
with Pre =>
not Tampering_With_The_Element_Prohibited (Container)
or else raise Program_Error,
Post => Is_Empty (Container);
function Element (Container : Holder)
return Element_Type
with Pre =>
not Is_Empty (Container)
or else raise Constraint_Error,
Global =>
null, Use_Formal => Element_Type;
procedure Replace_Element (Container :
in out Holder;
New_Item :
in Element_Type)
with Pre =>
not Tampering_With_The_Element_Prohibited (Container)
or else raise Program_Error,
Post =>
not Is_Empty (Container);
procedure Query_Element
(Container :
in Holder;
Process :
not null access procedure (Element :
in Element_Type))
with Pre =>
not Is_Empty (Container)
or else raise Constraint_Error;
procedure Update_Element
(Container :
in out Holder;
Process :
not null access procedure (Element :
in out Element_Type))
with Pre =>
not Is_Empty (Container)
or else raise Constraint_Error;
type Constant_Reference_Type
(Element :
not null access constant Element_Type)
is private
with Implicit_Dereference => Element,
Nonblocking, Global =>
in out synchronized,
Default_Initial_Condition => (
raise Program_Error);
type Reference_Type
(Element :
not null access Element_Type)
is private
with Implicit_Dereference => Element,
Nonblocking, Global =>
in out synchronized,
Default_Initial_Condition => (
raise Program_Error);
function Constant_Reference (Container :
aliased in Holder)
return Constant_Reference_Type
with Pre =>
not Is_Empty (Container)
or else raise Constraint_Error,
Post => Tampering_With_The_Element_Prohibited (Container),
Nonblocking, Global =>
null, Use_Formal =>
null;
function Reference (Container :
aliased in out Holder)
return Reference_Type
with Pre =>
not Is_Empty (Container)
or else raise Constraint_Error,
Post => Tampering_With_The_Element_Prohibited (Container),
Nonblocking, Global =>
null, Use_Formal =>
null;
procedure Assign (Target :
in out Holder; Source :
in Holder)
with Post => (Is_Empty (Source) = Is_Empty (Target));
function Copy (Source : Holder)
return Holder
with Post => (Is_Empty (Source) = Is_Empty (Copy'Result));
procedure Move (Target :
in out Holder; Source :
in out Holder)
with Pre => (
not Tampering_With_The_Element_Prohibited (Target)
or else raise Program_Error)
and then
(
not Tampering_With_The_Element_Prohibited (Source)
or else raise Program_Error),
Post => (
if not Target'Has_Same_Storage (Source)
then
Is_Empty (Source)
and then (
not Is_Empty (Target)));
procedure Swap (Left, Right :
in out Holder)
with Pre => (
not Tampering_With_The_Element_Prohibited (Left)
or else raise Program_Error)
and then
(
not Tampering_With_The_Element_Prohibited (Right)
or else raise Program_Error),
Post => Is_Empty (Left) = Is_Empty (Right)'Old
and then
Is_Empty (Right) = Is_Empty (Left)'Old;
private
... -- not specified by the language
end Ada.Containers.Indefinite_Holders;
The actual function for the generic formal function
"=" on Element_Type values is expected to define a reflexive
and symmetric relationship and return the same result value each time
it is called with a particular pair of values. If it behaves in some
other manner, the function "=" on holder values returns an
unspecified value. The exact arguments and number of calls of this generic
formal function by the function "=" on holder values are unspecified.
The type Holder is used to represent holder containers.
The type Holder needs finalization
(see
7.6).
Empty_Holder represents an empty holder object. If
an object of type Holder is not otherwise initialized, it is initialized
to the same value as Empty_Holder.
Some operations check for “tampering with
the element” of a container because they depend
on
the element of the container not being replaced.When tampering with the
element is
prohibited for
a particular holder object
H, Program_Error is propagated by the
finalization of
H, as well as by a call that passes
H to
certain of the operations of this package, as indicated by the precondition
of such an operation.
Paragraphs 30 through
35 are removed as preconditions now describe these rules.
function "=" (Left, Right : Holder) return Boolean;
If Left and Right
denote the same holder object, then the function returns True. Otherwise,
it compares the element contained in Left to the element contained in
Right using the generic formal equality operator, returning the result
of that operation. Any exception raised during the evaluation of element
equality is propagated.
function Tampering_With_The_Element_Prohibited
(Container : Holder) return Boolean
with Nonblocking, Global => null, Use_Formal => null;
Returns True if
tampering with the element is currently prohibited for Container, and
returns False otherwise.
function To_Holder (New_Item : Element_Type) return Holder
with Post => not Is_Empty (To_Holder'Result);
Returns a nonempty
holder containing an element initialized to New_Item. To_Holder performs
indefinite insertion (see
A.18).
function Is_Empty (Container : Holder) return Boolean
with Global => null, Use_Formal => null;
Returns True if
Container is empty, and False if it contains an element.
procedure Clear (Container : in out Holder)
with Pre => not Tampering_With_The_Element_Prohibited (Container)
or else raise Program_Error,
Post => Is_Empty (Container);
Removes the element
from Container.
function Element (Container : Holder) return Element_Type
with Pre => not Is_Empty (Container) or else raise Constraint_Error,
Global => null, Use_Formal => Element_Type;
Returns the element
stored in Container.
procedure Replace_Element (Container : in out Holder;
New_Item : in Element_Type)
with Pre => not Tampering_With_The_Element_Prohibited (Container)
or else raise Program_Error,
Post => not Is_Empty (Container);
Replace_Element
assigns the value New_Item into Container, replacing any preexisting
content of Container; Replace_Element performs indefinite insertion (see
A.18).
procedure Query_Element
(Container : in Holder;
Process : not null access procedure (Element : in Element_Type))
with Pre => not Is_Empty (Container) or else raise Constraint_Error,
Global => null, Use_Formal => null;
Query_Element calls
Process.all with the contained element as the argument. Tampering
with the element of Container is prohibited during the execution of the
call on Process.all. Any exception raised by Process.all
is propagated.
procedure Update_Element
(Container : in out Holder;
Process : not null access procedure (Element : in out Element_Type))
with Pre => not Is_Empty (Container) or else raise Constraint_Error;
Update_Element calls
Process.all with the contained element as the argument. Tampering
with the element of Container is prohibited during the execution of the
call on Process.all. Any exception raised by Process.all
is propagated.
type Constant_Reference_Type
(Element : not null access constant Element_Type) is private
with Implicit_Dereference => Element,
Nonblocking, Global => in out synchronized,
Default_Initial_Condition => (raise Program_Error);
type Reference_Type (Element : not null access Element_Type) is private
with Implicit_Dereference => Element,
Nonblocking, Global => in out synchronized,
Default_Initial_Condition => (raise Program_Error);
The types Constant_Reference_Type
and Reference_Type need finalization.
This paragraph
was deleted.
function Constant_Reference (Container : aliased in Holder)
return Constant_Reference_Type
with Pre => not Is_Empty (Container) or else raise Constraint_Error,
Post => Tampering_With_The_Element_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
This function (combined
with the Implicit_Dereference aspect) provides a convenient way to gain
read access to the contained element of a holder container.
Constant_Reference returns an object whose discriminant
is an access value that designates the contained element. Tampering with
the element of Container is prohibited while the object returned by Constant_Reference
exists and has not been finalized.
function Reference (Container : aliased in out Holder)
return Reference_Type
with Pre => not Is_Empty (Container) or else raise Constraint_Error,
Post => Tampering_With_The_Element_Prohibited (Container),
Nonblocking, Global => null, Use_Formal => null;
This function (combined
with the Implicit_Dereference aspects) provides a convenient way to gain
read and write access to the contained element of a holder container.
Reference returns an object whose discriminant
is an access value that designates the contained element. Tampering with
the element of Container is prohibited while the object returned by Reference
exists and has not been finalized.
procedure Assign (Target : in out Holder; Source : in Holder)
with Post => (Is_Empty (Source) = Is_Empty (Target));
If Target denotes
the same object as Source, the operation has no effect. If Source is
empty, Clear (Target) is called. Otherwise, Replace_Element (Target,
Element (Source)) is called.
function Copy (Source : Holder) return Holder
with Post => (Is_Empty (Source) = Is_Empty (Copy'Result));
If Source is empty,
returns an empty holder container; otherwise, returns To_Holder (Element
(Source)).
procedure Move (Target : in out Holder; Source : in out Holder)
with Pre => (not Tampering_With_The_Element_Prohibited (Target)
or else raise Program_Error) and then
(not Tampering_With_The_Element_Prohibited (Source)
or else raise Program_Error),
Post => (if not Target'Has_Same_Storage (Source) then
Is_Empty (Source) and then (not Is_Empty (Target)));
If Target denotes
the same object as Source, then the operation has no effect. Otherwise,
the element contained by Source (if any) is removed from Source and inserted
into Target, replacing any preexisting content.
procedure Swap (Left, Right : in out Holder)
with Pre => (not Tampering_With_The_Element_Prohibited (Left)
or else raise Program_Error) and then
(not Tampering_With_The_Element_Prohibited (Right)
or else raise Program_Error),
Post => Is_Empty (Left) = Is_Empty (Right)'Old and then
Is_Empty (Right) = Is_Empty (Left)'Old;
If Left denotes
the same object as Right, then the operation has no effect. Otherwise,
operation exchanges the elements (if any) contained by Left and Right.
Bounded (Run-Time) Errors
It is a bounded error for the
actual function associated with a generic formal subprogram, when called
as part of an operation of this package, to tamper with the element of
any Holder parameter of the operation. Either Program_Error is raised,
or the operation works as defined on the value of the Holder either prior
to, or subsequent to, some or all of the modifications to the Holder.
It is a bounded error to call
any subprogram declared in the visible part of Containers.Indefinite_Holders
when the associated container has been finalized. If the operation takes
Container as an
in out parameter, then it raises Constraint_Error
or Program_Error. Otherwise, the operation either proceeds as it would
for an empty container, or it raises Constraint_Error or
Program_Error.
Erroneous Execution
Execution is erroneous if the holder container associated
with the result of a call to Reference or Constant_Reference is finalized
before the result object returned by the call to Reference or Constant_Reference
is finalized.
Implementation Requirements
No storage associated with a holder object shall
be lost upon assignment or scope exit.
The execution of an
assignment_statement
for a holder container shall have the effect of copying the element (if
any) from the source holder object to the target holder object.
Implementation Advice
Move and Swap should not copy any elements, and should
minimize copying of internal data structures.
If an exception is propagated from a holder operation,
no storage should be lost, nor should the element be removed from a holder
container unless specified by the operation.
Ada 2005 and 2012 Editions sponsored in part by Ada-Europe
