Инструкция утверждения

Инструкция утверждения

Утверждения, рассматриваемые до сих пор - предусловия, постусловия, инварианты, - это основные составляющие метода. Они устанавливают связь между конструкциями ОО-программных систем и теорией АТД, лежащей в основе метода. Инварианты класса, в частности, не могут быть поняты, и даже обсуждаться вне рамок ОО-подхода.

Можно рассматривать и другие возможности использования утверждений. Хотя они менее специфичны для нашего метода, но тоже играют важную роль, и должны быть частью нашей нотации. Наши расширения будут включать инструкцию проверки check, а также конструкции, задающие корректность цикла (инварианты и варианты цикла), рассматриваемые в следующем разделе.

Инструкция check выражает уверенность автора программы, что некоторое свойство всегда выполняется, когда вычисление достигает точки, в которой находится наша инструкция. Синтаксически, инструкция записывается в следующей форме:

check

assertion_clause1

assertion_clause2

...

assertion_clausen

end

Включив эту инструкцию в программный текст, мы говорим, что всякий раз, когда управление достигает этой инструкции, заданное утверждение (предложения утверждения между check и end) должно выполняться.

Это некоторый способ убеждать самого себя, что некоторые свойства выполняются. Более важно, что это позволяет будущим читателям вашего программного текста понять, на каких гипотезах вы основываетесь. Создание ПО требует многочисленных предположений о свойствах объектов системы. Тривиальный, но типичный пример - вызов sqrt(x) предполагает x>=0. Это предположение может быть очевидным из контекста, например, если вызов является частью условного оператора в форме:

if x >= 0 then y := sqrt (x) end

Но проверка может быть чуть менее очевидной, если, например:

x := a^2 + b^2

Инструкция check дает возможность выразить наше предположение о свойствах объектов:

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 помогает избежать подобных проблем, требуя документирования нетривиальных предположений.