Разница между
Коды исключений являются целыми. Значения для предопределенных исключений задаются целочисленными константами, обеспечиваемыми классом
Check_instruction: INTEGER is 7
-- Код исключения при нарушении утверждения check
Class_invariant: INTEGER is ...
-- Код исключения при нарушении инварианта класса
Incorrect_inspect_value: INTEGER is ...
-- Код исключения, когда проверяемое значение не является ни одной
-- ожидаемых констант, если отсутствует часть Else
Loop_invariant: INTEGER is ...
-- Код исключения при нарушении инварианта цикла
Loop_variant: INTEGER is ...
-- Код исключения при нарушении убывания варианта цикла
No_more_memory: INTEGER is ...
-- Код исключения при отказе в распределении памяти
Postcondition: INTEGER is ...
-- Код исключения при нарушении постусловия
Precondition: INTEGER is ...
-- Код исключения при нарушении предусловия
Routine_failure: INTEGER is ...
-- Код исключения при отказе вызванной программы
Void_assigned_to_expanded: INTEGER is ...
Так как значения констант не играют здесь роли, то показано только первое из них.
Приведу несколько других запросов, обеспечивающих при необходимости дополнительной информацией. Смысл запросов понятен из их описания:
meaning (except: INTEGER)
-- Сообщение, описывающее природу исключения с кодом except
is_assertion_violation: BOOLEAN
-- Является ли последнее исключение нарушением утверждения
-- или нарушением убывания варианта цикла
ensure
Result = (exception = Precondition) or (exception = Postcondition) or
(exception = Class_invariant) or
(exception = Loop_invariant) or (exception = Loop_variant)
is_system_exception: BOOLEAN
-- Является ли последнее исключение внешним событием
-- (ошибкой операционной системы)?
is_signal: BOOLEAN
-- Является ли последнее исключение сигналом операционной системы?
tag_name: STRING
-- Метка утверждения, нарушение которого привело к исключению
original_tag_name: STRING
-- Метка последнего нарушенного утверждения оригинальным исключением.
recipient_name: STRING
-- Имя программы, чье выполнение было прервано последним исключением
class_name: STRING
-- Имя класса, включающего получателя последнего исключения
original_recipient_name: STRING
-- Имя программы, чье выполнение было прервано
-- последним оригинальным исключением
original_class_name: STRING
-- Имя класса, включающего получателя последнего оригинального исключения