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

Добрый день
Помогите простыми словами или же более менее формально, структурировано определить понятие инварианта цикла.
Потребность в этом возникла при прорешивании упражнений из "Алгоритмы. Построение и анализ" Т.Кормена.
Не могу уловить, что именно от меня требуется при задании "сформулируйте инвариант".

В основном, все источники говорят о том, что это логическое выражение, хотя если взять книгу того же Кормена, но попроще "Вводный курс", то у него все сводится к логическим рассуждениям - привожу скриншот. Он так упростил это понятие, что заменил "выражение" на "утверждение", или же термин "утверждение" тоже подходит?
Есть ли источники с понятными формулировками и примерами.

vi0,

vi0,

vi0,

Это набор из трёх правил. Они необходимы (но не достаточны) для определения правильности логики алгоритма.

Такой формальный подход порой позволяет выловить логическую ошибку, когда "на глазок" кажется, что всё правильно.

Попробуй сформулировать эти правила для какой-либо из простых сортировок - выбором или вставками.
Для них это дело смотрится логичнее.

vi0,

если на пальцах, то это адаптация программистами для своих целей метода математической индукции )

vi0, пример инварианта - проверка выхода за границы массива. В некоторых ЯП и runtime этот ивариант - встроен.

Еще пример. На некоторых собесах задают задачу - проверить корректность вложенных скобок.

Пример корректных

(((( () () ))))

Пример некорректных

())

Можно тут взять следующий ивариант. Если скобка открылась - то считаем +1 к некой переменной.
Если закрылась - то считаем -1. Если в теле цикла мы вышли ниже нуля - то ошибка вложенных скобок.

Ивариантом в нашем случае является НЕ-ОТРИЦАТЕЛЬНОСТЬ счетчика скобок.

+В конце можно проверить на ноль. Но это уже пост-вариант.

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

Ну и модульные тесты и еще раз тесты. Утверждения (asserts). Контракты.

mayton

Можно тут взять следующий ивариант. Если скобка открылась - то считаем +1 к некой переменной. Если закрылась - то считаем -1. Если в теле цикла мы вышли ниже нуля - то ошибка вложенных скобок. Ивариантом в нашем случае является НЕ-ОТРИЦАТЕЛЬНОСТЬ счетчика скобок. +В конце можно проверить на ноль. Но это уже пост-вариант.vi0, пример инварианта - проверка выхода за границы массива. В некоторых ЯП и runtime этот ивариант - встроен. Еще пример. На некоторых собесах задают задачу - проверить корректность вложенных скобок. Пример корректных (((( () () )))) Пример некорректных ()) Инварианты очень леко толкать в математике. Берете просто любую формулу и как только видите квадратный корень - то сразу говорите что под корнем - не отрицательное. Это инвариант. Ну и модульные тесты и еще раз тесты. Утверждения (asserts). Контракты.

Это неверный ответ.

Инварианты в программировании используются для формального доказательства корректности алгоритмов.

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

В примере со скобками инвариант цикла - это текущая накопленная сумма, плюс алгебраическая сумма оставшихся скобок.

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

А контрольная точка по вашему где должна стоять? В теле цикла может?

mayton

Aleksandr Sharahov В общем случае инвариантом называется выражение, которое всегда принимает одинаковое значение в некоторых "контрольных" точках алгоритма (например, на входе в цикл, в начале каждой итерации и на выходе). В примере со скобками инвариант цикла - это текущая накопленная сумма, плюс алгебраическая сумма оставшихся скобок. А контрольная точка по вашему где должна стоять? В теле цикла может?

Да. Контрольные точки доказывающий расставляет по своему усмотрению, как ему удобно.
Цикла вообще может не быть, а например лапша из goto.

Aleksandr Sharahov
mayton пропущено... А контрольная точка по вашему где должна стоять? В теле цикла может? Да. Контрольные точки доказывающий расставляет по своему усмотрению, как ему удобно. Цикла вообще может не быть, а например лапша из goto.

Но в таком случае почему сумма скобок - не инвариант?