Основы объектно-ориентированного программирования - Бертран Мейер

init;

while not exit do body

С вариантами и инвариантами цикл для maxarray выглядит так:

from

i := t.lower; Result := t @ lower

invariant

-- Result является максимумом нарезки массива t в интервале [t.lower,i].

variant

t.lower - i

until

i = t.upper

loop

i := i + 1

Result := Result.max (t @ i)

End

Заметьте, инвариант цикла выражен неформально, в виде комментария. Последующее обсуждение в этой лекции объяснит это ограничение языка утверждений.

Вот еще один пример, ранее показанный без вариантов и инвариантов. Целью следующей функции является вычисление наибольшего общего делителя - НОД (gcd - greatest common divisor) двух положительных целых a и b, следуя алгоритму Эвклида:

gcd (a, b: INTEGER): INTEGER is

-- НОД a и b

require

a > 0; b > 0

local

x, y: INTEGER

do

from

x := a; y := b

until

x = y

loop

if x > y then x := x - y else y := y - x end

end

Result := x

ensure

-- Result является НОД a и b

end

Как узнать, что функция gcd удовлетворяет своему постусловию и действительно вычисляет наибольший общий делитель a и b? Для проверки этого следует заметить, что следующее свойство истинно после инициализации цикла и сохраняется на каждой итерации:

x > 0; y > 0

-- Пара <x, y> имеет тот же НОД, что и пара <a, b>

Это и будет служить инвариантом цикла inv. Ясно, что inv выполняется после инициализации. Если выполняется inv и условие цикла x /= y, то после выполнения тела цикла:

if x > y then x := x - y else y := y - x end

инвариант inv остается истинным, замена большего из двух положительных неравных чисел их разностью не меняет их gcd и оставляет их положительными. Тогда по завершению цикла следует:

x = y and «Пара <x, y> имеет тот же НОД, что и пара <a, b>»

Отсюда, в свою очередь, следует, что x является наибольшим общим делителем. По определению НОД (x, x) = x.

Как узнать, что цикл всегда завершается? Необходим вариант. Если x больше чем y, то в теле цикла x заменяется разностью x-y. Если y больше x, то y заменяется разностью y-x. Нельзя в качестве варианта выбрать ни x, ни y, поскольку для каждого из них нет гарантии уменьшения. Но можно быть уверен, что максимальное из них обязательно будет уменьшено. Поэтому разумно выбрать в качестве варианта x.max(y). Заметьте, вариант всегда остается положительным. Теперь можно написать цикл со всеми предложениями:

from

x := a; y := b

invariant

x > 0; y > 0

-- Пара <x, y> имеет тот же НОД, что и пара <a, b>

variant

x.max (y)

until

x = y

loop

if x > y then x := x - y else y := y - x end

end

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

Использование утверждений

Теперь мы уже познакомились со всеми конструкциями, содержащими утверждения. Разумно, еще раз взглянуть на те преимущества, которые мы можем получить от этого. Выделим четыре основных применения.

[x]. Помощь в создании корректного ПО.

[x]. Поддержка документирования.

[x]. Поддержка тестирования, отладки и гарантия качества.

[x]. Поддержка приемлемого способа обработки неисправностей.

Только два последних пункта предполагают мониторинг утверждений в период выполнения.

Утверждения как средство для написания корректного ПО

Первое использование является чисто методологическим и, вероятно, самым важным. В деталях оно рассматривалось в предыдущих разделах: точные требования к каждой программе, глобальные свойства классов и циклов - все это помогает разработчикам производить программный продукт, корректный с самого начала в противоположность подходу, пытающемуся добиться корректности в процессе отладки. Преимущества точной спецификации и систематического подхода к конструированию программ не могут быть преувеличены. Во всей этой книге всякий раз при встрече с программным элементом его формальные свойства выражались точно, насколько это было возможным.

Ключевая идея этой лекции - Проектирование по контракту. Использование компонент некоторого модуля является контрактом с его службами. Хорошие контракты точно специфицируют и ограничивают права и обязанности каждого участника. В проектировании ПО, где корректность и устойчивость так важны, необходимо раскрытие терминов контракта, как предварительное условие их следованию. Утверждения дают способ точно установить, что ожидается и что гарантируется каждой стороне в этом соглашении.

Использование утверждений для документирования: краткая форма класса

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

В самом последнем разделе этой лекции можно ознакомиться с проектом, где эти правила были проигнорированы, что обошлось в $500 миллионов и привело к провалу космического проекта.

Средство автоматической документации short использует утверждения, как важную компоненту при извлечении из класса информации, значимой для потенциальных клиентов. Краткая форма класса - его описание на более высоком уровне. Она включает только ту информацию, которая полезна авторам клиентских классов, ничего не показывая из скрытых компонент, и не раскрывая реализации открытых. Но краткая форма сохраняет утверждения, составляющие основу документации, устанавливая контракты, которые класс предлагает своим клиентам.

Вот пример краткой формы класса STACK4:

indexing

description: "Стеки: Структуры с политикой доступа Last-In, First-Out %

%Первый пришел - Последний ушел, с фиксированной емкостью"

class interface STACK4 [G] creation

make

feature -- Initialization (Инициализация)

make (n: INTEGER) is

-- Создать стек, содержащий максимум n элементов

require

non_negative_capacity: n >= 0

ensure

capacity_set: capacity = n

end

feature -- Access (Доступ)

capacity: INTEGER

-- Максимальное число элементов стека

count: INTEGER

-- Число элементов стека

item: G is

-- Элемент в вершине стека

require

not_empty: not empty -- i.e. count > 0

end

feature -- Status report (Отчет о статусе)

empty: BOOLEAN is

-- Пуст ли стек?

ensure

empty_definition: Result = (count = 0)

end

full: BOOLEAN is

-- Заполнен ли стек?

ensure

full_definition: Result = (count = capacity)

end

feature -- Element change (Изменение элементов)

put (x: G) is

-- Втолкнуть x в вершину стека

require

not_full: not full

ensure

not_empty: not empty

added_to_top: item = x

one_more_item: count = old count + 1

end

remove is

-- Удалить элемент вершины стека

require

not_empty: not empty -- i.e. count > 0

ensure

not_full: not full

one_fewer: count = old count - 1

end

invariant

count_non_negative: 0 <= count