eiffel - 为什么后置条件中相同表达式的当前值和“旧”值相等？

Question

我试图在实现之前和之后获取二维数组中条目的值。但是下面的后置条件失败了，因为这两个条目在某种程度上是相同的（是的，我已经重新定义了 is_equal，所以~将是对象相等）：

    ensure
        designated_cell_changed:
            get_entry (row + 1, column + 1) /~ old get_entry (row + 1, column + 1)

为什么我会违反后置条件designated_cell_changed？

标签： eiffel

Answer 1

可能有几个原因：

1. 令人怀疑为什么索引是row + 1andcolumn + 1而不是rowand column。

2. 如果所讨论的特征明确地采用新值，例如put (value: G; row, column: ...)，它应该有一个先决条件

   require
       different_value: value /~ entry (row, column)
   

   旁注：对于查询，建议使用名词或形容词，而不是动词，因此entry而不是get_entry.

3. 如果特征不接受新值作为参数，它应该更新相应的值本身。

4. 该功能的代码可能存在错误：

   • 它不会一直更改值（例如，在某些条件分支中）。
   • 它会更改值，但会更改其他一些索引。

5. 如果特征entry (row + 1, column + 1)的开头和结尾的值不同，则实现is_equal可能会漏掉一些使对象不同的情况。