-Al: m>0, n>0.

a-f-0 a-l c-(-m бч-l бч-О d-f-n

ча.стное(сЧ-d) г Ч- остаток (с -4- d)

Л2; c = m>0, d = n>0, a = 6 = 0, в=6:зг1.

>45; am+ 6n = d, am + 6n = c = gd + r, 0<r<d, gcd(c,d) - gcd(m,n).

r E3. r = 0? >/ \

V--ЛДаГ /Конец\

Нет , -

----A4: am + 6n = d = gcd(m,n).

с -f- d, d .f- г; Б4. < Ч-a, a«-a, a < - 9a;

-i45.- am + bn = d, am + 6n = c = d + г 0<r<d, gcd(c,d) = gcd(m,n).

A6: am + bn - d, am + bn = c, d>0, gcd(c, d) = gcd(m,n).

Рис. 4. Блок-схема алгоритма E, дополненная примечгщиями, которые доказывают правильность работы алгоритма.

следует А6. Поэтому нам достаточно доказать, что выполнение А6 до шага Е2 влечет за собой выполнение A3 после этого шага. Заметим, что условие d > О необходимо в А6 для того, чтобы операция Е2 имела смысл.) Нужно показать также, что из A3 (при условии, что г = 0) следует А4, из A3 (при условии, что г / 0) следует А 5 и т. д. Все это доказывается очень просто.

Если доказать утверждение (7) для каждого блока, то все примечания к стрелкам будут верны в любом случае выполнения алгоритма. Теперь мы можем применить индукцию по числу шагов, т. е. по числу стрелок в блок-схеме. При прохождении первой стрелки (той, которая выходит из блока "Начало") утверждение А1 верно, поскольку мы всегда исходим из предположения, что входные значения удовлетворяют заданным условиям.. Таким образом, утверждение, которое соответствует первой стрелке, верно. Если утверждение, которое соответствует п-й стрелке, верно, то согласно (7) утверждение, которое соответствует (п -Ь 1)-й стрелке, тоже верно.

Исходя из этого общего метода доказательство правильности заданного алгоритма, очевидно, сводится к нахождению правильных утверждений, соответствующих стрелкам блок-схемы. Как только данное начальное препятствие будет преодолено, останется лишь рутинная работа, связанная с доказательством того, что каждое утверждение на входе в блок влечет за собой утверждение на-ыходе из блока. В действительности после того как вы придумаете самые трудные из этих утверждений, найти все остальные уже не составит труда. Скажем, если-даны утверждения А1, А4 и А6, уже понятно, какими должны быть утверждения А2, A3 и А5. В нашем

примере самых больших твррческих усилий потребует доказательство утверждения А6; все остальное, в принципе, должно получиться автоматически. Поэтому я и не пытался давать для алгоритмов, приведенных в книге, формальные доказательства с той степенью детализации, которая отражена на рис. 4. Вполне достаточно сформулировать только главные утверждения. Обычно они приводятся либо в ходе обсуждения алгоритма, либо даются в скобках в тексте самого алгоритма.

Этот подход к доказательству корректности алгоритма имеет и другой, еще более важный аспект: он отражает способ нашего понимания алгоритма. Если по.мните, в разделе 1.1 я предупреждал о том, чтобы вы не читали алгоритмы, как роман. Я рекомендую проверять работу алгоритма на Примере одного-двух наборов входных данных. И это не олучайно, так как пробная "прогонка" алгоритма поможет вам мысленно сформулировать утверждения, соответствующие стрелкам на блок-схеме. Автор твердо убежден, что истинная уверенность в корректности алгоритма приходит только тогда, когда мысленно сформулированы все утверждения, приведенные на рис. 4. Отсюда следуют важные психологические выводы, касающиеся передачи алгоритма от одного лица к другому. Речь идет о том, что, объясняя алгоритм кому-либо другому, всегда следует явно формулировать основные утверждения, которые трудно получить автоматически. Например, в случае алгоритма Е нужно обязательно упомянуть утверждение А6.

Но бдительный читатель, конечно, заметил зияюш;зЮ брешь в нашем последнем доказательстве алгоритма Е. Из него нигде не следует, что алгоритм обладает свойством конечности, т. е. рано или поздно его выполнение завершится. Мы доказали только, что если алгоритм конечен, то он дает правильный результат!

(Например, заметим, что алгоритм Е по-прежнему имеет смысл, если его переменные т, п, с, d и г принимают значения типа u + v л/2, где и и v - целые числа*. Переменные q, а, Ь, а, У должны по-прежнему принимать целые значения. Если, например, на вход подать значения /71 = 12-6 \/2 и п = 20-10 \/2, то на выходе будет получен "наибольший общий делитель" d = 4-2 \/2 и коэффициенты а = +2, b = -1. Даже при таком расширении исходных предположений доказательства утверждений от Al до А6 остаются в силе. Следовательно, на любом этапе выполнения этой процедуры все утверждения верны. Но если начать со значений ш = 1 и га = \/2, то вычисления никогда не закончатся (см. упр. 12). Следовательно, из доказательства утверждений А1-А6 еще не следует, что алгоритм конечен.)

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

