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

Корректность предложения rescue

Формальное определение корректности класса выдвигает два требования к компонентам класса. Первое (1) требует, чтобы процедуры создания гарантировали корректную инициализацию - выполнение инварианта класса. Второе (2) напрямую относится к нашему обсуждению, требуя от каждой программы, запущенной при условии выполнения предусловия и инварианта класса, выполнения в завершающем состоянии постусловия и инварианта класса. Диаграмма, описывающая жизненный цикл объекта, отражает эти требования:

Рис. 12.3.  Жизнь объекта

Формально правило (2) говорит:

3.

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

{prer (xr) and INV} Bodyr {postr (xr) and INV}

Для простоты позвольте в дальнейшем рассмотрении игнорировать аргументы x_r.

Пусть Rescue_r обозначает ту часть предложения rescue, в которой игнорируются все ветви, ведущие к retry, другими словами в этой части сохраняются все ветви, доходящие до конца предложения rescue. Правило (2) задает спецификацию для программ тела - Body_r. Можно ли получить такую же спецификацию для Rescue_r? Она должна иметь вид:

{ ? } Rescuer { ? }

с заменой знаков вопроса соответствующими утверждениями. (Полезно, перед дальнейшим чтением постараться самостоятельно задать эти утверждения.)

Рассмотрим, прежде всего, предусловие для Rescue_r. Любая попытка написать нечто не тривиальное будет ошибкой! Напомним, чем сильнее предусловие, тем проще работа программы. Любое предусловие для Rescue_r ограничит число случаев, которыми должна управлять эта программа. Но она должна работать во всех ситуациях! Когда возникает исключение, ничего нельзя предполагать, - такова природа исключения. Нам не дано предугадать, когда компьютер даст сбой, или пользователю вздумается нажать клавишу 'break'.

Поэтому остается единственная возможность - предусловие для Rescue_r равно True. Это самое слабое предусловие, удовлетворяющее всем состояниям и означающее, что Rescue_r должна работать во всех ситуациях.

Для ленивого создателя Rescue_r это 'плохая новость', - тот случай, когда 'заказчик всегда прав'!

Что можно сказать о постусловии Rescue_r? Напомню, эта часть предложения rescue ведет к отказу, но, прежде чем передать управление клиенту, необходимо восстановить стабильное состояние. Это означает необходимость восстановления инварианта класса.

Отсюда следует правило, в котором уже больше нет знаков вопросов:

Правило корректности для включающего отказ предложения rescue

4.

{True} Rescuer {INV}

Похожие рассуждения дают правило для Retry_r - части предложения rescue, включающей ветви, приводящие к инструкции retry:

Правило корректности для включающего повтор предложения rescue

5.

{True} Retryr {INV and prer }

Четкое разделение ролей

Интересно сравнить формальные роли тела и предложения Rescue_r:

{prer and INV} Bodyr {postr (xr) INV}
{True} Rescuer {INV}

Входное утверждение сильнее для Body_r - в то время, когда Rescue_r не накладывает никаких требований, перед началом выполнение тела программы (предложения do) должно выполняться предусловие и инвариант. Это упрощает работу Body_r.

Выходное утверждение также сильнее для Body_r - в то время, когда Rescue_r обязана восстановить только инвариант класса, Body_r обязана сыграть свою роль и обеспечить истинность выполнения постусловия. Это делает ее работу более трудной.

Эти правила отражают разделение ролей между предложением do и предложением rescue. Задача тела обеспечить выполнение контракта программы, не управляя непосредственно исключениями. Задача rescue - управлять обработкой исключениями, возвращая управление либо телу программы, либо вызывающей программе. Но в обязанности rescue не входит обеспечение контракта.