compare - 埃菲尔 is_equal() 函数

Question

我试图更好地理解在类COMPARABLE中定义的函数is_equal()。

我想知道在哪种情况下，对于对象o函数调用o.is_equal(o)给出false。

我知道这个函数与=不同，它不仅比较对象的地址，还比较对象所有属性的值。

按照这个定义，我很确定这样的调用总是会给出true，因为我们正在比较同一个对象。

如果有人能解释我的想法有什么问题，我将不胜感激。

Answer 1

目前，特征的起源is_equal是类ANY，而不是COMPARABLE。类COMPARABLE重新定义了该特性并添加了一个后置条件，该后置trichotomy条件根据不等式（或者is_less更精确的查询）指定等式的属性。因此，要了解发生了什么，让我们看看起源。

类ANY有一个不变量

reflexive_equality: standard_is_equal (Current)

同时特征is_equal有一个后置条件

consistent: standard_is_equal (other) implies Result

将两者结合起来（即使不知道是什么standard_is_equal）我们可以推导出一个新的不变量

new_reflexive_equality: is_equal (Current)

这应该对每个对象都有效。因此，只要o在表达式中始终产生相同的对象（例如，如果它是一个变量，而不是在每次调用时返回不同对象的函数），就o.is_equal (o) 应该始终产生True. 当然，可以尝试重新定义is_equalreturn False，但这会破坏该功能的合同。

在现实生活中，比较通常o1.is_equal (o2)可以是True或False取决于 和 的o1值o2。