Когда нет предложения rescue

5.

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

4.

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

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 ведет к отказу, но, прежде чем передать управление клиенту, необходимо восстановить стабильное состояние. Это означает необходимость восстановления инварианта класса.

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

True Rescuer INV

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

True Retryr INV and prer

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

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

prer and INV Bodyr postr (xr) INV

True Rescuer INV

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

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

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

Формализовав роль предложения rescue, вернемся к рассмотрению ситуации, когда это предложение отсутствует в программе. Правило для этого случая было введено ранее, но с обязательством его уточнения. Ранее полагалось, что отсутствующее предложение rescue эквивалентно присутствию пустого предложения (rescue end). В свете наших формальных правил это не всегда является приемлемым решением. Правило (3) требует:

True Rescuer INV

Если Rescuer является пустой инструкцией, а инвариант не тождественен True, то правило не выполняется.

Зададим точное правило. Класс Any является корневым классом - прародителем всех классов. В состав этого класса включена процедура default_rescue, наследуемая всеми классами - потомками Any:

default_rescue is

-- Обрабатывает исключение, если нет предложения rescue.

-- (По умолчанию: ничего не делает)

do

end

Программа, не имеющая предложения rescue, рассматривается теперь как эквивалентная программе с предложением rescue в следующей форме:

rescue

default_rescue

Каждый класс может переопределить default_rescue, для выполнения специфических действий, гарантирующих восстановление инварианта класса, вместо эффекта пустого действия, заданного по умолчанию в GENERAL. Механизм переопределения компонент класса будет изучаться в последующих лекциях, посвященных наследованию.

Вы, конечно, помните, что одна из ролей процедуры создания состоит в производстве состояния, удовлетворяющего инварианту класса INV. Отсюда понятно, что во многих случаях переопределение default_rescue может основываться на использовании процедур создания.

Дата добавления: 2014-01-07