Что такое инвариант цикла?

Question

Я читаю "Введение в алгоритм" от CLRS. В главе 2 авторы упоминают «петлевые инварианты». Что такое инвариант цикла?

Answer 1

Проще говоря, инвариант цикла - это некоторый предикат (условие), который выполняется для каждой итерации цикла.Например, давайте рассмотрим простой цикл for, который выглядит следующим образом:

int j = 9;
for(int i=0; i<10; i++)  
  j--;

В этом примере верно (для каждой итерации), что i + j == 9.Более слабый инвариант, который также верен, состоит в том, что i >= 0 && i <= 10.

Answer 2

Мне нравится это очень простое определение: ( источник )

Инвариант цикла - это условие [среди переменных программы], которое обязательно истинно непосредственно перед и сразу после каждой итерации цикла. (Обратите внимание, что это ничего не говорит о его истинности или ложности в процессе итерации.)

Сам по себе инвариант цикла мало что делает. Однако, учитывая соответствующий инвариант, он может быть использован для доказательства правильности алгоритма. Простой пример в CLRS, вероятно, связан с сортировкой. Например, пусть ваш инвариант цикла будет выглядеть примерно так: в начале цикла сортируются первые i записи этого массива. Если вы можете доказать, что это действительно инвариант цикла (т. Е. Что он сохраняется до и после каждой итерации цикла), вы можете использовать это для доказательства правильности алгоритма сортировки: при завершении цикла инвариант цикла все еще выполняется , а счетчик i - длина массива. Следовательно, первые i записи отсортированы, что означает, что весь массив отсортирован.

Еще более простой пример: Циклы инвариантов, корректность и вывод программы .

То, как я понимаю инвариант цикла, - это систематический, формальный инструмент для рассуждения о программах. Мы делаем единственное утверждение, которое сосредотачиваемся на доказательстве истинности, и называем это циклическим инвариантом Это организует нашу логику. Хотя мы также можем неформально спорить о правильности какого-либо алгоритма, использование инварианта цикла заставляет нас очень тщательно мыслить и гарантирует, что наши рассуждения непроницаемы.

Answer 3

Есть одна вещь, которую многие люди не осознают сразу, имея дело с циклами и инвариантами.Они путаются между инвариантом цикла и условным циклом (условием, управляющим завершением цикла).

Как отмечают люди, инвариант цикла должен быть истинным

1. до начала цикла
2. перед каждой итерацией цикла
3. послецикл завершается

(хотя он может временно быть ложным в теле цикла). С другой стороны, условный цикл должен быть ложным после завершения цикла, иначе цикл никогда не завершится.

Таким образом, инвариант цикла и условный цикл должны быть разными условиями.

Хороший пример инварианта сложного цикла - бинарный поиск.

bsearch(type A[], type a) {
start = 1, end = length(A)

    while ( start <= end ) {
        mid = floor(start + end / 2)

        if ( A[mid] == a ) return mid
        if ( A[mid] > a ) end = mid - 1
        if ( A[mid] < a ) start = mid + 1

    }
    return -1

}

Таким образом, условный цикл кажется довольно прямым - когда начало> конец цикла завершается.Но почему цикл правильный?Что такое инвариант цикла, который доказывает его правильность?

Инвариант - это логическое утверждение:

if ( A[mid] == a ) then ( start <= mid <= end )

Это утверждение является логической тавтологией - оно всегда верно в контекстеконкретный цикл / алгоритм, который мы пытаемся доказать .И он предоставляет полезную информацию о правильности цикла после его завершения.

Если мы вернемся, потому что нашли элемент в массиве, то утверждение явно верно, так как если A[mid] == a, то a находится вмассив и mid должны находиться между началом и концом.И если цикл завершается из-за start > end, то не может быть такого числа, чтобы start <= mid и mid <= end, и поэтому мы знаем, что утверждение A[mid] == a должно быть ложным.Однако в результате общее логическое утверждение все еще верно в нулевом смысле.(В логике утверждение if (false) затем (что-то) всегда истинно.)

А что насчет того, что я сказал о условном цикле, который обязательно должен быть ложным, когда цикл завершается?Похоже, когда элемент найден в массиве, тогда условие цикла истина, когда цикл завершается !?На самом деле это не так, потому что условный цикл подразумевается действительно while ( A[mid] != a && start <= end ), но мы сокращаем реальный тест, поскольку подразумевается первая часть.Это условие явно ложно после цикла независимо от того, как цикл завершается.

Answer 4

Предыдущие ответы очень хорошо определили инвариант цикла.

Ниже описано, как авторы CLRS использовали инвариант цикла для доказательства правильности сортировки вставок.

Алгоритм сортировки вставками (как указано в Книге):

INSERTION-SORT(A)
    for j ← 2 to length[A]
        do key ← A[j]
        // Insert A[j] into the sorted sequence A[1..j-1].
        i ← j - 1
        while i > 0 and A[i] > key
            do A[i + 1] ← A[i]
            i ← i - 1
        A[i + 1] ← key

Инвариант цикла в этом случае: Подмассив [1 - j-1] всегда сортируется.

Теперь давайте проверим это и докажем, что алгоритм верен.

Инициализация : до первой итерации j = 2. Таким образом, под-массив [1: 1] - это массив для тестирования. Поскольку у него есть только один элемент, он сортируется. Таким образом, инвариант выполняется.

Обслуживание : Это можно легко проверить, проверив инвариант после каждой итерации. В этом случае оно выполняется.

Завершение : На этом шаге мы докажем правильность алгоритма.

Когда цикл заканчивается, значение j = n + 1. Снова цикл-инвариант выполняется. Это означает, что под-массив [от 1 до n] должен быть отсортирован.

Это то, что мы хотим сделать с нашим алгоритмом. Таким образом, наш алгоритм правильный.

Answer 5

Помимо всех хороших ответов, я думаю, отличный пример из Джеффа Эдмондса "Как думать об алгоритмах" может очень хорошо проиллюстрировать концепцию:

ПРИМЕР 1.2.1 «Алгоритм Find-Max с двумя пальцами»

1) Технические характеристики: Входной экземпляр состоит из списка L (1..n) элементов.Выход состоит из индекса i, такого что L (i) имеет максимальное значение.Если существует несколько записей с одним и тем же значением, возвращается любая из них.

2) Основные шаги: вы выбираете метод двумя пальцами.Ваш правый палец перемещается по списку.

3) Мера прогресса: мера прогресса заключается в том, насколько далеко вдоль списка находится ваш правый палец.

4) Инвариант цикла: Инвариант цикла гласит, что ваш левый палец указывает на одну из самых больших записей, с которыми когда-либо сталкивался ваш правый палец.

5) Основные шаги: На каждой итерации вы перемещаете правый палец вниз на одну запись всписок.Если ваш правый палец сейчас указывает на запись, которая больше, чем запись на левом пальце, то переместите ваш левый палец, чтобы быть правым пальцем.

6) Продвигайтесь: вы делаете успехи, потому что ваш правый палец движетсяодна запись.

7) Ведение инварианта цикла: Вы знаете, что инвариант цикла поддерживается следующим образом.Для каждого шага новый элемент левого пальца - Макс (старый элемент левого пальца, новый элемент).По инварианту цикла это Max (Max (более короткий список), новый элемент).Математически это Макс (более длинный список).

8) Установление инварианта цикла: Вы изначально устанавливаете инвариант цикла, указывая двумя пальцами на первый элемент.

9) Условие выхода: вы закончили, когда ваш правый палец закончил обход списка.

10) Окончание: В конце мы знаем, что проблема решается следующим образом.По условию выхода ваш правый палец встретил все записи.По инварианту цикла ваш левый палец указывает на максимум из них.Верните эту запись.

11) Завершение и время выполнения. Требуемое время несколько раз умножено на длину списка.

12) Особые случаи: проверьте, что происходит при наличии нескольких записей сто же значение или когда n = 0 или n = 1.

13) Подробности кодирования и реализации: ...

14) Формальное доказательство: правильность алгоритма следует из вышеприведенных шагов.

Answer 6

Следует отметить, что инвариант цикла может помочь в разработке итерационных алгоритмов, когда рассматривается утверждение, выражающее важные отношения между переменными, которые должны быть истинными в начале каждой итерации и когда цикл завершается. Если это имеет место, вычисления находятся на пути к эффективности. Если false, алгоритм потерпел неудачу.

Answer 7

Инвариант в этом случае означает условие, которое должно быть истинным в определенный момент в каждой итерации цикла.

В программировании контракта инвариант - это условие, которое должно быть истинным (по контракту) до и после любогоВызывается публичный метод.

Answer 8

Значение инварианта никогда не меняется

Здесь инвариант цикла означает, что «изменение, которое происходит с переменной в цикле (увеличение или уменьшение), не изменяет условие цикла, т. Е. Условие удовлетворяет», так что концепция инварианта цикла пришла

Answer 9

Свойство инварианта цикла - это условие, которое выполняется для каждого шага выполнения циклов (т. Е. Для циклов, циклов и т. Д.)

Это необходимо для проверки циклического инварианта, когда можночтобы показать, что алгоритм выполняется правильно, если на каждом этапе его выполнения выполняется свойство инварианта цикла.

Чтобы алгоритм был корректным, инвариант цикла должен иметь значение:

Инициализация (начало)

Техническое обслуживание (каждый шаг после)

Завершение (когда оно закончено)

Этоиспользуется для оценки множества вещей, но лучший пример - жадные алгоритмы для взвешенного обхода графа.Чтобы жадный алгоритм давал оптимальное решение (путь через граф), он должен достичь соединения всех узлов на пути с наименьшим возможным весом.

Таким образом, свойство инварианта цикла состоит в том, что выбранный путь имеет наименьшийвес.В начало мы не добавили ребер, поэтому это свойство имеет значение true (в данном случае это не false).В каждый шаг мы следуем по краю наименьшего веса (жадный шаг), поэтому снова мы выбираем путь с наименьшим весом.В конце мы нашли наименьший взвешенный путь, поэтому наше свойство также верно.

Если алгоритм этого не делает, мы можем доказать, что он не оптимален.

Answer 10

Извините, у меня нет разрешения на комментарии.

@ Томас Петричек, как вы упомянули

Более слабый инвариант, который также верен, состоит в том, что я>= 0 && i <10 (потому что это условие продолжения!) "</p>

Как это инвариант цикла?

Надеюсь, я не ошибаюсь, насколько я понимаю ^[1] , инвариант цикла будет истинным в начале цикла (инициализация), он будет истинным до и после каждой итерации (обслуживание), а также будет истинным после завершенияцикл (Завершение) . Но после последней итерации i становится равным 10. Итак, условие i> = 0 && i <10 становится ложным и завершает цикл. Это нарушает третье свойство (Завершение) инварианта цикла. </p>

[1] http://www.win.tue.nl/~kbuchin/teaching/JBP030/notebooks/loop-invariants.html