Итак, мы уже дважды доказали правильность алгоритма Е. Чтобы быть последовательными до конца, нам следова.ло бы попытаться доказать, что первый алгоритм в этом разделе, а именно - алгоритм I, также корректен. Ведь, в сущности, мы использовали алгорит.м I, чтобы показать корректность любого доказательства по индукции. Но если мы попытаемся доказать, что алгоритм I работает правильно, то попадем в затруднительное положение: мы не сможем сделать это, не воспользовавшись снова индукцией! Итак, получается замкнутый круг.

* Определение деления с Остатком в 9T0M(ii,V-lae п{)иведено в решении к упр. 12. - Прим. ред.

в последнее время любое свойство целых чисел принято доказывать с помощью индукции в ту или иную сторону. Ведь если мы обратимся к основным понятиям, то .увидим, что целые числа, в сущности, определяются по индукции. Поэтому можно принять в качестве аксиомы утверждение о том, что любое целое положительное число п либо равно 1, либо может быть получено, если взять 1 за исходное значение и последовательно прибавлять по единице. Этого достаточно, чтобы доказать правильность алгоритма I. Более подробно фундаментальные понятия, связанные с целыми числами, рассматриваются в статье Leon Henkin, On Mathematical Induction, AMM 67 (1960), 323-338.]

Таким образом, метод математической индукции глубоко связан с понятием числа. Первым европейцем, применившим в 1575 году метод математической индукции для получения строгих доказательств, был итальянский ученый Франческо Мауро-лико (Francesco MauroHco). В начале 17 века Пьер де Ферма (Pierre de Fermat) усовершенствовал этот метод; он называл его методом бесконечного спуска. Это понятие явно используется также в последних трудах Блеза Паскаля (Blaise Pascal) (1653). Термин "математическая индукция", видимо, был придуман А. Де Морганом (А. De Morgan) в начале 19 века. [См. АММ 24 (1917), 199-207; 25 (1918), 197-201; Arch. Hist. Exact Sci. 9 (1972), 1-21.] Более подробно метод математической индукции рассматривается в книге Д. Пойа (G. Polya) Induction and Analogy in Mathematics (Princeton, N. J.; Princeton University Press, 1954), Chapter 7 ("Математика и правдоподобные рассуждения"; т. 1, "Индукция и аналогия в математике" (М.: Изд-во иностр. лит., 1957), гл. 7).

Описанный выше метод доказательства алгоритмов с помощью утверждений, соответствующих стрелкам, и индукции, по существу, принадлежит Р. В. Флойду (R. W. Floyd). Он показал, что смысловое определение каждой операции в языке программирования можно сформулировать в виде логического правила. Это правило точно определяет, какие утверждения могут быть верны после вьшолнения операции, если известно, какие утверждения верны до ее выполнения. [См. "Assigning Meanings to Programs", Proc. Symp. Appl. Math., Amer. Math. Soc, 19 (1967), 19-32.] Аналогичные идеи были независимо высказаны Питером Науром (Peter Naur), BIT 6 (1966), 310-316, который называл утверждения, соответствующие стрелкам на блок-схемах, общими снимками (general snapshots). Необходимо уточнить, что понятие "инвариант" было введено Ч. Э. Р. Хоаром (С. А. R. Ноаге) (например, см. САСМ 14 (1971), 39-45). В более поздних публикациях считалось, что выгоднее изменить направление, заданное Флойдом, на противоположное, т. е. что нужно исходить из утверждения, которое должно выполняться после операции, и доказывать, что "самое слабое предусловие", которое должно иметь место до выполнения этой операции, на самом деле имеет место. Подобный подход позволяет разрабатывать новые алгоритмы, выбирая в качестве отправной точки характеристики желаемых выходных данных и двигаясь в обратном направлении (т. е. вверх по блок-схеме). При выполнении этого условия полученные алгоритмы обязательно будут корректными. [См. Е. W. Dijkstra, САСМ 18 (1975), 453-457; А Discipline of Programming (Prentice-Hail, 1976).]

На самом деле зачатки идеи индуктивных утвержденийчюявились в 1946 году, в то время, когда Г. Г. Голдстайн (Н. И. Goldstine) и Дж. фон Нейман (J. von Neumann) изобрели блок-схемы. Их первоначальные блок-схемы включали в себя "блоки с утверждениями", которые очень похожи на утверждения, показанные на рис. 4.