> -- Rifat писал(а):
> Многие наверно слышали про инвариант цикла. Кое-кто может быть слышал про инвариант класса в языке Eiffel. Но также выделяют еще инвариант рекурсии, инвариант итератора и инвариант данных.Инварианты класса и итератора - это, пожалуй, частные случаи инварианта данных. Инвариант данных - это часть инварианта всех процедур, которые используют эти данные.

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

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

> -- Цитата:
> Кто как считает необходимы ли все эти инварианты?
Считаю, что они нужны в понятиях языка, чтобы иметь возможность доказывать корректность программ автоматическими средствами, не прибегая к трюкам, наподобии спец-комментариев. Но подойти к внедрению нужно осторожно, потому что легко доулучшаться до невозможности легко программировать.