Почему текущее и старое значение одного и того же выражения в постусловии равны?

Я пытаюсь получить значение записи в 2D-массиве до реализации и после нее. Но следующее постусловие не работает, потому что две записи в чем-то одинаковы (и да, я переопределил is_equal, так что ~ будет равноправием объектов):

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

Почему я получаю нарушение постусловия designated_cell_changed?


person NoName    schedule 22.09.2018    source источник


Ответы (1)


Причин может быть несколько:

  1. Подозрительно, почему индексы row + 1 и column + 1 вместо row и column.

  2. Если рассматриваемая функция явно принимает новое значение, например. put (value: G; row, column: ...), у него должно быть предварительное условие

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

    Примечание. в запросах рекомендуется использовать существительные или прилагательные, а не глаголы, поэтому entry вместо get_entry.

  3. Если функция не принимает новое значение в качестве аргумента, она должна сама обновить соответствующее значение.

  4. В коде функции могут быть ошибки:

    • It does not change the value all the time (e.g., in some conditional branches).
    • Он меняет значение, но по некоторым другим показателям.
  5. Если значения entry (row + 1, column + 1) в начале и в конце признака различаются, реализация is_equal может пропустить некоторые случаи, которые делают объекты разными.

person Alexander Kogtenkov    schedule 23.09.2018
comment
Спасибо, это нарушает, когда новое значение, которое будет присвоено ячейке, ТАКОЕ ЖЕ, что и старое значение. - person NoName; 25.09.2018