Поиск программных инвариантов в виде полиномов

Abstract

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

Наведено рiшення проблеми пошуку iнварiантiв програм у виглядi полiномiальних залежностей методом верхньої апроксимацiї. Цей iтерацiйнний метод, вдало застосований для програм з абсолютно вiльними алгебрами i векторними просторами даних, адаптований для кiльця полiномiв. Множина iнварiантiв в цьому випадку являє собою iдеал кiльця полiномiв. Розв’язанi задачi про спiввiдношення i про перетин множин iнварiантiв з використанням базисiв Грьобнера при умовi невиродженостi оператора присвоювання.

A solution of the polynomial invariant generation problem for programs is presented. The iteration upper approximation method which was successfully applied to free algebras is adopted for a polynomial ring. The set of invariants is interpreted as an ideal over a polynomial ring. The solutions of the relationship and intersection problems are proposed. An intersection of Gröbner bases is applied to solve the intersection problem. The inverse obligatory is applied to solve the relationship problem.