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

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

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

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

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

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