While y r do

Begin

r := r - y; q := q + 1

end;

выдать(q,r);

Сформулируем постусловие R: (r < y) AND (x = y*q + r).

Нужно доказать, что {y > 0 ANDx/y} S {(r < y) AND (x = y*q + r)}.

Доказательство.

1.Очевидно, что Q => x = x + y*0.

2.Применим аксиому A1 к оператору r := x, тогда получим

{x = x + y*0 } r := x {x = r + y*0}.

3.Аналогично, применяя A1 к оператору q := 0, получим:

{x = r + y*0} q := 0 {x = r + y*q}.

4.Применяя правило A3 к результатам пунктов 1 и 2, получим

{Q} r := x {x = r + y*0}.

5.Применяя правило A4 к результатам пунктов 4 и 3, получим

{Q} r := x; q := 0 {x = r + y*q}.

6.Выполним равносильное преобразование

x = r + y*q ANDy r => q = (r - y) + y*(q + 1).

7.Применяя правило A1 к оператору r := r - y, получим

{x = (r - y) + y*(q + 1)} r := r - y {x = r+ y*(q+1)}.

8.Для оператора q := q + 1 аналогично получим

{x = r + y*(q + 1)} q := q + 1 {x = r + y*q}.

9.Применяя правило A4 к результатам пунктов 7 и 8, получим

{x = (r - y) + y*(q + 1)} r := r - y; q := q + 1 {x = r + y*q}.

10.Применяя правило A2 к результатам пунктов 6 и 9, получим

{x = r + y*q AND y r} r := r - y; q := q + 1 {x = r + y*q}.

11.Применяя правило A8 к результату пункта 10, получим

{x = r + y*q} while y r do begin r := r - y; q := q + 1 end

{NOT (y <= r) AND (x = r + y*q)}.

Высказывание x = r + y*q является инвариантом цикла, так как значение его остается истинным до цикла и после выполнения каждого шага цикла.

12.Применяя правило A4 к результатам пунктов 5 и 11, получаем то, что требовалось доказать: {Q} S {NOT (y r) AND (x = r + y*q)}.

Осталось доказать, что выполнение программы заканчивается.

Доказывать будем от противного, т.е. предположим, что программа не заканчивается. Тогда должна существовать бесконечная последовательность значений r и q, удовлетворяющая условиям

1) y r;

2) r, q Nat.

Но значение r на каждом шаге цикла уменьшается на положительную величину: r := r - y (y > 0). Значит, последовательность значений r и q является конечной, т.е. найдется такое значение r, для которого не будет выполняться условие y r и циклический процесс завершится.