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

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 - программа класса. Для каждой программы Body_r - ее тело, pre_r(x_r) , post_r(x_r) - ее предусловие и постусловие с возможными аргументами x_r. Если предусловие или постусловие для программы r опущены, то будем считать их заданными константой True.

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

representation = Void
capacity = 0
count = 0

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

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

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

1

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

{Default_C and pre_p(x_p)} Body_p {post_p(x_p) and Inv}

2

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

{pre_r(x_r) and Inv} Body_r {post_r (x_r) and Inv}

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

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

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

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

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