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

Этот класс является отложенным:
indexing description: "Линейные списки" deferred class LIST [G] feature -- Access count: INTEGER is -- Число элементов deferred end index: INTEGER is -- Положение курсора deferred end item: G is -- Элемент в позиции курсора deferred end feature - Отчет о статусе after: BOOLEAN is -- Курсор за последним элементом? deferred end before: BOOLEAN is -- Курсор перед первым элементом? deferred end feature - Сдвиг курсора forth is -- Передвинуть курсор на одну позицию вперед. require not after deferred ensure index = old index + 1 end ... Другие компоненты ... invariant non_negative_count: count >= 0 offleft_by_at_most_one: index >= 0 offright_by_at_most_one: index <= count + 1 after_definition: after = (index = count + 1) before_definition: before = (index = 0) end
Здесь инвариант выражает соотношения между разными запросами. Первые два предложения утверждают, что курсор может выйти за границы множества элементов не более чем на одну позицию слева или справа.

| Два последних предложения инварианта можно также представить в виде постусловий: ensure Result = (index = count + 1) для after и ensure Result = (index = 0) для before. Такой выбор всегда возникает при выражении свойств, включающих только запросы без аргументов. Я предпочитаю использовать предложения инварианта, рассматривая такие свойства как глобальные свойства класса, а не прикреплять их к конкретному компоненту. |