Определение и пример

Рассмотрим снова реализацию стека классом STACK2:

class STACK2 [G] creation

make

feature

? make, empty, full, item, put, remove?

capacity: INTEGER

count: INTEGER

feature NONE -- Implementation

representation: ARRAY [G]

end

Атрибуты класса - массив representation и целые capacity, count - задают представление стека. Хотя предусловия и постусловия программ отражают семантику стека, их недостаточно для выражения важных свойств, связывающих атрибуты. Например, count всегда должно удовлетворять условию:

0 <= count; count <= capacity

из которого следует, что capacity >=0 и что capacity задает размер массива:

capacity = representation.capacity

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

Выше приведенные примеры инвариантов включали только атрибуты. Инварианты могут выражать отношения между функциями и между функциями и атрибутами. Например, инвариант STACK2 может включать следующее свойство, описывающее связь между функцией empty и count:

empty = (count = 0)

Этот пример не показателен, он повторяет утверждение, заданное постусловием empty. Более полезные утверждения те, которые включают только атрибуты или более чем одну функцию.

Вот еще один типичный пример. Предположим, что мы имеем дело с банковскими счетами, и есть класс Bank_Account с компонентами: deposits_list, withdrawals_list и balance. Тогда инвариантом такого класса может быть утверждение в форме:

consistent_balance: deposits_list.total - withdrawals_list.total = balance

где функция total дает суммарное значение списка всех операций (приходных или расходных). Инвариант определяет основное условие согласования всех банковских операций над счетом, связывая баланс, приходные и расходные операции.

Форма и свойства инвариантов класса

Синтаксически инвариант класса является утверждением, появляющимся в предложении invariant, стоящим после всех предложений feature, и перед предложением end. Вот пример:

class STACK4 [G] creation

...Как в STACK2...

feature

...Как в STACK2...

invariant

count_non_negative: 0 <= count

count_bounded: count <= capacity

consistent_with_array_size: capacity = representation.capacity

empty_if_no_elements: empty = (count = 0)

item_at_top: (count > 0) implies (representation.item (count) = item)

end

Инвариант класса C это множество утверждений, которым удовлетворяет каждый экземпляр класса во все "стабильные" времена. В эти времена экземпляр класса находится в наблюдаемом состоянии:

[x]. на момент создания экземпляра, сразу после выполнения create a или create a.make(...), где a класса C;

[x]. перед и после каждого удаленного вызова a.r(...) программы r класса С.

Следующий рисунок, показывающий жизнь объектов, поможет разобраться в инвариантах и стабильных временах:

Рис. 11.4. Жизнь объектов

Жизнь объектов не столь уж захватывающая. Вначале - слева на рисунке - он просто не существует. При выполнении инструкции create a или create a.make(...) или clone объект создается и достигает первой станции S1 в своей жизни. Затем идет череда довольно скучных событий: клиенты, для которых доступен объект, один за другим вызывают его компоненты в форме a.f(..). Так все продолжается, пока не завершится вычисление.

Инвариант является характеристическим свойством состояний, представленных большими квадратиками на рисунке: S1, S2, S3 и т.д. Эти состояния соответствуют стабильным временам, упомянутым выше.

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

Инвариант в момент изменения

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

Кто должен обеспечить сохранность инвариантов

Квалифицированные вызовы в форме a.f(...), выполняемые на стороне клиента, всегда начинаются и заканчиваются в состоянии, удовлетворяющем инварианту. Подобного правила нет для неквалифицированных вызовов в форме f(...), недоступных для клиентов, но используемых в квалифицированных вызовах для служебных целей. Как следствие, обязанность управлять инвариантами возлагается только на модули, экспортируемые всем клиентам или выборочно. Закрытые методы, недоступные клиентам, не обязаны беспокоиться об инвариантах.

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

Правило инварианта

Утверждение Inv является корректным инвариантом класса, если и только если оно удовлетворяет следующим двум условиям:

1 Каждая процедура создания, применимая к аргументам, удовлетворяющим ее предусловию в состоянии, в котором атрибуты имеют значения, установленные по умолчанию, вырабатывает заключительное состояние, гарантирующее выполнение Inv.

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

Заметьте, в этом правиле:

[x]. Предполагается, что каждый класс обладает процедурой создания, задаваемой конструктором по умолчанию, при отсутствии явного ее определения.

[x]. Состояние объекта определяется значениями всех его полей (значениями атрибутов класса для этого конкретного экземпляра).

[x]. Предусловие программы может включать начальное состояние и аргументы.

[x]. Постусловие может включать только заключительное состояние, начальное состояние, (используя нотацию old) и, в случае функций, возвращаемое значение, заданное предопределенной сущностью Result.

[x]. Инвариант может включать только состояние.

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

Можно использовать правило Инварианта как основу для ответа на вопрос, что означает нарушение инварианта в период выполнения системы? Мы уже установили, что нарушение предусловия означает ошибку (жучок) клиента, нарушение постусловия - ошибка поставщика. Для инвариантов ответ такой же, как и для постусловий[21].

