Как продлить обязательные условия функции в Eiffel?

Question

У меня есть класс, который переопределяет функцию копирования из ANY, Я хотел бы добавить новое требование, но я получаю эту ошибку:

Assertion in redeclaration uses just 'require' or 'ensure'. invalid precondition feature 'copy'

Код:

copy ( other : like Current )
require
    size_is_enough: Current.max_size >= other.count
do
    -- ...
end

Объяснение:

Этот класс содержит массив, и я хотел бы проверить перед копированием, имеет ли объект достаточно места для них

Answer 1

Предварительные условия в переобъявлении объектов могут быть ослаблены в Eiffel с помощью использования require else вместо require (для постусловий это будет гарантировано, а не гарантировано). Новая эффективная предпосылка будет сочетать оригинальную и новую. Например, если есть функция

foo
    require
        A

который объявлен как

foo
    require else
        B

тогда эффективным предварительным условием будет A or else B, Другими словами, предварительное условие переопределения всегда слабее, чем первоначальная особенность.

То же самое относится к предварительному условию функции copy: оно может стать только слабее. Это означает, что вы не можете проверить, что размер массива текущего объекта больше, чем другого. Предварительное условие переопределения будет проверяться только в том случае, если исходное предварительное условие не выполнено, т. Е. Когда тип другого объекта отличается от типа текущего объекта. Другими словами, вы пытаетесь усилить предварительное условие, а это невозможно.

Одним из вариантов является использование другой функции вместо copyдругим является изменение размера хранилища текущего объекта, если это необходимо. В обоих случаях предварительным условием функции copy остается неизменной.