11.5. Обработка ошибок в языке Eiffei

Утверждения

В языке Eiffei подход к обработке исключений основан на концепции, что, прежде всего, ошибок быть не должно. Конечно, все программисты борются за это, и особенность языка Eiffei состоит в том, что в него включена поддер­жка определения правильности программы. Она основана на понятии утвер­ждений (assertions), которые являются логическими формулами и обычно ис­пользуются для формализации программы, но не являются непосредственно частью ее (см. раздел 2.2). Каждая подпрограмма, называемая рутиной (rou­tine) в Eiffei, может иметь связанные с ней утверждения. Например, подпро­грамма для вычисления результата (result) и остатка (remainder) целочисленно­го деления делимого (dividend) на делитель (divisor) была бы написана следую­щим образом:

integer_division(dividend, divisor, result, remainder: INTEGER) is

require

divisor > 0

do

from

result = 0; remainder = dividend;

invariant

dividend = result*divisor + remainder

variant

remainder

until

remainder < divisor

loop

remainder := remainder - divisor;

result := result + 1 ;

end

ensure

dividend = result*divisor + remainder;

remainder < divisor

end

Конструкция require (требуется) называется предусловием и специ­фицирует, какие выходные данные подпрограмма считает правильными. Конструкция do (выполнить) содержит выполняемые операторы, собственно и составляющие программу. Конструкция ensure (гарантируется) называется постусловием и содержит. условия, истинность которых подпрограмма обещает обеспечить, если будет выполнена конструкция do над данными, удовлетворяющими предусловию. В данном случае справедливость постус­ловия является достаточно тривиальным следствием инварианта (см. 6.6) и условия until.

На большем масштабе вы можете присоединить инвариант к классу (см. раздел 15.4). Например, класс, реализующий стек с помощью массива, вклю­чал бы инвариант такого вида:

invariant

top >= 0;

top < max;

Все подпрограммы класса должны гарантировать, что инвариант истинен, когда объект класса создан, и что каждая подпрограмма сохраняет истиность инварианта. Например, подпрограмма pop имела бы предусловие top> 0, в противном случае выполнение оператора:

top := top - 1

могло бы нарушить инвариант.

Типы перечисления

Инварианты применяются также, чтобы гарантировать безопасность типа, которая достигается в других языках использованием типов перечисления. Следующие объявления в языке Ada:

Dial: Heat;

были бы записаны на языке Eiffel как обычные целые переменные с имено­ванными константами:

Dial: Integer;

Off: Integer is 0;

Low: Integer is 1;

Medium: Integer is 2;

High: Integer is 3;

Инвариант гарантирует, что бессмысленные присваивания не выполнятся:

invariant

Off <= Dial <= High

Последняя версия языка Eiffel включает уникальные константы (unigue con­stants), похожие на имена перечисления в том отношении, что их фактические значения присваиваются компилятором. Однако они по-прежнему остаются целыми числами, поэтому безопасность типа должна по-прежнему обеспе­чиваться с помощью утверждений: постусловие должно присоединяться к лю­бой подпрограмме, которая изменяет переменные, чьи значения должны быть ограничены этими константами.

Проектирование по контракту

Утверждения — базовая компонента того, что язык Eiffel называет проекти­рованием по контракту, в том смысле, что проектировщик подпрограммы заключает неявный контракт с пользователем подпрограммы: если вы обес­печите состояние, которое удовлетворяет предусловию, то я обещаю преоб­разовать состояние так, чтобы оно удовлетворяло постусловию. Точно так же класс поддерживает истинность своих инвариантов. Если контракты ис­пользуются в системе повсеместно, то ничто никогда не может идти непра­вильно.

На практике, конечно, разработчик может потерпеть неудачу, пытаясь со­здать соответствующую контракту подпрограмму (либо потому, что операто­ры не удовлетворяют утверждениям, либо потому, что были выбраны непра­вильные утверждения). Для отладки и тестирования в реализации языка Eiffel для пользователя предусмотрена возможность запросить проверку утвержде­ний при входе в подпрограмму и выходе из нее так, чтобы можно было оста­новить выполнение, если утверждение неверно.

Исключения

Подпрограммы Eiffel могут содержать обработчики исключений:

proc is

do

… -- Может возбуждаться исключение

rescue

… -- Обработчик исключения

end;

Когда возбуждается исключение, считается, что подпрограмма потерпела не­удачу, и выполняются операторы после rescue. В отличие от языка Ada, после завершения обработчика исключение порождается снова в вызывающей про­грамме. Это эквивалентно завершению в Ada обработчика исключения raise-оператором, который повторно порождает в вызывающей подпрограмме то же самое исключение, которое заставило вызвать обработчик.

Мотивировка такого решения в предположении, что постусловие подпрограммы (и/или инвариант класса) удовлетворяются.

Если это не так, то вам, возможно, захочется получить уведомление, но уж наверняка вы не можете удовлетворить постусловие, т. е. потерпели неудачу при выполнении работы, которую заказала вам вызывающая под­программа. Другими словами, если.вам известно, как справиться с проблемой и удовлетворить постусловие, то предусмотрите это в подпро­грамме. Это аналогично нашему совету не пользоваться исключениями вместо операторов if.

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

Обработчик исключений в языке Ada можно смоделировать в Eiffel следу­ющим образом, хотя это идет вразрез с философией языка:

proc is

local

tried: Boolean; -- Инициализировано как false;

do

if not tried then

-- Обычная обработка

-- Порождает исключения

else

-- «Обработчик исключения»

end

rescue

if not tried then

tried := true; -- Чтобы не было двойного повтора

retry

end

end;