Корректность предложения rescue
Корректность предложения rescue
Формальное определение корректности класса выдвигает два требования к компонентам класса. Первое (1) требует, чтобы процедуры создания гарантировали корректную инициализацию - выполнение инварианта класса. Второе (2) напрямую относится к нашему обсуждению, требуя от каждой программы, запущенной при условии выполнения предусловия и инварианта класса, выполнения в завершающем состоянии постусловия и инварианта класса. Диаграмма, описывающая жизненный цикл объекта, отражает эти требования:
Рис. 12.3. Жизнь объекта
Формально правило (2) говорит:
3.
Для каждой экспортируемой программы r и любого множества правильных аргументов xr
{prer (xr) and INV} Bodyr {postr (xr) and INV}
Для простоты позвольте в дальнейшем рассмотрении игнорировать аргументы xr.
Пусть Rescuer обозначает ту часть предложения rescue, в которой игнорируются все ветви, ведущие к retry, другими словами в этой части сохраняются все ветви, доходящие до конца предложения rescue. Правило (2) задает спецификацию для программ тела - Bodyr. Можно ли получить такую же спецификацию для Rescuer? Она должна иметь вид:
{ ? } Rescuer { ? }
с заменой знаков вопроса соответствующими утверждениями. (Полезно, перед дальнейшим чтением постараться самостоятельно задать эти утверждения.)
Рассмотрим, прежде всего, предусловие для Rescuer. Любая попытка написать нечто не тривиальное будет ошибкой! Напомним, чем сильнее предусловие, тем проще работа программы. Любое предусловие для Rescuer ограничит число случаев, которыми должна управлять эта программа. Но она должна работать во всех ситуациях! Когда возникает исключение, ничего нельзя предполагать, - такова природа исключения. Нам не дано предугадать, когда компьютер даст сбой, или пользователю вздумается нажать клавишу "break".
Поэтому остается единственная возможность - предусловие для Rescuer равно True. Это самое слабое предусловие, удовлетворяющее всем состояниям и означающее, что Rescuer должна работать во всех ситуациях.
Для ленивого создателя Rescuer это "плохая новость", - тот случай, когда "заказчик всегда прав"!
Что можно сказать о постусловии Rescuer? Напомню, эта часть предложения rescue ведет к отказу, но, прежде чем передать управление клиенту, необходимо восстановить стабильное состояние. Это означает необходимость восстановления инварианта класса.
Отсюда следует правило, в котором уже больше нет знаков вопросов:
Правило корректности для включающего отказ предложения rescue
4.
{True} Rescuer {INV}
Похожие рассуждения дают правило для Retryr - части предложения rescue, включающей ветви, приводящие к инструкции retry:
Правило корректности для включающего повтор предложения rescue
5.
{True} Retryr {INV and prer }