Why current and "old" value of the same expression in a postcondition are equal?

Question

I'm trying to get the value of an entry in a 2D-array before the implementation and afterwards. But the following postcondition is failing because the 2 entries are somehow the same (and yes, I have redefined is_equal, so that ~ will be object equality):

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

Why do I get a postcondition violation designated_cell_changed?

Answer 1

There could be several reasons:

1. It's suspicious why the indexes are row + 1 and column + 1 instead of row and column.

2. If the feature in question takes a new value explicitly, e.g. put (value: G; row, column: ...), it should have a precondition

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

   Side note: for queries it's recommended to use nouns or adjectives, not verbs, thus entry instead of get_entry.

3. If the feature does not take a new value as an argument, it should update the corresponding value itself.

4. There could be mistakes in the code of the feature:

   • It does not change the value all the time (e.g., in some conditional branches).
   • It changes the value but at some other indices.

5. If the values of entry (row + 1, column + 1) at the beginning and at the end of the feature are different, the implementation of is_equal may miss some cases that make the objects different.