indexing description: "Values that may be hashed into an integer index, for use as keys in hash tables" deferred class interface HASHABLE feature -- Access hash_code: INTEGER -- Hash code value ensure good_hash_value: Result >= 0 feature -- Status report is_hashable: BOOLEAN -- May current object be hashed? -- (True if it is not its type's default.) ensure ok_if_not_default: Result implies (Current /= default) invariant -- from GENERAL reflexive_equality: standard_is_equal (Current); reflexive_conformance: conforms_to (Current); end -- class HASHABLE