indexing
description: "Objects identified, uniquely during any session, by an integer"
status: "See notice at end of class"
date: "$Date$"
revision: "$Revision$"
class interface
IDENTIFIED
feature
frozen id_object (an_id: INTEGER): IDENTIFIED
an_id
ensure
consistent: Result = void or else Result.object_id = an_id
frozen object_id: INTEGER
ensure
valid_id: id_object (Result) = Current
feature
is_equal (other: like Current): BOOLEAN
other
require ANY
other_not_void: other /= void
ensure ANY
symmetric: Result implies other.is_equal (Current)
consistent: standard_is_equal (other) implies Result
feature
frozen id_freed: BOOLEAN
Current
feature
frozen free_id
object_id
ensure
object_freed: id_freed
feature
copy (other: like Current)
other
require ANY
other_not_void: other /= void
type_identity: same_type (other)
ensure ANY
is_equal: is_equal (other)
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
indexing
library: "[
EiffelBase: Library of reusable components for Eiffel.
]"
status: "[
Copyright 1986-2001 Interactive Software Engineering (ISE).
For ISE customers the original versions are an ISE product
covered by the ISE Eiffel license and support agreements.
]"
license: "[
EiffelBase may now be used by anyone as FREE SOFTWARE to
develop any product, public-domain or commercial, without
payment to ISE, under the terms of the ISE Free Eiffel Library
License (IFELL) at http://eiffel.com/products/base/license.html.
]"
source: "[
Interactive Software Engineering Inc.
ISE Building
360 Storke Road, Goleta, CA 93117 USA
Telephone 805-685-1006, Fax 805-685-6869
Electronic mail <info@eiffel.com>
Customer support http://support.eiffel.com
]"
info: "[
For latest info see award-winning pages: http://eiffel.com
]"
end -- IDENTIFIED