loop invariant

А что такое инвариант, знаешь?

Не обращайте на терминологию внимания. Можно писать хорошие программы, зная лишь минимальный набор терминов.

Только из вики

Вот почему голосования за бан открытого. Ты и Alv были бы первыми. Хоть в одной бы теме ответил что-нибудь нормальное

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

Выявление такого условия может использоваться, например, для доказательства крооектности алгоритма по индукции. Если я правильно понял, то в случае сортировки вставкое это условие звучит как «первые n элементов идут в порядке возрастания». Перед первой итерацией, очевидно, первый один элемент идёт в пордке возрастания (а как ещё-то?). Далее доказывается, если перед n-й итерацией первые n элементов были в порядке возрастания, то после этой итерации первые n+1 элеентов будут в порядке возрастания. Следовательно, после последней итерации весь массив будет упорядочен.

Вот что является инвариантом цикла в этом примере?

 while(x<10) x:=x+1; 

Какое выражение остается истинным в течение каждой итерации тела цикла?

Инвариант цикла - это выражение, которое на протяжении всех итераций цикла остается истиным и подтверждает корректность алгоритма. Так? :)

подтверждает корректность алгоритма

Nope. Посредством инвариантов можно подтвердить корректность алгоритма, а можно и не подтвердить.

s/подтверждает/помогает доказать/ ?

Часто помогает доказать – так будет совсем точно.

Спасибо всем! Я вроде понял.

> Вот почему голосования за бан открытого. Ты и Alv были бы первыми.

Первым был бы анонимус;-)