Теперь заметим: для того чтобы
Теперь заметим: для того чтобы завершить цикл, булево условие в цикле while должно иметь значение False, то есть вычисление должно быть в таком состоянии, при котором --(х > b), что эквивалентно х < b. Объединив эту формулу с инвариантом, мы показали, что программа действительно выполняет целочисленное деление.
Точнее, если программа завершается, то результат является правильным. Это называется частичной правильностью. Чтобы доказать полную правильность, мы должны также показать, что цикл завершается.
Это делается следующим образом. Так как во время выполнения программы b является константой (и предполагается положительной!), нам нужно показать, что неоднократное уменьшение х на b должно, в конечном счете, привести к состоянию, в котором 0 < х < b. Но 1) поскольку х уменьшается неоднократно, его значение не может бесконечно оставаться больше значения b; 2) из условия завершения цикла и из вычисления в теле цикла следует, что х никогда не станет отрицательным. Эти два факта доказывают, что цикл должен завершиться.
Инварианты цикла в языке Eiffel
Язык Eiffel имеет в себе средства для задания контрольных утверждений вообще (см. раздел 11.5) и инвариантов циклов в частности:
from
у = 0; х = а;
invariant
|
Eiffel |
variant
х
until
x< b
loop
x :=x-b;
у:=у+1;
end
Конструкция from устанавливает начальные условия, конструкция until задает условие для завершения цикла, а операторы между loop и end образуют тело цикла. Конструкция invariant определяет инвариант цикла, а конструкция variant определяет выражение, которое будет уменьшаться (но останется неотрицательным) с каждой итерацией цикла. Правильность инварианта проверяется после каждого выполнения тела цикла.
6.7.
