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

post = inv and exit

так что мы можем остановить цикл, - чьи промежуточные состояния по построению удовлетворяют inv , - как только выполнится exit . В этом состоянии, следовательно, будет выполнено и post .

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

[x].Инвариант цикла inv - утверждение.

[x].Условие выхода exit , чья конъюнкция с inv дает желаемую цель.

[x].Вариант var - целочисленное выражение.

[x].Множество инструкций инициализации, которые всегда приводят к состоянию, в котором inv выполняется, а var становится неотрицательным.

[x].Множество инструкций body , которое (при условии, что оно начинается в состоянии, где var неотрицательно и выполняется inv ), сохраняет инвариант и уменьшает var , в то же время следя за тем, чтобы оно не стало меньше нуля.

[x].Синтаксис цикла честно комбинирует эти ингредиенты:

from

init

invariant

inv

variant

var

until

exit

loop

body

end

Предложения invariantи variantявляются возможными. Предложение fromпо синтаксису требуется, но инструкция init может быть пустой.

Эффект выполнения цикла можно описать так: вначале выполняется init , затем 0 или более раз выполняется тело цикла, которое перестает выполняться, как только exit принимает значение false .

В языках Pasal, C и других такой цикл называется "циклом while", в отличие от цикла типа " repeat ... until", в котором тело цикла выполняется, по меньшей мере, один раз. Здесь же тест является условием выхода, а не условием продолжения, и синтаксис цикла явно содержит фазу инициализации. Потому эквивалент записи нашего цикла на языке Pascal выглядит следующим образом:

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

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

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