note description: "A sample hashable object." class EB2_KEY inherit V_HASHABLE redefine is_model_equal end create set_value feature -- Access value: INTEGER -- State. hash_code: INTEGER -- Hash code. do Result := value.abs end feature -- Modification set_value (v: INTEGER) -- Set `value' to `v'. do value := v ensure value = v end feature -- Specification hash_code_: INTEGER -- Hash code in terms of abstract state. note status: functional, ghost do Result := value.abs end is_model_equal (other: like Current): BOOLEAN -- Is the abstract state of `Current' equal to that of `other'? note status: ghost explicit: contracts do Result := value.abs = other.value.abs ensure then definition: Result = (value.abs = other.value.abs) end lemma_transitive (x: like Current; ys: MML_SET [like Current]) -- Property that follows from transitivity of `is_model_equal'. note status: lemma do end end