Инвариант гарантирует, что бессмысленные присваивания
Dial: Integer;
Off: Integer is 0;
Low: Integer is 1;
Medium: Integer is 2;
High: Integer is 3;
Инвариант гарантирует, что бессмысленные присваивания не выполнятся:
invariant
Off <= Dial <= High
Последняя версия языка Eiffel включает уникальные константы (unigue constants), похожие на имена перечисления в том отношении, что их фактические значения присваиваются компилятором. Однако они по-прежнему остаются целыми числами, поэтому безопасность типа должна по-прежнему обеспечиваться с помощью утверждений: постусловие должно присоединяться к любой подпрограмме, которая изменяет переменные, чьи значения должны быть ограничены этими константами.
Проектирование по контракту
Утверждения — базовая компонента того, что язык Eiffel называет проектированием по контракту, в том смысле, что проектировщик подпрограммы заключает неявный контракт с пользователем подпрограммы: если вы обеспечите состояние, которое удовлетворяет предусловию, то я обещаю преобразовать состояние так, чтобы оно удовлетворяло постусловию. Точно так же класс поддерживает истинность своих инвариантов. Если контракты используются в системе повсеместно, то ничто никогда не может идти неправильно.
На практике, конечно, разработчик может потерпеть неудачу, пытаясь создать соответствующую контракту подпрограмму (либо потому, что операторы не удовлетворяют утверждениям, либо потому, что были выбраны неправильные утверждения). Для отладки и тестирования в реализации языка Eiffel для пользователя предусмотрена возможность запросить проверку утверждений при входе в подпрограмму и выходе из нее так, чтобы можно было остановить выполнение, если утверждение неверно.
Исключения
Подпрограммы Eiffel могут содержать обработчики исключений:
proc is
do