Роль инвариантов класса в программной инженерии

Свойство (2) правила инвариантов показывает, что неявно их можно рассматривать как добавления к предусловиям и постусловиям каждой экспортируемой программы класса. Посему принципиально понятие инварианта класса избыточно - это часть предусловий и постусловий программ.

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

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

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

Инварианты и контракты

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

Давайте пойдем дальше. Выше отмечалось, что инварианты можно рассматривать как добавки к предусловиям и постусловиям экспортируемых программ. Пусть body тело программы, pre - предусловие, post - постусловие, Inv - инвариант программы. Требование корректности программы может быть записано в виде:

INV and pre body INV and post

Это означает, что любое выполнение body, начинающееся в состоянии, удовлетворяющем Inv и pre, завершится в состоянии, в котором выполняются Inv и post. Для человека, создающего body, появление инварианта является "хорошей" или "плохой" новостью, облегчается или затрудняется его задача? Ответ, как следует из предыдущих обсуждений, и да и нет! Вспомним ленивого работника, который мечтает о сильном предусловии и слабом постусловии, чтобы можно было бы работать как можно меньше. Инвариант усиливает как предусловие, так и постусловие. Так что, если вы ответственны за реализацию body, то добавление инварианта:

[x]. Облегчает работу: накладывая на клиента более жесткие требования, уменьшая тем самым число ситуаций, при которых нужно приступать к работе.

[x]. Усложняет работу: помимо постусловия в заключительном состоянии необходимо гарантировать выполнение инварианта.

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

Класс BANK_ACCOUNT, упоминавшийся выше, с инвариантом класса:

deposits_list.total - withdrawals_list.total = balance

дает хороший пример. При добавлении в класс новой программы гарантируется, что свойства deposits_list, withdrawals_list, balance имеют согласованные значения, посему нет необходимости в проверках согласованности. Но это также означает, что при написании программы следует следить за сохранением согласованности. Так что процедура withdraw, которая занимается снятием некоторых сумм со счетов, должна в конце работы изменить соответственно и баланс - атрибут balance.

Заметьте, balance может быть не атрибутом, а функцией, возвращающей значение, вычисляемое, например, так: deposits_list.total - withdrawal_list.total. В этом случае процедуре withdraw вообще ничего не нужно делать для обеспечения выполнимости инварианта. Возможность переключаться между двумя представлениями (атрибута и функции) без влияния на клиента обеспечивается принципом Унифицированного доступа.

Когда класс корректен?

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

Корректность класса

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

Класс, подобно всем остальным программным элементам, не может быть корректным или некорректным сам по себе, - только по отношению к некоторой спецификации. Инварианты, предусловия и постусловия, это способ задания спецификации класса. На этой основе можно приступать к определению корректности: класс корректен, если и только если его реализация, заданная подпрограммами, согласована с предусловиями, постусловиями и инвариантами.

Нотация P A Q поможет выразить наше определение более строго.

Пусть C обозначает класс, Inv - инвариант, r - программа класса. Для каждой программы Bodyr - ее тело, prer(xr), postr(xr) - ее предусловие и постусловие с возможными аргументами xr. Если предусловие или постусловие для программы r опущены, то будем считать их заданными константой True.

Наконец, пусть DefaultC обозначает утверждение, выражающее тот факт, что атрибуты класса C имеют значения по умолчанию, определенные их типами. Например, DefaultSTACK2 для класса STACK2 является следующим утверждением:

representation = Void

capacity = 0

count = 0

Эта нотация позволяет дать общее определение корректности класса:

Определение: Корректность класса

Класс C корректен по отношению к своим утверждениям, если и только если:

Для любого правильного множества аргументов xp процедуры создания p:

DefaultC and prep(xp) Bodyp postp(xp) and Inv

Для каждой экспортируемой программы r и для любого множества правильных аргументов xr:

prer(xr) and Inv Bodyr postr(xr) and Inv

Это правило является математической формулировкой ранее рассмотренной неформальной диаграммы, показывающей жизненный цикл типичного объекта (рис. 11.4). Условие (1) означает, что любая процедура создания при ее вызове с выполняемым предусловием должна вырабатывать начальное состояние (S1 на рисунке), удовлетворяющее постусловию и инварианту. Условие (2) отражает тот факт, что любая экспортируемая процедура r (f и g на рисунке), вызываемая в состояниях (S1, S2, S3), удовлетворяющих предусловию и инварианту, должна завершаться в состояниях, удовлетворяющих постусловию и инварианту.

Два практических замечания:

[x]. Если у класса нет предложения creation, то можно полагать, что существует неявная процедура создания по умолчанию - nothing с пустым телом. Применение правила (1) к Bnothing в этом случае означает, что DefaultC влечет Inv; другими словами, значения полей по умолчанию должны удовлетворять инварианту в этом случае.

[x]. Из определения корректности класса следует, что любая экспортируемая программа может делать, все что угодно, если при ее вызове нарушается предусловие или инвариант.

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

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