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