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