Пример

Пример

Предположим, я написал класс MATRIX, реализующий операции линейной алгебры. Среди прочих возможностей я предлагаю своим клиентам подпрограмму расчета обратной матрицы. Фактически это сочетание команды и двух запросов: процедура invert инвертирует матрицу, присваивает атрибуту inverse значение обратной и устанавливает логический атрибут inverse_valid. Значение атрибута inverse имеет смысл тогда и только тогда, когда inverse_valid является истинным; в противном случае матрицу инвертировать не удалось, так как она вырождена. В ходе нашего обсуждения случай вырожденной матрицы мы можем проигнорировать.

Конечно же, я могу найти лишь приближенное значение обратной матрицы и готов гарантировать определенную точность расчетов, однако, не владея численными подпрограммами в совершенстве, буду принимать лишь запросы с точностью не выше 10-6. В итоге, моя подпрограмма будет выглядеть приблизительно так:

invert (epsilon: REAL) is

-- Обращение текущей матрицы с точностью epsilon

require

epsilon >= 10 ^ (-6)

do

"Вычисление обратной матрицы"

ensure

((Current * inverse) |-| One) <= epsilon

end

Постусловие предполагает, что класс содержит инфиксную функцию infix "|-|" такую, что m1 |-| m2 есть |m1 - m2| (норма разности матриц m1 и m2), а также функцию infix "*", результатом которой является произведение двух матриц. One - единичная матрица.

Как человек негордый, летом я приглашу программиста, и он перепишет мою подпрограмму invert, используя более удачный алгоритм, лучше аппроксимирующий результат и допускающий меньшее значение epsilon (как повторное объявление, эта запись синтаксически некорректна:

require

epsilon >= 10 ^ (-20)

...

ensure

((Current * inverse) |-| One) <= (epsilon / 2)

Автор новой версии достаточно умен, чтобы не переписывать MATRIX в целом. Изменения коснутся лишь нескольких подпрограмм. Они будут включены в состав порожденного от MATRIX класса NEW_MATRIX.

Если повторное объявление содержит новые утверждения, они должны иметь иной синтаксис, нежели приведенный выше. Правило появится чуть позднее.

Изменения, внесенные в утверждения, удовлетворяют правилу повторного объявления: новое предусловие epsilon >= 10 ^ (-20) слабее исходного epsilon >= 10 ^ (-6), новое же постусловие сильнее сформулированного вначале.

Вот как все должно происходить. Клиент исходного класса MATRIX запрашивает расчет обратной матрицы именно у него, но на деле - ввиду динамического связывания - вызывает реализацию класса NEW_MATRIX. Тот же клиент может иметь в своем составе подпрограмму

some_client_routine (m1: MATRIX; precision: REAL) is

do

... ; m1.invert (precision); ...

-- Возможен вызов версии как MATRIX, так и NEW_MATRIX

end

которой один из его собственных клиентов передает первый параметр типа NEW_MATRIX.

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

При усилении предусловия invert, например, epsilon >= 10 ^ (-5), вызов, корректный для класса MATRIX, мог стать теперь некорректным. При ослаблении постусловия возвращаемый результат стал бы хуже, чем гарантируемый для MATRIX.