Eiffel: как использовать старое ключевое слово в условии контракта с отделенным

Question

Как использовать ключевое слово old в предложении ensure функции, текущая инструкция кажется недействительной во время выполнения

relationships: CHAIN -- any chain

some_feature
    do
    (...)
    ensure
        relationship_added: attached relationships as l_rel implies
            attached old relationships as l_old_rel and then
            l_rel.count = l_old_rel.count
    end

Для всего случая, следующие скриншоты демонстрируют случай

начало рутинного исполнения конец рутинного исполнения

Answer 1

Необходимо рассмотреть 2 случая: когда исходная ссылка равна void, а когда - нет:

attached relationships as r implies r.count =
    old (if attached relationships as o then o.count + 1 else 1 end)

Интуиция за утверждением следующая:

1. Если relationships равно Void на выходе, нас не волнует count.
2. Если relationships присоединен при выходе, он имеет еще один элемент по сравнению со старым значением. Может быть добавлено старое значение или Void:
   • если прикреплено старое значение, новым номером будет старое число плюс 1;
   • если старое значение Void, новое число элементов 1.