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

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

-- Пара имеет тот же НОД, что и пара

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

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

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

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

Отсюда, в свою очередь, следует, что 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

-- Пара имеет тот же НОД, что и пара

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].Поддержка приемлемого способа обработки неисправностей.

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

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