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