6.6. Инварианты

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

у = 0;

while (х >- b) { /* Пока b «входит» в х, */

х -= b; /* вычитание b означает, что */

у++; /* результат должен быть увеличен */

}

и рассмотрим формулу:

a = yb +х

где курсивом обозначено значение соответствующей программной перемен­ной. После операторов инициализации она, конечно, будет правильной, по­скольку у = 0 и х = а. Кроме того, в конце программы формула определяет, что у есть результат целочисленного деления а/b при условии, что остаток х мень­ше делителя b.

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

(у + \)b + (х-b)=уb+b+х-b=уb+х=а

Таким образом, выполнение тела цикла переводит программу из состояния, которое удовлетворяет инварианту, в другое состояние, которое по-прежнему удовлетворяет инварианту.

Теперь заметим: для того чтобы завершить цикл, булево условие в цикле while должно иметь значение False, то есть вычисление должно быть в таком состоянии, при котором --(х > b), что эквивалентно х < b. Объединив эту фор­мулу с инвариантом, мы показали, что программа действительно выполняет целочисленное деление.

Точнее, если программа завершается, то результат является правильным. Это называется частичной правильностью. Чтобы доказать полную правиль­ность, мы должны также показать, что цикл завершается.

Это делается следующим образом. Так как во время выполнения програм­мы b является константой (и предполагается положительной!), нам нужно по­казать, что неоднократное уменьшение х на b должно, в конечном счете, при­вести к состоянию, в котором 0 < х < b. Но 1) поскольку х уменьшается неод­нократно, его значение не может бесконечно оставаться больше значения b; 2) из условия завершения цикла и из вычисления в теле цикла следует, что х никогда не станет отрицательным. Эти два факта доказывают, что цикл дол­жен завершиться.

Инварианты цикла в языке Eiffel

Язык Eiffel имеет в себе средства для задания контрольных утверждений вооб­ще (см. раздел 11.5) и инвариантов циклов в частности:

from

у = 0; х = а;

invariant

variant

х

until

x< b

loop

x :=x-b;

у:=у+1;

end

Конструкция from устанавливает начальные условия, конструкция until зада­ет условие для завершения цикла, а операторы между loop и end образуют те­ло цикла. Конструкция invariant определяет инвариант цикла, а конструкция variant определяет выражение, которое будет уменьшаться (но останется неот­рицательным) с каждой итерацией цикла. Правильность инварианта проверя­ется после каждого выполнения тела цикла.