УДК 004.421.6

Анализ линейно определенных итеративных циклов

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

УДК 004.421.6

Аналіз лінійно визначених ітеративних циклів

Розглянуто новий метод доведення інваріантності системи лінійних нерівностей, а також завершуваності лінійно визначених ітеративних циклів імперативних програм. Тіло циклу — лінійний оператор, що перетворює вектор змінних програми. Метод враховує передумову циклу, а також умову повторення циклу у вигляді сукупності систем лінійних нерівностей. Метод ґрунтується на побудові та аналізі спектра цього лінійного оператора та обчисленні кількості ітерацій циклу, після виконання яких інваріантність або забезпечується, або спростовується. Теоретичний матеріал роботи проілюстровано прикладами. Іл.: 2. Бібліогр.: 23 назви.

UDC 004.421.6

Analysis of linear definite iterative loops

The paper presents a new method to prove the invariance of the system of linear inequalities and termination of linear definite iterative loops for imperative programs. Loop body is a linear operator that transforms the vector of program variables. The method takes into account the loop precondition, as well as the condition of loop repetition in the form of a set of systems of linear inequalities. The method is based on the construction and analysis of the spectrum of the linear operator and calculating the number of loop iterations after which the invariance is either provided or disproved. The theoretical material is illustrated by examples. Figs: 2. Refs: 23 titles.

Ключевые слова:

статический анализ программ, линейные инварианты циклов, инвариантные системы линейных неравенств.


ПОЛНЫЙ ТЕКСТ

Об авторе(ах):

Львов Михаил Сергеевич, доктор физ.-мат. наук, профессор, заведующий кафедрой Херсонского государственного университета,
e-mail: lvov@ksu.ks.ua