Хотя у отложенного компонента нет реализации, а у отложенного класса либо нет реализации, либо он реализован частично, часто требуется задать их абстрактные семантические свойства. Для этой цели можно использовать утверждения.
Как и другие классы, отложенный класс может иметь инвариант, а у отложенного компонента может быть предусловие, постусловие или оба эти утверждения.
Рассмотрим пример линейных списков, описанных независимо от конкретной реализации. Как и для многих других структур такого рода, удобно связать с каждым списком курсор, указывающий на текущий активный элемент.
Этот класс является отложенным:
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. Такой выбор всегда возникает при выражении свойств, включающих только запросы без аргументов. Я предпочитаю использовать предложения инварианта, рассматривая такие свойства как глобальные свойства класса, а не прикреплять их к конкретному компоненту. |