AOP_Tom1 (1021736), страница 10
Текст из файла (страница 10)
Блок-схема алгоритма Е, дополненная примечаниями, которые доказывают правильность работы алгоритма. следует Аб. Поэтому нам достаточно доказать, что выполнение Аб до шага Е2 влечет за собой выполнение АЭ после этого шага. Заметим, что условие Н > 0 необходимо в Аб для того, чтобы операция Е2 имела смысл.) Нужно показать также, что из АЭ (при условии, что г = 0) следует А1, из АЭ (при условии, что г ~ 0) следует АЭ н т. д.
Все это доказывается очень просто. Если доказать утверждение (7) для каждою блока, то все примечания к стрелкам будут верны в любом случае выполнепля алгоритма. Теперь мы можем применить индукцию по числу шагов, т. е. по числу стрелок в блок-схеме. При прохождении первой стрелки (той, которая выходит из блока "Начало" ) утверждение А1 верно, поскольку мы всегда исходим из предположения, что входные значения удовлетворяют заданным условиям.
Таким образом, утверждение, которое соответствует первой стрелке, верно. Если утверждение, которое соответствуетп-й стрелке, верно, то согласно (7) утверждение, которое соответствует (и + 1)-й стрелке, тоже верно. Исходя из этою общего метода доказательство правильности заданного алгоритма, очевидно, сводится к нахождению правильных утверждений, соответствующих стрелкам блок-схемы.
Как только данное начальное препятствие будет преодолено, останется лишь рутинная работа, связанная с доказательством того, что каждое утверждение на входе в блок влечет за собой утверждение на'выходе из блока. В действительности после того как вы придумаете самые трудные из этих утверждений, найти все остальные уже не составит труда. Скажем, если'даны утверждения А1.
А1 и Аб, уже понятно, каккми должны быть утверждения АЭ, АЭ н А5. В нашем примере самых больших творческих усилий потребует доказательство утверждения Аб; все остальное, в принципе, должно получиться автоматически. Поэтому я и не пытался давать для алгоритмов, приведенных в книге, формальные доказательства с той степенью детализации, которая отражена на рис.
4. Вполне достаточно сформулировать только главные утверждения. Обычно онн приводятся либо в ходе обсуждения алгоритма, либо даются в скобках в тексте самого алгоритма. Этот подход к доказательству корректности алгоритма имеет и другой, еще более важный аспект: он отражает способ нашего понимания алгоритма. Если помните, в разделе 1.1 я предупреждал о том, чтобы вы не читали алгоритмы., как роман. Я рекомендую проверять работу алгоритма на примере одного-двух наборов входных данных. И это не случайно, так как пробная "прогонка" алгоритма поможет вам мысленно сформулировать утверждения, соответствующие стрелкам на блок-схеме.
Автор твердо убежден, что истинная уверенность в корректности алгоритма приходит только тогда, когда мысленно сформулированы все утверждения, приведенные на рнс. 4. Отсюда следуют важные психологические выводы, касающиеся передачи алгоритма от одного лица к другому. Речь идет о том, что, объясняя алгоритм кому-либо другому, всегда следует явно формулировать основные утверждения, которые трудно получить автоматически. Например, в случае алгоритма Е нужно обязательно упомянуть утверждение Аб.
Но бдительный читатель, конечно, заметил зияющую брешь в нашем последнем доказательстве алгоритма Е. Из него нигде не следует, что алгоритм обладает свойством конечности, т. е. рано илн поздно его выполнение завершится. ЬАы доказали только, что если алгоритм конечен, то он дает правильный результат! (Например, заметим, что алгоритм Е по-прежнему имеет смысл, если его переменные т, и, с, с1 н г принимают значения типа и + н х/2, где и и н — целые числа*. Переменные 4, а, Ь, а', Ь' должны по-прежнему принимать целые значения, Если, например, на вход подать значения пэ = 12-6 э/2 и и = 20 — 10 т/2, то на выходе будет получен "наибольший общий делитель" с1 = 4 — 2 ъ'2 и коэффициенты а = +2, Ь = -1.
Даже при таком расширении исходных предположений доказательства утверждений от А1 до Аб остаются в силе. Следовательно, на любом этапе выполнения этой процедуры все утверждения верны. Но если начать со значений пэ = 1 и и = э/2. то вычисления никогда не закончатся (см. упр.
12). Следовательно, из доказательства утверждений А1-А6 еще не следует, что алгоритм конечен.) Доказательства конечности алгоритмов обычно проводят отдельно. Но в упр. 13 показано, что во многих важных случаях приведенный выше метод можно обобщить таким образом, чтобы включить доказательство конечности в виде промежуточного результата. Итак, мы уже дважды доказали правильность алгоритма Е. Чтобы быть последовательными до конца, нам следовало бы попытаться доказать, что первый алгоритм в этом разделе, а именно — алгоритм 1, также корректен.
Ведь, в сущности, мы использовали алгоритм 1,чтобы показать корректность любого доказательства по индукции. Но если мы попытаемся доказать, что алгоритм 1 работает правильно, то попадем в затруднительное положение: мы не сможем сделать это, не воспользовавшись снова нндукцией! Итак, получается замкнутый круг. * Определение делении с Остатком в этом'Слуэае приведено в решении к упр.
ПЬ -- Лриээ ред. В последнее время любое свойство целых чисел принято доказывать с помощью индукции в ту или иную сторону. Ведь если мы обратимся к основным понятиям, то увидим, что целые числа, в сущности, определяюгися по индукции. Поэтому можно принять в качестве аксиомы утверждение о том, что любое целое положительное число п либо равно 1, либо может быть получено, если взять 1 за исходное значение и последовательно прибавлять по единице.
Этого достаточно, чтобы доказать правильность алгоритма 1. [Более подробно фундаментальные понятия, связанные с целыми числами, рассматриваются в статье Ьеоп НепЫп, Оп МагЬешабса! 1пг!пс1юп, АММ 67 (1960), 323-338.) Таким образом, метод математической ицлукции глубоко связан с понятием числа.
Первым европейцем, применившим в 1575 году метод математической индукции для получения строгих доказательств, был итальянский ученый Франческо Мауро- лико (Ргапсевсо Машо!ко). В начале 17 века Пьер де Ферма (Р!егге с!е Регша1) усовершенствовал этот метод; он называл его методом бесконечного спуска. Это понятие явно используется также в последних трудах Блеза Паскаля (В!а!эе Рааса!) (1653). Термин "математическая индукция", видимо, был придуман А. Де Морганом (А.
Пе Могйап) в начале 19 века. [См. АММ 24 (1917), 199 — 207; 25 (1918), 197- 201; Агсй. НЫ. Ехас! Яск'. 9 (1972), 1-21.] Более подробно метод математической индукции рассматривается в книге Д. Пойа (С. Рб!уа) 7пс(ис1!оп ало Апа(ойу 1и Магйешас1сэ (РПпсесоп, 5!. Лх РНпсесоп Нп!гегв!1у Ргеээ, 1954), СЬарсег 7 (" Математика и правдоподобные рассуисдения"; т. 1, "Индукция и аналогия в математике" (Мс Изд-во иностр. лиг., 1957), гл.
7). Описанный выше метод доказательства алгоритмов с помощью утверждений, соответствующих стрелкам, и индукции, по существу, принадлежит Р. В. Флойду (Н. %. Р!оуб). Он показал, что смысловое определение каждой операции в языке программирования можно сформулировать в виде логического правила. Это правило точно определяет, какие утверждения могут быть верны после выполнения операции, если известно, какие утверждения верны до ее выполнения.
[См. "Лээ!8п!п8 Меап!пйэ со Рго8гашэ", Ргос. Яушр. Арр1. Ма1Ь., Агпег. Маг!ь Бос., 19 (1967), 19 — 32.! Аналогичные идеи были независимо высказаны Питером Науром (Ре1ег Хаиг), В1Т 6 (1966), 310 — 316, который называл утверждения, соответствующие стрелкам на блоксхемах, общими снимками (8епега! впарэЬо1э). Необходимо уточнить, что понятие "инвариант" было введено Ч.
Э. Р. Хоаром (С. А. К. Ноаге) (например, см. САСМ 14 (1971), 39-45). В более поздних публикациях считалось, что выгоднее изменить направление, заданное Флойдом, на противоположное, т. е, что нужно исходить из утверждения, которое должно выполняться после операции, и доказывать, что "самое слабое предусловие", которое должно иметь место да выполнения этой операции, на самом деле имеет место. Подобный подход позволяет разрабатывать новые алгоритмы, выбирая в качестве отправной точки характеристикк желаемых выходных данных и двигаясь в обратном направлении (т. е.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
