Что цикл является инвариантным?
Я читаю "Введение в Алгоритм", СБРАСЫВАЕТ. В главе 2 авторы упоминают "инварианты цикла". Что цикл является инвариантным?
3 ответа
Простыми словами, инвариант цикла — это некий предикат (условие), который справедлив для каждой итерации цикла. Например, давайте посмотрим на простой цикл for, который выглядит следующим образом:
int j = 9;
for(int i=0; i<10; i++)
j--;
В этом примере верно (для каждой итерации), что i + j == 9.Более слабый инвариант, который также верен, заключается в том, что
i >= 0 && i <= 10.
Инвариант в данном случае означает условие, которое должно быть истинным в определенной точке каждой итерации цикла.
В контрактном программировании инвариант — это условие, которое должно быть истинным (по контракту) до и после вызова любого открытого метода.
Мне нравится это очень простое определение: ( источник )
Инвариант цикла - это условие [среди переменных программы], которое обязательно выполняется непосредственно перед и сразу после каждого итерация цикла. (Обратите внимание, что это ничего не говорит о его истинности или ложности на этапе итерации.)
Сам по себе инвариант цикла мало что делает. Однако при наличии соответствующего инварианта его можно использовать для доказательства правильности алгоритма.Простой пример в CLRS, вероятно, связан с сортировкой. Например, пусть ваш инвариант цикла будет примерно таким: в начале цикла сортируются первые i записи этого массива. Если вы можете доказать, что это действительно инвариант цикла (т. Е. Что он сохраняется до и после каждой итерации цикла), вы можете использовать это, чтобы доказать правильность алгоритма сортировки: при завершении цикла инвариант цикла все еще выполняется. , а счетчик i - это длина массива. Следовательно, первые i записи сортируются, что означает сортировку всего массива.
Еще более простой пример: Инварианты циклов, корректность и вывод программ .
Я понимаю инвариант цикла как систематический формальный инструмент для размышлений о программах. Мы делаем единственное утверждение, на котором мы сосредотачиваемся на доказательстве истинности, и называем его инвариантом цикла. Это упорядочивает нашу логику. Хотя мы можем с таким же успехом неформально спорить о правильности некоторого алгоритма, использование инварианта цикла заставляет нас очень тщательно думать и обеспечивает непротиворечивость наших рассуждений.