Бертран Мейер - Основы объектно-ориентированного программирования

x := a^2 + b^2

... Другие инструкции ...

check

x >= 0

-- Поскольку x был вычислен как сумма квадратов.

end

y := sqrt (x)

Здесь нет конструкции if... then..., защищающей вызов sqrt ; но checkпоказывает, что вызов корректен. Хорошей практикой является сопровождать инструкцию комментарием с обоснованием утверждения, как это сделано в примере. Отступы при записи инструкции это тоже часть рекомендованного стиля; они подчеркивают, что при нормальных обстоятельствах инструкция проверки никак не влияет на ход алгоритмического процесса вычислений.

Этот пример типичен для демонстрации того, что наиболее вероятное применение инструкции проверки состоит в добавлении ее, как раз перед вызовом программы, имеющей предусловие. В качестве еще одного примера рассмотрим вызов

s.remove

в точке, где вы точно знаете, что стек s не пуст, поскольку до этого в стек засылалось n элементов, а удалялось m , и вам известно, что n>m . В этом случае нет необходимости защищать вызов: if (not s.empty) then ...; но, если причина корректности вызова непосредственно следует из контекста, то есть смысл напомнить читателю, что "беззащитный" вызов является осознанным решением, а не недосмотром. Этого можно достичь, добавляя проверку:

check not s.empty end

Вариант такой ситуации встречается, когда пишется вызов в форме x.f в полной уверенности, что x/=Void , так что нет необходимости заключать этот вызов в оператор if (x/=Void) then ..., но, тем не менее, существование x не очевидно из контекста. Вернемся к рассмотрению процедур put и remove нашего "защищенного" класса STACK3 . Вот текст тела процедуры put :

if full then

error := Overflow

else

check representation /= Void end

representation.put (x); error := 0

end

Здесь читатель может думать, что вызов в else ветви: representation.put(x) потенциально не безопасен, поскольку ему не предшествует тест: (representation /=Void) . Но, исследуя текст класса, можно понять, что из условия (full = false) следует положительность capacity , откуда, в свою очередь, следует, что representation не может быть Void . Это важное и не совсем тривиальное свойство, которое должно быть частью инварианта реализации класса. Фактически, с полностью установленным инвариантом реализации следует переписать инструкцию проверки следующим образом:

check

representation_exists: representation /= Void

-- Поскольку предложение representation_exists истинно, когда

-- full ложно, что следует из инварианта реализации.

end

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

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