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

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? Для проверки этого следует заметить, что следующее свойство истинно после инициализации цикла и сохраняется на каждой итерации: