Главная » Java, Структуры данных и алгоритмы » Индукция и инварианты цикла

0

В большинстве случаев в утверждениях о времени выполнения программы или используемом пространстве применяется целочисленный параметр п (обозначающий «размеры» задачи). Более того, подобные утверждения равносильны, как правило, утверждению типа «q(n) истинно для всех п> 1». Так как данное утверждение относится к бесконечному множеству чисел, невозможно провести исчерпывающее прямое доказательство.

Индукция

Зачастую приводимые выше утверждения можно доказать с помощью метода индукции. Данный метод основан на том, что для любого п> 1 существует конечная последовательность действий, которая начинается с чего-то заведомо истинного и, в конечном итоге, приводит к доказательству того, что q(n) истинно. Таким образом, доказательство с помощью индукции начинается с утверждения, что q(n) истинно при п = 1 (и, возможно, некоторых других значениях п — 2, 3, …, к, где к — некоторая константа). Далее доказывается, что следующий «шаг» индукции также является истинным для п> к, то есть показываем, что «если q(i) истинно для i < п, то q(n) — истинно». Объединение этих двух этапов и составляет метод доказательства с помощью индукции.

Пример 3.5. Рассмотрим последовательность Фибоначчи:

F( 1) = 1, F(2) = 2, F(n) = F(n – 1) + F{n – 2), где n > 2.

Докажем, что F(n) < 2".

Доказательство: доказательство истинности утверждения проведем с помощью метода индукции.

Исходные положения: (т < 2). F( 1) =1 < 2 = 21, F(2) = 2 < 4 = 22.

Шаг индукции: (п>2). Предположим, что приведенное утверждение истинно для п’ < п. Рассмотрим F(n). Так как

п > 2, F(n) = F(n -1) + F(n - 2).

Более того, так как я-1<яия-2<я, можно сделать индуктивное допущение (иногдатоворят — «индуктивную гипотезу») о том, что

Доказательство завершено.

Иногда в недоумение может привести требование доказать истинность некоторого утверждения для всех п > 1. Не следует, однако, забывать о преимуществе метода индукции, показывающего, что для любого п существует конечная последовательность утверждений, которая начинается с некоторого истинного утверждения и приводит к выводу об истинности для всех п. В целом метод индукции предлагает формулу построения последовательности прямых доказательств.

Инварианты цикла

Заключительным методом доказательства, рассматриваемого в данном разделе, является использование инварианта цикла, который применяется при анализе и проверке циклов.

Для доказательства того, что некое утверждение S в отношении цикла истинно, представим ? в виде совокупности составляющих его утверждений So, S\9 Sk, где:

1.     Исходное утверждение -So верно перед началом выполнения цикла.

2.     Если5/_1 верно перед началом итерации /, то можно показать, что

Si будет верно и после завершения итерации /.

3.     Заключительное утверждение S^ подтверждает, что утверждение S,

доказательство которого проводится, истинно.

Прием использования инварианта цикла уже применялся в разделе 3.2 (при доказательстве правильности алгоритма аггауМах). Приведем еще один пример использования этого метода для доказательства правильности алгбритма arrayFind, представленного во фрагменте кода 3.3, который осуществляет поиск элемента х в массиве А.

Алгоритм arrayFinf (х,А):

Input: элемент х и массив А, содержащий п элементов.

Output: индекс соответствующий элементу х = A[i] или равный —1, если ни один элемент массива А не равен х.

Abstract: данный метод осуществляет поиск в массиве А с помощью обычного цикла while.

/ 0

while i п do if х = А[/] then

return / else

/ / + 1 return -1

Фрагмент кода 3.3. Алгоритм arrayFind

Для доказательства верности алгоритма arrayFind применим инвариант цикла. Индуктивно определим последовательность утверждений Si, которые постепенно подтверждают его правильность. В частности, перед итерацией / утверждается, что следующее выражение истинно:

Si: х не равен ни одному из первых / элементов массива А.

Это утверждение истинно перед началом первой итерации цикла, так как среди первых 0 элементов массива А нет элементов (подобное очевидное утверждение называется пустым). Во время итерации / программа сравнивает элемент х с элементом A[i] и возвращает индекс /, если их значения равны, что доказывает правильность алгоритма, и его выполнение прекращается. Если значения элемента х и элемента A[i] не равны, это означает, что обнаружен еще один элемент, не равный х; индекс / увеличивается в этом случае на 1. Таким образом, утверждение 5/ будет истинно для нового значения /, то есть остается верным перед началом новой итерации. Если выполнение цикла while прекращается, и программа не находит никакого значения индекса массива А, то в этом случае должно быть истинно, что / = п. Другими словами, Sn истинно, массив А не содержит элементов, равных х. В этом случае алгоритм выполняется правильно, возвращая, как и требовалось, значение —1.

Источник: Гудрич М.Т. Г93 Структуры данных и алгоритмы в Java / М.Т. Гудрич, Р. Тамассия; Пер. с англ. A.M. Чернухо. — Мн.: Новое знание, 2003. — 671 е.: ил.

По теме:

  • Комментарии