indexing
status: "See notice at end of class"
date: "$Date$"
revision: "$Revision$"
product: eiffelstore
database: all_bases
class interface
HANDLE
feature
all_types: DB_ALL_TYPES
ensure
result_not_void: Result /= void
database: DB [DATABASE]
execution_type: DB_EXEC
login: LOGIN [DATABASE]
process: POINTER_REF
status: DB_STATUS
invariant
ANY
reflexive_equality: standard_is_equal (Current)
reflexive_conformance: conforms_to (Current)
end -- HANDLE