Заметки по структурному программированию

       

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


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

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


Содержание раздела