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