indexing
description: "This class provides a mapping between Java and Eiffel objects"
class interface
JAVA_OBJECT_TABLE
create
make
feature
item (jobject: POINTER): JAVA_OBJECT
require
jobject_not_void: jobject /= default_pointer
put (object: JAVA_OBJECT)
require
jobject_not_void: (object /= void) and then (object.java_object_id /= default_pointer)
ensure
inserted: table.has (object.java_object_id.hash_code)
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- JAVA_OBJECT_TABLE