Как использовать сквозной цикл в постусловии для сравнения старого массива и нового массива по определенным индексам?

У меня есть метод, который сдвигает все элементы в массиве влево на одну позицию. В моем состоянии публикации мне нужно убедиться, что мои элементы сместились влево на один. Я уже сравнил первый элемент старого массива с последним элементом нового массива. Как пройти через старый массив от 2 до count, перебрать новый массив от 1 до count-1 и сравнить их? Это моя реализация на данный момент.

        items_shifted:
                    old array.deep_twin[1] ~ array[array.count]
                        and
                    across 2 |..| (old array.deep_twin.count) as i_twin all
                        across 1 |..| (array.count-1) as i_orig  all
                            i_twin.item ~ i_orig.item
                            end
                        end



    end

Я ожидал, что результат будет верным, но вместо этого я получаю нарушение контракта, указывающее на это условие публикации. Я протестировал метод вручную, распечатав массив до и после метода, и получил ожидаемый результат.


eiffel post-conditions
person Ed Shirinian    schedule 28.09.2019    source источник

Ответы (1)


arrow_upward
1
arrow_downward

В невыполненном постусловии курсоры цикла i_twin и i_orig перебирают последовательности 2 .. array.count и 1 .. array.count - 1 соответственно, т. е. их элементами являются индексы 2, 3, ... и 1, 2, .... Итак, цикл выполняет сравнения 2 ~ 1, 3 ~ 2 и т. д. (во время выполнения он останавливается на первом неравенстве). Однако вы хотели бы сравнивать элементы, а не индексы.

Одно из возможных решений показано ниже:

    items_shifted:
        across array as c all
            c.item =
                if c.target_index < array.upper then
                    (old array.twin) [c.target_index + 1]
                else
                    old array [array.lower]
                end
        end

Цикл проверяет, что все элементы смещены. Если курсор указывает на последний элемент, он сравнивает его со старым первым элементом. В противном случае он проверяет, равен ли текущий элемент старому элементу по следующему индексу.

Косметика:

  1. Постусловие не предполагает, что массив начинается с 1, а вместо этого использует array.lower и array.upper.

  2. Постусловие не создает глубокий двойник исходного массива. Это позволяет сравнивать элементы, используя =, а не ~.

Редактировать: Чтобы избежать потенциальной путаницы, вызванной правилами приоритета, и подчеркнуть, что сравнение выполняется для всех элементов между старым и новым массивом, лучший вариант, предложенный Эриком Безо, выглядит следующим образом:

    items_shifted:
        across array as c all
            c.item =(old array.twin)
                [if c.target_index < array.upper then
                    c.target_index + 1
                else
                    array.lower
                end]
        end
person Alexander Kogtenkov    schedule 28.09.2019
comment
Я думаю, что это должно быть: старый (array.twin) [array.lower] - person Eric Bezault; 29.09.2019
comment
Чтобы избежать этой ошибки, вы могли бы выделить такой код: c.item = (old array.twin) [if c.target_index ‹ array.upper then c.target_index + 1 else array.lower end] - person Eric Bezault; 29.09.2019
comment
Если выражения в квадратных скобках имеют более низкий приоритет, чем старые выражения, код следует изменить, как это предлагается. В противном случае (например, если выражения в квадратных скобках имеют приоритет над квалифицированными вызовами функций) код должен быть в порядке. В любом случае, вариант с одним старым выражением действительно выглядит лучше. - person Alexander Kogtenkov; 29.09.2019
comment
Меня беспокоил не столько приоритет, сколько тот факт, что вы забыли .twin в другой ветке. old array — это тот же объект, что и array, поэтому вы должны использовать old (array.twin). - person Eric Bezault; 30.09.2019
comment
old array [array.lower] интерпретируется как old (array [array.lower]), который получает элемент из исходного массива, а не из обновленного. Добавление здесь вызова twin ничего не меняет, потому что old (array [array.lower]) = old (array.twin [array.lower]). - person Alexander Kogtenkov; 30.09.2019
comment
Ага, понятно. Итак, я проверил стандарт ECMA, и целью выражения в квадратных скобках не может быть старое выражение, если оно не заключено в скобки. Итак, вы правы, old array [array.lower] не может интерпретироваться как (old array) [array.lower] и, как следствие, должно интерпретироваться как old (array [array.lower]). - person Eric Bezault; 30.09.2019
comment
Если бы я сделал c.item ~ if c.target_index < array.upper then (old array.deep_twin) [c.target_index + 1] else (old array.deep_twin) [array.lower], это дало бы тот же результат? - person Ed Shirinian; 01.10.2019
comment
@EdShirinian Да, это даст тот же результат. Однако постусловие с =, а не ~ немного сильнее, так как гарантирует сохранение всех исходных элементов. Условие с ~ говорит только о том, что элементы равны, но не обязательно одинаковые объекты. Эта небольшая разница может быть существенной, когда элементы относятся к ссылочному типу и когда они могут быть изменены. Другими словами, постусловие с = дает меньше свободы для возможной реализации. В частности, с = такая реализация не может помещать в массив двойников исходных объектов. - person Alexander Kogtenkov; 01.10.2019