5. ПРИМЕР ДОКАЗАТЕЛЬСТВА ПРАВИЛЬНОСТИ ПРОГРАММЫ

Рассмотрим следующий фрагмент программы:

integer  r,  dd;
r:=a; dd:=d;
while dd  r do dd:=2*dd; 
while dd  d do 
begin dd:=dd/2;
    if dd  r do r:=r-dd; 
end 

в предположении, что целые константы а и d удовлетворяют отношениям

a 0    и    d 0

Чтобы применить теорему линейного поиска (см. раздел "О наших интеллектуальных средствах", подраздел "О математической индукции"), рассмотрим последовательность значений, заданную формулами

Отсюда с помощью обычных математических приемов можно вывести, что

dd_n=d*2ⁿ     (1)

Кроме того, поскольку d>0, можно сделать вывод, что для любого конечного значения r отношение

dd_k >r

будет выполняться при некотором конечном значении k; первый цикл завершается при

dd=d*2^k

Решая уравнение

ddi=2*d_i-1

относительно d_i-1, получаем

d_i-1=d_i/2

и теперь теорема линейного поиска позволяет нам утверждать, что второй цикл тоже завершится. (На самом деле второй цикл выполнится в точности столько же раз, сколько и первый.)

По окончании первого цикла

dd=dd_k

и поэтому выполняется соотношение

0 r < dd     (2)

Как было показано ранее (раздел "О наших интеллектуальных средствах", подраздел "О перечислении"), это соотношение сохраняется при выполнении повторяемого оператора второго заголовка. После завершения повторений (в соответствии с заголовком while ddd do) мы получим

dd=d

Отсюда и из соотношения (2) следует, что

0 r < d     (3)

Далее мы доказываем, что после начала работы программы всегда выполняется отношение

dd 0 mod (d)     (4)

Это следует, например, из того, что возможные значения dd имеют вид (см. (1))

d*2ⁱ при 0 i k

Наша следующая задача состоит в том, чтобы показать, что после присваивания r начального значения всегда выполняется отношение

a r mod (d)     (5)

Объединяя отношения (3) и (5), получаем, что окончательное значение r удовлетворяет условиям

0 r < d    и    a r mod (d)

т.е. r - это наименьший неотрицательный остаток от деления а на d.

Замечание 1. Программа

integer r, dd, q;
r:=a;  dd:=d;   q:=0;
while dd  r do dd:=2*dd;
while dd d do
    begin dd:=dd/2; q:=2*q;
        if dd  r do begin r:=r-dd; q:=q+1 end
end

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

a=q*dd+r

(Я обязан этим примером моему коллеге Н. Г. де Бруэйну.)

Замечание 2. В подразделе "О математической индукции" доказали теорему линейного поиска. В предыдущем доказательстве мы использовали другую теорему о повторениях (которая, разумеется может быть доказана только математической индукцией, но доказательство настолько простое, что мы оставляем его читателю в качестве упражнения). Эта теорема состоит в том, что если перед началом повторений выполняется некоторое соотношение Р, истинность которого не нарушается однократным выполнением повторяемого оператора, то соотношение Р будет выполняться и после завершения повторений. Это очень полезная теорема, и она часто позволяет нам избежать явного применения математической индукции. (Можно сформулировать эту теорему несколько более кратко: для цикла

while В do S

нужно показать, что оператор S таков, что истинность

P B

перед выполнением S означает истинность

Р

после выполнения этого оператора.)

Замечание 3. Предлагаю читателю в качестве упражнения (за которое следует благодарить Дж. Кинга, Питтсбург, США) доказать, что при целых А, В, х, у и z и при условии, что

A > 0    и    B > 0

после выполнения фрагмента программы

х:=А;  у:=В;  z:=1;  
while y  0 do
    begin if нечет (у) do
        begin y:=y -1; z:=z*x end;
        y:=y/2; x:=x*x;
    end

будет получено окончательное значение z = А^B.

Доказательство сводится к тому, чтобы показать, что (несмотря на оператор у:=у/2) все переменные сохраняют целые значения. Наш метод позволяет показать инвариантность отношений

x > 0    и    y 0    и    А^B = z*х^y