indexing
description: "Objects identified, uniquely during any session, by an integer"
class interface
IDENTIFIED
feature -- Access
frozen id_object (an_id: INTEGER): IDENTIFIED
-- Object associated with an_id (void if no such object)
ensure
consistent: Result = void or else Result.object_id = an_id
frozen object_id: INTEGER
-- Unique for current object in any given session
ensure
valid_id: id_object (Result) = Current
feature -- Comparison
is_equal (other: like Current): BOOLEAN
-- Is other attached to an object considered
-- equal to current object?
require -- from GENERAL
other_not_void: other /= void
ensure -- from GENERAL
symmetric: Result implies other.is_equal (Current);
consistent: standard_is_equal (other) implies Result
feature -- Status report
frozen id_freed: BOOLEAN
-- Has Current been removed from the table?
feature -- Removal
frozen free_id
-- Free the entry associated with object_id if any
ensure
object_freed: id_freed
feature -- Duplication
copy (other: like Current)
-- Update current object using fields of object attached
-- to other, so as to yield equal objects.
require -- from GENERAL
other_not_void: other /= void;
type_identity: same_type (other)
ensure -- from GENERAL
is_equal: is_equal (other)
invariant
-- from GENERAL
reflexive_equality: standard_is_equal (Current);
reflexive_conformance: conforms_to (Current);
end -- class IDENTIFIED