Поиск программных инвариантов в виде полиномов
Представлено решение проблемы поиска инвариантов программ в виде полиномиальных
 зависимостей методом верхней аппроксимации. Этот итерационный метод, с успехом примененный к программам над абсолютно свободными алгебрами и векторными пространствами данных, адаптирован для кольца полиномов. Мн...
Saved in:
| Published in: | Доповіді НАН України |
|---|---|
| Date: | 2013 |
| Main Author: | |
| Format: | Article |
| Language: | Russian |
| Published: |
Видавничий дім "Академперіодика" НАН України
2013
|
| Subjects: | |
| Online Access: | https://nasplib.isofts.kiev.ua/handle/123456789/85891 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| Journal Title: | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| Cite this: | Поиск программных инвариантов в виде полиномов / А.Н. Максимец // Доповiдi Нацiональної академiї наук України. — 2013. — № 9. — С. 44–50. — Бібліогр.: 12 назв. — рос. |
Institution
Digital Library of Periodicals of National Academy of Sciences of Ukraine| _version_ | 1860135780809179136 |
|---|---|
| author | Максимец, А.Н. |
| author_facet | Максимец, А.Н. |
| citation_txt | Поиск программных инвариантов в виде полиномов / А.Н. Максимец // Доповiдi Нацiональної академiї наук України. — 2013. — № 9. — С. 44–50. — Бібліогр.: 12 назв. — рос. |
| collection | DSpace DC |
| container_title | Доповіді НАН України |
| description | Представлено решение проблемы поиска инвариантов программ в виде полиномиальных
зависимостей методом верхней аппроксимации. Этот итерационный метод, с успехом примененный к программам над абсолютно свободными алгебрами и векторными пространствами данных, адаптирован для кольца полиномов. Множество инвариантов
в этом случае представляется в виде идеала кольца полиномов. Решены задачи о соотношениях и о пересечении множеств инвариантов с использованием базисов Гребнера при условии невырожденности оператора присваивания.
Наведено р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.
|
| first_indexed | 2025-12-07T17:46:54Z |
| format | Article |
| fulltext |
УДК 519.6:539.3
А.Н. Максимец
Поиск программных инвариантов в виде полиномов
(Представлено членом-корреспондентом НАН Украины С.И. Ляшко)
Представлено решение проблемы поиска инвариантов программ в виде полиномиальных
зависимостей методом верхней аппроксимации. Этот итерационный метод, с успе-
хом примененный к программам над абсолютно свободными алгебрами и векторными
пространствами данных, адаптирован для кольца полиномов. Множество инвариантов
в этом случае представляется в виде идеала кольца полиномов. Решены задачи о соот-
ношениях и о пересечении множеств инвариантов с использованием базисов Гребнера
при условии невырожденности оператора присваивания.
1. После прорыва в теории верификации, связанного с появлением теории индуктивных
утверждений Флойда–Хоара–Дейкстры [1] в 70-х гг. (Вегбрейт, 1974, 1975; Герман и Вег-
брейт, 1975; Кац и Манна, 1976; Куазот и Куазот, 1976; Сузуки и Ишихата, 1977; Дер-
шовицем и Манна, 1978), наступил тихий период в этой области. Оживление последова-
ло с изучением средств автоматического доказательства теорем (САДТ) и верификации
моделей программ вместо исходных программ. Все перечисленные подходы формальных
доказательств свойств программы используют утверждения, которые истинны во время
выполнения программы в качестве входных данных. Проблема поиска таких увтерждений
(инвариантов) остается особенно актуальной и по сей день.
Исследования в этой области велись и в СССР, особенно в Киеве и Новосибирске, в 70-х
и 80-х гг. прошлого столетия. В результате были разработаны эффективные алгоритмы
генерации инвариантов для программ. Проводились исследования следующих алгебр дан-
ных: абсолютно свободная алгебра данных [4, 12], группы, полугруппы, абелевы группы
и абелевы полугруппы, векторное пространство [3], кольцо многочленов [9, 10].
Программа представлена в виде U–Y -схемы на алгебре многочленов. В данной работе
итерационные алгоритмы, удачно примененные для абсолютно свободных алгебр и вектор-
ных пространств, адаптипрованы для полиномиальных пространств [7].
Инвариант U–Y -схемы в состоянии — это утверждение, которое верно для любого дос-
тижимого состояния памяти U–Y -схемы. Термин “состояние” далее обозначает состояние
(узел) U–Y -схемы. Рассматриваемый подход строит базис инвариантых соотношений для
каждого состояния программы, учитывая переданные соотношения на вход U–Y -схемы.
Эта работа была вызвана схожими работами по генерации инвариантов в виде полиноми-
номов с использованием базисов Гребнера (Мюллер-Олм и Зайдель, 2004; Санкаранараянан,
2004; Родригес-Карбонелл и Капур, 2007). Рассмотренный итерационный метод позволяет
генерировать более широкое множество инвариантов, что аргументирует его применение.
2. Обозначения. Пусть A — U–Y -схема над памятью [5] и R = {r1, . . . , rm} — мно-
жество переменных, которое определено на алгебре данных (D,Ω); K(Ω, Eq) — класс ал-
гебр, который включает в себя алгебру (D,Ω) [2]. Рассмотрим кольцо многочленов (D,Ω)
и алгебру термов T (Ω, R) на R из класса K(Ω, Eq).
© А.Н. Максимец, 2013
44 ISSN 1025-6415 Reports of the National Academy of Sciences of Ukraine, 2013, №9
Определение 1 (алгебраическое соотношение). Алгебраическим соотношением Ψ на-
зывается соотношение вида
∧
i
pi(r1, . . . , rm) = 0, где каждый pi ∈ ℜ[r1, . . . , rm]. Степень
соотношения — это максимальная степень среди степеней многочленов, которые состав-
ляют соотношение.
Определение 2 (идеал). Множество I ⊆ ℜ[r1, . . . , rn] называется идеалом тогда и толь-
ко, когда:
1) 0 ∈ I;
2) если p1, p2 ∈ I, то p1 + p2 ∈ I;
3) если p1 ∈ I и p2 ∈ ℜ[r1, . . . , rn], то p1p2 ∈ ℜ[r1, . . . , rn].
Идеалом, порожденным множеством многочленов N (обозначается ((N))), называется
минимальный идеал, содержащий N . Это равносильно ((N)) = {g1p1 + · · · + gmpm | g1, . . .,
. . . , gm ∈ R[r1, . . . , rn], p1, . . . , pm ∈ P}. Идеал I считается конечно порожденным, если су-
ществует конечное множество N , так, что I = ((N)). Знаменитая теорема Гильберта утвер-
ждает, что все идеалы в ℜ[r1, . . . , rn] являются конечнопорожденными. В результате ал-
гебраические соотношения можно рассматривать как порождающие идеалы и наоборот.
Любой идеал определяет многообразие, которое является множеством общих нулей всех
полиномов, которые он содержит.
Определение 3 (пересечение идеалов). Множество K является пересечением идеалов
I = {f1, . . . , fl} и J = {g1, . . . , gm}, если
K =
{
s(r1, . . . , rn) | s(r1, . . . , rn) =
l
∑
i=1
pifi =
m
∑
j=1
qjgj , p1, . . . , pl, q1, . . . , qm ∈
∈ ℜ[r1, . . . , rn]
}
.
Теорема 1 (пересечение идеалов). Пусть I и J — идеалы в R[r1, . . . , rn]
I
⋂
J = (tI + (1− t)J)
⋂
ℜ[r1, . . . , rn], (1)
где t ∈ R — новая введенная переменная [6].
Доказательство. Заметим, что tI + (1 − t)J является идеалом в ℜ[r1, . . . , rn, t]. Для
доказательства истинности равенства мы докажем включение в обе стороны.
Пусть f ∈ I
⋂
J . Поскольку f ∈ I, то tf ∈ tI. Аналогично f ∈ J следует (1−t)f ∈ (1−t)J .
Получаем, что f = tf + (1 − t)f ∈ tI + (1 − t)J и I, J ⊂ ℜ[r1, . . . , rn].
Чтобы доказать включение в обратную сторону, допустим f ∈(tI+(1−t)J)
⋂
ℜ[r1, . . . , rn].
Тогда f(r) = g(r, t) + h(r, t), где g(r, t) ∈ tI и h(r, t) ∈ (1 − t)J . Сначала рассмотрим ва-
риант t = 0. Исходя из того, что каждый элемент из tI умножается на t, g(r, 0) = 0,
f(r) = h(r, 0) и f(r) ∈ J . Рассмотрим вариант t = 1, тогда f можно представить в виде
f(r) = g(r, t)+h(r, t). Каждый элемент (1−t)J умножается на 1−t и в результате h(r, 1) = 0.
В этом случае f(r) = g(r, 1) и f(r) ∈ I. Исходя из того, что f принадлежит I и J , f ∈ I
⋂
J .
Получаем I
⋂
J ⊃ (tI + (1 − t)J)
⋂
ℜ[r1, . . . , rn], что и завершает доказательство.
Пусть A = {a0, a1, . . . , a∗} — множество вершин U–Y -схемы; Nai — базис соотношений
в вершине ai на текущем шаге метода; Na0 , Na1 , . . . , Na∗ — базисы соотношений в вершинах
U–Y -схемы; U — множество условий в виде u = (p(r1, . . . , rn) = 0), где p(r1, . . . , rn) ∈
∈ ℜ[r1, . . . , rn]; Y — множество операторов присваивания в виде ri := p(r1, . . . , rn), где
p(r1, . . . , rn) ∈ ℜ[r1, . . . , rn].
ISSN 1025-6415 Доповiдi Нацiональної академiї наук України, 2013, №9 45
3. Метод верхней аппроксимации. Рассмотрим псевдокод метода верхней аппрок-
симации(МВА) с [2].
Вход: U–Y-схема A, N0 — базис инвариантов в вершине a0.
Выход: Na0 , Na1 , . . . , Na∗ — базисы инвариантов для каждой вершины.
Na0 := N0
ToVisit.push(a0)
Visited := {}
while ToVisit 6= ∅ do
c := ToVisit.pop()
Visited := Visited
⋃
c
for all (c, y, a′) do
if Not a′ in Visited then
Na′ := ef(Na′ , y)
ToVisit.push(a′)
end if
end for
end while
ToVisit := A/{a0}
while ToVisit 6= ∅ do
c := take from ToVisit
if Nc 6= ∅ then
N := Nc
forall (a′, y, c) do
N := N
⋂
ef(Na′ , y)
end for
if (N 6= Nc) then
Nc := N
ToVisit := ToVisit
⋃
{a | for every (c, y, a)}
end if
end if
end while
Для применения метода для алгебры данных в виде кольца полиномов нужно решить
три задачи: задача о соотношениях (ef(. . .)), пересечении (
⋂
) и стабилизации.
46 ISSN 1025-6415 Reports of the National Academy of Sciences of Ukraine, 2013, №9
Рис. 1. U–Y -программа УМН (x, y)
Задача о соотношениях. Для данного базиса соотношений M и оператора присваи-
вания y ∈ Y построить базис соотношений ef(M,y), которые истинны после выполнения
оператора присваивания.
В работе рассмотрен частный случай, когда оператор присваивания обратимый. В этом
случае равенство, которое представляет присваивание r′i = p(r1, . . . , rn), можно предста-
вить в виде ri = p′(r1, . . . , r
′
i, . . . , rn), где r′i — новое значение переменной. Заменив старую
переменную ее значением относительно нового значения переменной, получим базис соот-
ношений, справедливый после выполнения оператора присваивания.
Задача пересечения. По заданным базисам множеств соотношений I и J построить
базис множества соотношений I
⋂
J . Согласно теореме 1 о пересечении идеалов, пересечение
можно построить, используя формулу (1).
Задача стабилизации. Доказать, что процесс работы метода построения базисов соо-
тношений конечен. Исследование этой задачи не представлено в данной работе.
4. Реализация. Рассмотрим U–Y -программу из рис. 1. На этой программе мы проде-
монстрируем роботу алгоритма, считая алгебру данных кольцом полиномов [8]. Применяя
алгоритм МВА к этой U–Y -программе, получаем нижеприведенную цепочку вычислений
и инвариантные соотношения.
На первом этапе алгоритма МВА генерируем начальные множества соотношений. Сна-
чала множествам соотношений для всех состояний программы присваивается значение 1
(∀P : P
∗
⋂
1 = P ), при этом ToVisit= {a0}.
Далее рассматриваем состояние a0 из ToVisit, фиксируя Visited= {a0}. Из состояния a0
есть один переход (a0, 1, y = (u := x; z := 0), a1).
Анализируя этот переход, множеству соотношений Pa1 присваиваем
Pa1 := ef(Pa0 , y) = ef(1, (u := x, z := 0)) = {u− x = 0, z = 0}.
При этом ToVisit = {a1}.
Переходим к состоянию a1 из ToVisit, фиксируя Visited = {a0, a1}. Из состояния a1 есть
два перехода (a1, (u 6= 0), (u := u − 1; z := z + y), a1), (a1, (u = 0), ε, a∗). Исходя из a1 ∈
Visited, рассмотрению подлежит только переход из a1 в a∗.
Анализируя переход (a1, (u = 0), ε, a∗), находим целесообразным заменить этот переход
следующим переходом (a1, 1, u := 0, a∗). То есть заменить обязательное условие перехода
оператором присваивания. Множеству соотношений Pa∗ присваиваем:
Pa∗ := ef(Pa1 , y) = ef({u− x = 0, z = 0}, {u := 0}) = {x = 0, z = 0}.
ISSN 1025-6415 Доповiдi Нацiональної академiї наук України, 2013, №9 47
При этом ToVisit = {a∗}.
Переходим к состоянию a∗ из ToVisit, фиксируя Visited = {a0, a1, a
∗}. Нет переходов
из состояния a∗. Исходя из ToVisit = ∅, первый этап МВА заканчиваем. Переходим ко
второму этапу алгоритма.
На втором этапе алгоритма мы на каждом шаге итерации генерируем соотношения для
состояний. После пересекаем множества соотношений с полученными на предыдущем шаге.
При инициализации ToVisit = A/{a0} = {a1, a
∗}.
Переходим к состоянию a1 из ToVisitP = Pa1 = {u − x = 0, z = 0}. В состояние a1 есть
два перехода (a0, 1, (u := x; z := 0), a1), (a1, (u 6= 0), (u := u − 1; z := z + y), a1).
Анализируя переход (a0, 1, (u := x; z := 0), a1), множеству соотношений P присваиваем
P := P
∗
⋂
ef(Pa0 , y) := P
∗
⋂
ef(1, (u := x; z := 0)) =
= {u− x = 0, z = 0}
∗
⋂
{u− x = 0, z = 0} = {u− x = 0, z = 0}.
Анализируя переход (a1, (u 6= 0), (u := u− 1; z := z + y), a1), множеству соотношений P
присваиваем
P := P
∗
⋂
ef(Pa1 , y) := P
∗
⋂
ef({u− x = 0, z = 0}, (u := u− 1; z := z + y)) =
= {u− x = 0, z = 0}
∗
⋂
{u+ 1− x = 0, z − y = 0} =
= {z + (u− x)y = 0, z(y − z) = 0, zx− zu− z = 0, (u− x)2 + u− x = 0}.
Исходя из P 6= Pa1 , присваиваем
Pa1 := {z + (u− x)y = 0, z(y − z) = 0, zx− zu− z = 0, (u− x)2 + u− x = 0}
и ToVisit := ToVisit
⋃
{a1, a
∗} = {a1, a
∗}.
Переходим к состоянию a∗ из ToVisit, фиксируя Visited = {a1} и P = Pa∗ = {x = 0, z =
= 0}. В состояние a∗ есть один переход (a1, 1, u := 0, a∗).
Анализируя переход (a1, 1, u := 0, a∗), множеству соотношений P присваиваем:
P := P
∗
⋂
ef(Pa1 , y) = P
∗
⋂
ef({z + (u− x)y = 0, z(y − z) = 0, zx− zu− z = 0,
(u− x)2+ u− x= 0}, u := 0)= P
∗
⋂
{xy− z= 0, zy− z2= 0, zx− z= 0, x2− x= 0}=
= {x = 0, z = 0}
∗
⋂
{xy − z = 0, zy − z2 = 0, zx− z = 0, x2 − x = 0} =
= {z(x− 1) = 0, z(y − z) = 0, (x2 − x)u = 0, (xy − z)u = 0}.
Исходя из P 6= Pa∗ , присваиваем Pa∗ := {z(x − 1) = 0, z(y − z) = 0, (x2 − x)u = 0, (xy −
− z)u = 0}.
48 ISSN 1025-6415 Reports of the National Academy of Sciences of Ukraine, 2013, №9
Переходим к состоянию a1 из ToVisit, фиксируя Visited = ∅ и P = Pa1 = {z+(u−x)y =
= 0, z(y − z) = 0, zx − zu − z = 0, (u − x)2 + u − x = 0}. В состояние a1 есть два перехода
(a0, 1, (u := x; z := 0), a1), (a1, (u 6= 0), (u := u − 1; z := z + y), a1).
Анализируя переход (a0, 1, (u := x; z := 0), a1), множеству соотношений P присваиваем:
P := P
∗
⋂
ef(Pa0 , y) := P
∗
⋂
{u− x = 0, z = 0} = {z + (u− x)y = 0, z(y − z) = 0,
zx− zu− z = 0, (u− x)2 + u− x = 0}
∗
⋂
{u− x = 0, z = 0} =
= {(x− u)y − z = 0, zy − z2 = 0, zx− zu− z = 0, (u− x)2 + u− x = 0}.
Анализируя переход (a1, (u 6= 0), (u := u− 1; z := z + y), a1), множеству соотношений P
присваиваем
P := P
∗
⋂
ef(Pa1 , y) := P
∗
⋂
ef(Pa1 , (u := u− 1; z := z + y)) = {xy − uy − z = 0, . . .}.
Исходя из P 6= Pa1 , присваиваем
Pa1 := {xy − uy − z = 0, . . .} и ToVisit := ToVisit
⋃
{a1, a
∗} = {a1, a
∗}.
Переходим к состоянию a∗ из ToVisit, фиксируя Visited = {a1} и P = Pa∗ = {z(x −
− 1) = 0, z(y − z) = 0, (x2 − x)u = 0, (xy − z)u = 0}. В состояние a∗ есть один переход
(a1, 1, u := 0, a∗).
Анализируя этот переход, множеству соотношений P присваиваем: P := P
∗
⋂
ef(Pa1 , u :=
= 0) := P
∗
⋂
{xy − z = 0, . . .} = {xy − z = 0, . . .}.
Исходя из P 6= Pa∗ , присваиваем Pa∗ := {xy − z = 0, . . .}.
Выполняя действия по алгоритму, мы заметили, что с каждой новой итерацией размер-
ность базисов Pa1 и Pa∗ остается неизменной, так же, как и один из многочленов этих
базисов. Это многочлен xy−uy− z = 0 в a1 и xy− z = 0 в a∗. Как мы видим из постановки
задачи, инвариант z = xy подтверждает правильность программы. В этом примере работа
автоматического доказчика не понадобилась.
Таким образом, в работе представлены теоретические обоснования и реализация метода
верхней аппроксимации для программ над кольцами полиномов. Инварианты программ
приведены в виде идеалов. Идеалы, в свою очередь, задаются базисами Гребнера, операции
над которыми удовлетворяют требованиям по применению МВА, изложенным в [2]. Метод
реализован в программном коплексе Maple, который содержит мощные инструменты для
символьных вычислений. Приведен пример функционирования разработанного метода.
1. Hoare T. The verifying compiler: A Grand challenge for computing research // J. of the ACM. – 2003. –
No 50(1) – P. 63–69.
2. Годлевский А.Б., Капитонова Ю.В., Кривой С.Л., Летичевский А.А. Итеративные методы анализа
программ. Равенства и неравенства // Кибернетика. – 1990. – № 3. – С. 1–9.
3. Кривой С.Л. Об одном алгоритме поиска инвариантных соотношений в программах // Там же. –
1981. – № 5. – С. 12–18.
4. Кривой С.Л. О поиске инвариантных соотношений в программах // Математическая теория проек-
тирования вычислительных машин. – Киев: Изд. Ин-та кибернетики АН УССР, 1978. – С. 35–51.
ISSN 1025-6415 Доповiдi Нацiональної академiї наук України, 2013, №9 49
5. Летичевский А.А. О поиске инвариантных соотношений в программах // Алгоритмы в современной
математике – 1981. – № 122. – С. 304–314.
6. Gröbner bases and applications / Eds. B. Buchberger, F. Winkler. – Cambridge: Cambridge Univ. Press,
1998. – 552 p.
7. Максимец А.Н. Поиск инвариантов U–Y-программ итерационным алгоритмом над совершенно сво-
бодными алгебрами данных // Пробл. програмування. – 2012. – № 2–3. – С. 228–333.
8. Maksymets O.M. Upper approximation method for polynomial invariants // Theoretical and Applied
Aspects of Cybernetics. – Proceedings of the 2nd Intern. Scientific Conf. of Students and Young Scientists.
Computer Science Section. – Kyiv, 2012. – P. 45–47.
9. Lvov M. S. About one algorithm of program polynomial invariants generation // Proc. Workshop on Invari-
ant Generation: (Techn. rep.) Univ. of Linz / Eds. M. Giese, T. Jebelean. No 0707. – (RISC Report Series).
Linz (Austria), 2007. – P. 85–99 (electronic).
10. Львов М.С., Крекнiн В.А. Нелiнiйнi iнварiанти лiнiйних циклiв та власнi полiноми лiнiйних опера-
торiв // Кибернетика и системный анализ. – 2012. – № 2. – С. 126–140.
11. Годлевский А.Б., Капитонова Ю.В., Кривой С.Л., Летичевский А.А. Итеративные методы анализа
программ. Равенства и неравенства // Кибернетика. – 1990. – № 3. – С. 1–9.
12. Sabelfeld V.K. Equivalente Transformationen für Flussdiagramme // Acta Informatica. – 1978. – 10. –
P. 127–155.
Поступило в редакцию 28.01.2013Киевский национальный университет
им. Тараса Шевченко
О.М. Максимець
Пошук програмних 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 про перетин множин iнварiантiв з використанням
базисiв Грьобнера при умовi невиродженостi оператора присвоювання.
O.M. Maksymets
Polynomial invariants generation of programs
A solution of the polynomial invariant generation problem for programs is presented. The itera-
tion 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.
50 ISSN 1025-6415 Reports of the National Academy of Sciences of Ukraine, 2013, №9
|
| id | nasplib_isofts_kiev_ua-123456789-85891 |
| institution | Digital Library of Periodicals of National Academy of Sciences of Ukraine |
| issn | 1025-6415 |
| language | Russian |
| last_indexed | 2025-12-07T17:46:54Z |
| publishDate | 2013 |
| publisher | Видавничий дім "Академперіодика" НАН України |
| record_format | dspace |
| spelling | Максимец, А.Н. 2015-08-31T16:16:29Z 2015-08-31T16:16:29Z 2013 Поиск программных инвариантов в виде полиномов / А.Н. Максимец // Доповiдi Нацiональної академiї наук України. — 2013. — № 9. — С. 44–50. — Бібліогр.: 12 назв. — рос. 1025-6415 https://nasplib.isofts.kiev.ua/handle/123456789/85891 519.6:539.3 Представлено решение проблемы поиска инвариантов программ в виде полиномиальных
 зависимостей методом верхней аппроксимации. Этот итерационный метод, с успехом примененный к программам над абсолютно свободными алгебрами и векторными пространствами данных, адаптирован для кольца полиномов. Множество инвариантов
 в этом случае представляется в виде идеала кольца полиномов. Решены задачи о соотношениях и о пересечении множеств инвариантов с использованием базисов Гребнера при условии невырожденности оператора присваивания. Наведено р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. ru Видавничий дім "Академперіодика" НАН України Доповіді НАН України Інформатика та кібернетика Поиск программных инвариантов в виде полиномов Пошук програмних iнварiантiв у виглядi полiномiв Polynomial invariants generation of programs Article published earlier |
| spellingShingle | Поиск программных инвариантов в виде полиномов Максимец, А.Н. Інформатика та кібернетика |
| title | Поиск программных инвариантов в виде полиномов |
| title_alt | Пошук програмних iнварiантiв у виглядi полiномiв Polynomial invariants generation of programs |
| title_full | Поиск программных инвариантов в виде полиномов |
| title_fullStr | Поиск программных инвариантов в виде полиномов |
| title_full_unstemmed | Поиск программных инвариантов в виде полиномов |
| title_short | Поиск программных инвариантов в виде полиномов |
| title_sort | поиск программных инвариантов в виде полиномов |
| topic | Інформатика та кібернетика |
| topic_facet | Інформатика та кібернетика |
| url | https://nasplib.isofts.kiev.ua/handle/123456789/85891 |
| work_keys_str_mv | AT maksimecan poiskprogrammnyhinvariantovvvidepolinomov AT maksimecan pošukprogramnihinvariantivuviglâdipolinomiv AT maksimecan polynomialinvariantsgenerationofprograms |