Предусловия и статус экспорта

Принцип обоснованности предусловия

Каждое предусловие программы при требовательном стиле проектирования должно удовлетворять следующим требованиям:

1 Предусловие появляется в официальной документации, поставляемой авторам клиентских модулей.

2 Предусловие формулируется только в терминах спецификации, что делает возможным его вычисление.

Первое требование поддерживается понятием краткой формы, изучаемой позднее в этой лекции. Второе требование исключает появление ограничений, определяемых реализацией поставщика программы. Например, для программы, занимающейся выталкиванием элементов из стека, предусловие not empty является требованием, проверяемым в терминах спецификации, и вытекающим из очевидного факта - из пустого стека ничего нельзя вытолкнуть. При вычислении квадратного корня предусловие x>0 отражает известный математический факт, - отрицательные числа не имеют вещественных квадратных корней.

Некоторые ограничения могут навязываться реализацией. Например, в программе put из класса STACK2 присутствие в качестве предусловия require not full связано с реализацией стека на основе массива. Но это не является нарушением принципа, поскольку класс STACK2 в полном соответствии с его спецификацией определяет стеки ограниченной емкости, что отражено, например, в предложении indexing этого класса. АТД, служащий в роли спецификации этого класса, не задает наиболее общий вид стеков, но является понятием стека ограниченной емкости.

Обычно следует избегать структур ограниченной емкости; даже в случае массивов можно строить стек на динамических массивах, изменяющих размерность при необходимости. В Базовой библиотеке представлен общий класс, описывающий стеки[20], отличающийся от класса STACK2 тем, что в нем не используется понятие емкости; стек по умолчанию перестраивается, когда текущей емкости недостаточно для хранения очередного поступающего элемента.

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

Рассмотрим следующую ситуацию:

-- Предупреждение: это неправильный класс, только в целях иллюстрации.

class SNEAKY feature

tricky is

require

accredited

do

...

end

feature NONE

accredited: BOOLEAN is do... end

end

Спецификация для tricky устанавливает, что любой вызов этой процедуры должен удовлетворять условию, выраженному булевой функцией accredited. Но при экспорте класса эта функция для клиентов является закрытой, поэтому у них нет способа проверить выполнимость условия перед вызовом tricky. Очевидно, подобная ситуация неприемлема.

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

Это правило учитывает все возможные ситуации экспорта, а не только случаи доступности всем клиентам (tricky) или полной недоступности (accredited). Как отмечалось, при обсуждении проблемы скрытия информации, компонент класса можно сделать доступным для некоторых клиентов, явно перечислив их в feature предложении, например feature A, B,..., определяющего доступность только для классов A, B,... и их потомков. Сформулируем правило языка:

Дата добавления: 2014-01-07