Основы объектно-ориентированного программирования полностью

Функция абстракции а обычно представима частичной функцией: не для каждого возможного конкретного объекта существует правильное представление абстрактного объекта. Например, не каждая пара является правильным представлением абстрактного стека. Если representation является массивом емкости 3 и count = 4, то они совместно не представляют абстрактный стек. Правильные представления (члены, входящие в область определения функции абстракции), - только те пары, для которых count находится между 0 и размерностью массива. Это свойство является инвариантом реализации.

В математических терминах, инвариант реализации является характеристической функцией области определения абстрактной функции. Другими словами, это булево свойство, определяющее применимость функции. (Характеристическая функция подмножества А задает булево свойство, истинное на А и ложное всюду вне его.)

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

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

Можно рассматривать и другие возможности использования утверждений. Хотя они менее специфичны для нашего метода, но тоже играют важную роль, и должны быть частью нашей нотации. Наши расширения будут включать инструкцию проверки 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