доказательства правильности программы
Рассмотрим следующий фрагмент программы:
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
Чтобы применить теорему линейного поиска (см. раздел "О наших интеллектуальных средствах", подраздел "О математической индукции"), рассмотрим последовательность значений, заданную формулами
для i=0 ddi=d
для i>0 ddi=2*ddi-1
Отсюда с помощью обычных математических приемов можно вывести, что
ddn=d*2n (1)
Кроме того, поскольку d>0, можно сделать вывод, что для любого конечного значения r отношение
ddk >r
будет выполняться при некотором конечном значении k; первый цикл завершается при
dd=d*2k
Решая уравнение
ddi=2*di-1
относительно di-1, получаем
di-1=di/2
и теперь теорема линейного поиска позволяет нам утверждать, что второй цикл тоже завершится. (На самом деле второй цикл выполнится в точности столько же раз, сколько и первый.)
По окончании первого цикла
dd=ddk
и поэтому выполняется соотношение
0 r < dd (2)
Как было показано ранее (раздел "О наших интеллектуальных средствах", подраздел "О перечислении"), это соотношение сохраняется при выполнении повторяемого оператора второго заголовка. После завершения повторений (в соответствии с заголовком while ddd do) мы получим
dd=d
Отсюда и из соотношения (2) следует, что
0 r < d (3)
Далее мы доказываем, что после начала работы программы всегда выполняется отношение
dd 0 mod (d) (4)
Это следует, например, из того, что возможные значения dd имеют вид (см. (1))
d*2i при 0 i k
Наша следующая задача состоит в том, чтобы показать, что после присваивания r начального значения всегда выполняется отношение
a r mod (d) (5)
(1) Оно выполняется после начальных присваиваний. (2) Повторяемый оператор первого заголовка (dd:=2*dd) сохраняет отношение (5), и поэтому весь первый цикл сохраняет отношение (5). (3) Повторяемый оператор из второго цикла состоит из двух операторов. Первый (dd:=dd/2) сохраняет инвариантность (5); второй также сохраняет отношение (5), так как он либо не изменяет значение r, либо уменьшает r на текущее значение dd, а эта операция в силу (4) также сохраняет справедливость отношения (5). Таким образом, весь повторяемый оператор второго цикла сохраняет инвариантность (5), а поэтому и весь второй цикл сохраняет отношение (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
