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

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

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

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

а≥0 и d>0

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

для i=0 dd_i=d

для i>0 dd_i=2*dd_i-1

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

dd_n=d*2ⁿ (1)

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

dd_k>r

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

dd=d*2^k

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

d_i=2*d_i-1

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

d_i-1= d_i/2

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

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

dd=dd_k

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

0≤r<dd (2)

Это соотношение сохраняется при выполнении повторяемого оператора второго заголовка. После завершения повторений (в соответствии с заголовком while dd≠d do) мы получим

dd=d

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

0≤r<d (3)

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

dd≡0 mod (d) (4)

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

d*2ⁱ при 0≤i≤k

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

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.

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

while В do S

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

Р/\В

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

Р

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

29. Типы разложения вычислений (сочленение, выбор, повторение).