Некоторые ограничения могут навязываться реализацией. Например, в программе
| Обычно следует избегать структур ограниченной емкости; даже в случае массивов можно строить стек на динамических массивах, изменяющих размерность при необходимости. В Базовой библиотеке представлен общий класс, описывающий стеки11.1), отличающийся от класса |
Предусловия и статус экспорта
Возможно, вы заметили необходимость дополнительного требования, не отраженного в принципе обоснованности предусловия. Для того чтобы клиент мог проверить предусловие, оно не должно использовать закрытые свойства класса, недоступность которых отражена в статусе экспорта.
Рассмотрим следующую ситуацию:
-- Предупреждение: это неправильный класс, только в целях иллюстрации.
class SNEAKY feature
tricky is
require
accredited
do
...
end
feature {NONE}
accredited: BOOLEAN is do ... end
end
Спецификация для
Причина, по которой принцип Обоснованности предусловия не покрывает подобные ситуации, в том, что это методологический принцип, а мы нуждаемся в правиле языка, заставляющем компилятор контролировать решение проблемы, не полагаясь на разработчиков.
Это правило учитывает все возможные ситуации экспорта, а не только случаи доступности всем клиентам (
Правило Доступности предусловия
Каждый компонент, появляющийся в предусловии программы, должен быть доступен каждому клиенту, которому доступна сама программа.
В соответствии с этим правилом каждый клиент, способный вызвать программу, способен проверить ее предусловие. По этому правилу класс
Подобного правила нет для постусловий. Не является ошибкой в постусловии ссылаться на компоненты, закрытые или экспортируемые избранным клиентам. Просто это означает, что описание эффекта выполнения программы содержит некоторые свойства, непосредственно не используемые клиентом. Подобная ситуация имеет место в процедуре
put (x: G) is
-- Добавить элемент x на вершину
require
not full
do
...
ensure
... Другие предложения...
in_top_array_entry: representation @ count = x
end