Verification of programs: status, problems and experimental results. II
Prombles in programming 2014; 1: 76-89
Збережено в:
| Дата: | 2025 |
|---|---|
| Автор: | |
| Формат: | Стаття |
| Мова: | Russian |
| Опубліковано: |
PROBLEMS IN PROGRAMMING
2025
|
| Теми: | |
| Онлайн доступ: | https://pp.isofts.kiev.ua/index.php/ojs1/article/view/733 |
| Теги: |
Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
|
| Назва журналу: | Problems in programming |
| Завантажити файл: |  |
Репозитарії
Problems in programming| id |
pp_isofts_kiev_ua-article-733 |
|---|---|
| record_format |
ojs |
| resource_txt_mv |
ppisoftskievua/e5/9feaedd7114fbf029f861984b9d5f3e5.pdf |
| spelling |
pp_isofts_kiev_ua-article-7332025-04-09T22:38:00Z Verification of programs: status, problems and experimental results. II Верификация программ: состояние, проблемы, экспериментальные результаты. II Верификация программ: состояние, проблемы, экспериментальные результаты. II Maksymets, A.N. UDC 51.681.3 УДК 51.681.3 Prombles in programming 2014; 1: 76-89 Рассматриваются алгоритмы поиска инвариантных соотношений в программах с простыми переменными, которые относятся к методам анализа потоков данных и верификации. Приводится краткий обзор таких методов и примеры для иллюстрации работы предлагаемых алгоритмов.Prombles in programming 2014; 1: 76-89 Рассматриваются алгоритмы поиска инвариантных соотношений в программах с простыми переменными, которые относятся к методам анализа потоков данных и верификации. Приводится краткий обзор таких методов и примеры для иллюстрации работы предлагаемых алгоритмов. PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2025-04-09 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/733 PROBLEMS IN PROGRAMMING; No 1 (2014); 76-89 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 1 (2014); 76-89 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 1 (2014); 76-89 1727-4907 ru https://pp.isofts.kiev.ua/index.php/ojs1/article/view/733/785 Copyright (c) 2025 PROBLEMS IN PROGRAMMING |
| institution |
Problems in programming |
| baseUrl_str |
https://pp.isofts.kiev.ua/index.php/ojs1/oai |
| datestamp_date |
2025-04-09T22:38:00Z |
| collection |
OJS |
| language |
Russian |
| topic |
UDC 51.681.3 |
| spellingShingle |
UDC 51.681.3 Maksymets, A.N. Verification of programs: status, problems and experimental results. II |
| topic_facet |
UDC 51.681.3 УДК 51.681.3 |
| format |
Article |
| author |
Maksymets, A.N. |
| author_facet |
Maksymets, A.N. |
| author_sort |
Maksymets, A.N. |
| title |
Verification of programs: status, problems and experimental results. II |
| title_short |
Verification of programs: status, problems and experimental results. II |
| title_full |
Verification of programs: status, problems and experimental results. II |
| title_fullStr |
Verification of programs: status, problems and experimental results. II |
| title_full_unstemmed |
Verification of programs: status, problems and experimental results. II |
| title_sort |
verification of programs: status, problems and experimental results. ii |
| title_alt |
Верификация программ: состояние, проблемы, экспериментальные результаты. II Верификация программ: состояние, проблемы, экспериментальные результаты. II |
| description |
Prombles in programming 2014; 1: 76-89 |
| publisher |
PROBLEMS IN PROGRAMMING |
| publishDate |
2025 |
| url |
https://pp.isofts.kiev.ua/index.php/ojs1/article/view/733 |
| work_keys_str_mv |
AT maksymetsan verificationofprogramsstatusproblemsandexperimentalresultsii AT maksymetsan verifikaciâprogrammsostoânieproblemyéksperimentalʹnyerezulʹtatyii |
| first_indexed |
2025-07-17T10:03:21Z |
| last_indexed |
2025-07-17T10:03:21Z |
| _version_ |
1850411430403112960 |
| fulltext |
Верифікація програм
© А.Н. Максимец, 2014
76 ISSN 1727-4907. Проблеми програмування. 2014. № 1
УДК 51.681.3
А.Н. Максимец
ВЕРИФИКАЦИЯ ПРОГРАММ: СОСТОЯНИЕ, ПРОБЛЕМЫ,
ЭКСПЕРИМЕНТАЛЬНЫЕ РЕЗУЛЬТАТЫ. II
Рассматриваются алгоритмы поиска инвариантных соотношений в программах с простыми
переменными, которые относятся к методам анализа потоков данных и верификации. Приводится
краткий обзор таких методов и примеры для илюстрации работы предлагаемых алгоритмов.
Введение
Данная работа – это продолжение
предыдущей (I части) [1].
В первой части работы были пред-
ставлены краткие сведения о методах ве-
рификации и актуальных задач проблемы
верификации программ. В ней обозрева-
лась проблематика верификации реактив-
ных и функциональных систем, где указа-
но место предложенного подхода в фор-
мальных методах верификации. Приводи-
лись основные понятия, используемые в
этой области, а также описывались свой-
ства введенных понятий вместе с обосно-
ванием их правильности.
В данной статье более детально
рассматриваются методы верификации и
их реализация применительно к конкрет-
ным программам над конкретными алгеб-
рами данных. Детально рассматривается
язык типа равенств для программ над аб-
солютно свободными алгебрами данных и
кольцами полиномов. Приведены резуль-
таты экспериментов для программ над
этими алгебрами данных.
1. Язык равенств.
Основные задачи
Пусть A – YU -программа с
множеством переменных },,,{= 21 mrrrR ,
рассматриваемая над алгеброй данных
),(D , ),( EqK класс алгебр, содержа-
щий алгебру ),(D и определяемый мно-
жеством тождественных соотношений Eq ,
а )(RTD – свободная алгебра термов над
R из класса ),( EqK .
Рассмотрим проблему поиска инва-
риантов для языка L , состоящего из усло-
вий типа равенств )(=)( rhrg , где
),,(=),()(),( 1 mD rrrRTrhrg (т. e. L
не учитывает условий из U ).
Приведем необходимые определе-
ния и некоторые результаты общего харак-
тера, следуя работам [2, 4, 5, 6].
Пусть M – некоторое множество
равенств. Алгебраическим замыканием
множества M относительно Eq называет-
ся наименьшее множество )(MC , содер-
жащее рефлексивное, симметричное и
транзитивное замыкание M , все тожде-
ства из Eq и для всякой n -арной опера-
ции вместе с парами ),(( 1 rg
))(),((,)),(1 rqrgrq nn содержит пару
)))(,),(()),(,),((( 11 rqrqrgrg nn .
Множество M называется алгебра-
ически замкнутым, если MMC =)( .
Теорема 1. MMMC =)( – кон-
груэнция на )(RTD .
Доказательство очевидным образом
следует из определений конгруэнции и ал-
гебраического замыкания.
Подмножество P алгебраически
замкнутого множества M называется ал-
гебраическим базисом M , если =)(PC
M= .
Пусть M – алгебраически замкну-
тое множество равенств. Соответствую-
щую фактор-алгебру будем обозначать
MRTD )/( , ее элементы ),(modMt t
)(RTD , а равенство термов в виде
)(= modMtt . С каждым оператором при-
сваивания ))(:=,),(:=(= 11 rtrrtry mm
))(( RTt Di и алгебраически замкнутым
множеством M свяжем гомоморфизм
Верифікація програм
77
MRTRTh DDy )/()(: , полагая =)( iy rh
)(= modMti .
Конгруэнция M на )(RTD называ-
ется нормальной, если она является ядром
эндоморфизма алгебры )(RTD , т. е.
MRTD )/( изоморфна подалгебре алгебры
)(RTD .
Пусть ),( yMef (сужение )),,( yuMef
обозначает множество равенств вида
)(=)( rtrt таких, что =),,( 1 mttt
Mttt m ),,(= 1 .
Очевидно, что ),( yMef – кон-
груэнция и )(=),( yhkeryMef , где :yh
MRTRT DD )/()(: – некоторый гомо-
морфизм.
Лемма 1.
.),(=)),,(( yyMefyyMefef
Теорема 2. Если M – нормальная
конгруэнция, то ),( yMef тоже нормаль-
ная конгруэнция.
Функция ef называется дистрибу-
тивной, если для любых M и M верно
),(),(=),( yMefyMefyMMef .
Теорема 3. Если множества M ,
M алгебраически замкнуты, то функция
ef дистрибутивна.
Заметим, что свойство дистрибу-
тивности функции ef более сильное, чем
свойство монотонности, т.к. из дистрибу-
тивности функции ef следует ее монотон-
ность.
Действительно, если M M , то в
силу дистрибутивности функции ef мож-
но записать
( , ) = ( , ) =ef M M y ef M y
),(),(= yMefyMef .
Откуда следует, что ),(),( yMefyMef .
Допустим что известно как строить
множество ),( yMef или его алгебраиче-
ский базис и находить пересечение таких
множеств или алгебраический базис этого
пересечения. Тогда, используя одну из
формул
,,0,>
),,,(=
1)(
),,,(
)(
Aaan
yuNefN
n
a
Sayua
n
a
(1)
или
( )
( 1) ( 1)
( , , , )
=
= ( ( , , )),
> 0, , ,
n
a
n n
a a
a u y a S
N
N ef N u y
n a a A
(2)
можно организовать процесс поиска инва-
риантов в состояниях программы, отправ-
ляясь от некоторых начальных алгебраи-
чески замкнутых множеств, сопоставлен-
ных состояниям программы, и повторять
его до тех пор, пока множества ),( yMef в
данных состояниях не перестанут изме-
няться (стабилизируются). Заметим, что
если множества ),( yMef обладают конеч-
ными базисами, то из стабилизации мно-
жеств ),( yMef следует стабилизация их
базисов и наоборот. Следовательно, про-
блема построения множеств инвариантов в
состояниях U -Y -программы над заданной
алгеброй данных )(RTD сводится к следу-
ющим основным задачам.
Задача о соотношениях. Постро-
ить по заданному множеству равенств M
(или его алгебраическому базису) и опера-
тору Yy множество ),( yMef (или его
алгебраический базис).
Задача о пересечении. По задан-
ным множествам ),( yMef и ),( yMef по-
строить множество ),(),( yMefyMef
(или его алгебраический базис).
Задача о стабилизации. Показать,
что процесс построения множеств
),( yMef (или их алгебраических базисов),
сопоставленных состояниям программы,
стабилизируется.
В определении метода МВА про-
цесс вычисления инвариантов зависит, во-
обще говоря, от выбора совокупности про-
стых путей, определяющих начальное
приближение. Аналогичная ситуация име-
ет место и при переходе от параллельного
Верифікація програм
78
вычисления приближений по формулам (1)
и (2), когда на каждом шаге итерации вы-
числения производятся одновременно для
всех состояний, к последовательному, ко-
гда в текущий момент для разных состоя-
ний рассматриваются, вообще говоря, раз-
ные приближения. Последовательное вы-
числение приближений позволяет суще-
ственно уменьшить объем вычислений, так
как для части состояний на определенных
итерациях вообще не будет происходить
изменений. Например, если существует
путь из a в a и не существует пути из a
в a , то множество инвариантов в состоя-
нии a никак не зависит от соответствую-
щего множества для состояния a и про-
цессы вычисления инвариантов для таких
состояний удобно разнести, вычисляя их
сначала для a и лишь затем для a .
Далее приводятся последователь-
ные алгоритмы нижней и верхней аппрок-
симации.
Относительно исходной U -Y -прог-
раммы будем предполагать. Во-первых,
что все ее состояния, за исключением быть
может начального и заключительного, яв-
ляются ветвлениями или слияниями. Этого
можно достичь в результате перемножения
операторов присваивания на линейных
участках. Во-вторых, что с каждым состо-
янием a ассоциируется множество соот-
ношений aN . Пусть S – множество пере-
ходов U -Y -программы и
}),,,(|{=)( SayuaAaaPs .
В описываемых далее алгоритмах
NNa , – переменные типа “множествo”,
значения которых – множества соотноше-
ний в состоянии Aa , 0N – начальное
множество соотношений, a |):|(1 Av – мас-
сив логических значений, C – переменная
типа множество.
2. Алгоритмы нижней и верхней
аппроксимаций
Рассмотрим представление МНА на
псевдоязыке.
Входные данные: 0N входные
условия для YU - схемы A .
Выходные данные: aN базис
инвариантов в состоянии a программы A .
Рассмотрим представление МВА на
псевдоязыке:
Входные данные: 0N входные
условия для U -Y -программы A .
Выходные данные: aN базис инва-
риантов в состоянии a программы A .
Семантика оператора take a from ToVisit
такова, что фиксируется элемент a в мно-
Верифікація програм
79
жестве ,ToVisit который при этом удаля-
ется из указанного множества, а оператор
выйти из цикла означает завершение
наименьшего цикла, в который он входит.
Стратегия выбора элементов из ToVisit ,
вообще говоря, произвольная, но предпо-
лагается, что всегда последним элементом,
извлекаемым из ToVisit , является заклю-
чительное состояние. Множество простых
путей, по которому определяется началь-
ное приближение, в числе входных пара-
метров не фиксируется.
Наряду с приведенными алгорит-
мами можно рассматривать их версии,
ориентированные на работу с алгебраиче-
скими базисами. Oни отличаются тем, что
значением входного параметра N являет-
ся не само множество соотношений, а его
алгебраический базис P , и вместо опера-
ции пересечения множеств соотноше-
ний следует рассматривать операцию
*
построения базиса их пересечения.
Некоторые общие свойства описан-
ных алгоритмов МВА и МНА при некото-
рых ограничениях вытекают из нижепри-
веденных утверждений [4, 6]. В силу двой-
ственности отношения частичного порядка
достаточно рассмотреть, например, убы-
вающую цепочку множеств соотношений
,321 nNNNN (3)
имеющую место в некотором состоянии a
YU - -программы A .
Теорема 4. Если свободная алгебра
)(RTD конечно порождена и каждый эле-
мент iN последовательности (3) является
нормальной конгруэнцией, то эта последо-
вательность стабилизируется через конеч-
ное число шагов.
Из этой теоремы получаем следу-
ющие утверждения.
Следствие 1. Если элементы после-
довательности (3) обладают алгебраиче-
скими базисами и, в частности, конечными
алгебраическими базисами, то эта после-
довательность стабилизируется через ко-
нечное число шагов.
Отметим еще некоторые простые
свойства алгоритмов генерации инвари-
антных соотношений, которые вытекают
из теоремы 4.
Теорема 5. Если в YU - -программе
множество 0N и пересечение нормальных
конгруэнций есть нормальные конгруэн-
ции, то алгоритм МВА заканчивает свою
работу после конечного числа шагов.
Действительно, по условию теоре-
мы алгоритм МВА в каждом состоянии
YU - -программы строит убывающую це-
почку нормальных конгруэнций (0)
aN
)((1) n
aa NN , которая конечна в
силу теоремы 4.
Теорема 6. Если в YU - -программе
0N – нормальная конгруэнция и пересече-
ние нормальных конгруэнций есть нор-
мальная конгруэнция, то алгоритм МНА
завершает свою работу после конечного
числа шагов.
Действительно, по условию теоре-
мы и согласно теореме 4 алгоритм МНА
в каждом состоянии U -Y -программы
строит возрастающую цепочку нормаль-
ных конгруэнций (1)(0) aa NN
)(n
aN , которая конечна в силу
выполнения условия обрыва возрастаю-
щих цепей.
Приведенные теоремы и их след-
ствия дают теоретическую завершимость
алгоритмов генерации множеств инвари-
антных соотношений, однако в них при-
сутствует некоторый элемент неконструк-
тивности – неизвестна длина последова-
тельности (3). При рассмотрении конкрет-
ных алгебр эта длина может уточняться.
Однако практическая ценность этих тео-
рем состоит в том, что они показывает, что
полнота алгоритмов генерации инвариант-
ных соотношений зависит от точности ал-
горитмов решения задач о соотношениях и
о пересечении. Если эти алгоритмы дают
точные решения, то алгоритмы МНА и
МВА дают максимально возможное мно-
жество инвариантов.
Попытаемся точно сформулиро-
вать условия, при выполнении которых
алгоритмы генерации инвариантных со-
отношений дают полные системы соот-
ношений.
Верифікація програм
80
Теорема 7. Если множество 0N и
множества соотношений, получаемых в
каждом состоянии YU - -программы в
процессе работы алгоритма МВА, нор-
мальные конгруэнции, то результат работы
алгоритма не зависит от порядка обхода
состояний YU - -программы (и от выбора
начальной совокупности простых путей), а
множествo инвариантов aN для всякого
состояния Aa совпадает с множеством
),( 0
),0(=
l
aall
yNef .
Доказательство этой теоремы мож-
но найти в [4, 6], позволяющее ввести та-
кое определение.
Определение 1. Множество инва-
риантов любого состояния YU - -прог-
раммы совпадающее с множеством
),( 0
),0(=
l
aall
yNef , называется полным от-
носительно генератора Gen, языка инвари-
антов L и начального множества 0N .
Теорема 7 дает условия, при кото-
рых алгоритм МВА генерирует полные
множества инвариантов относительно
начальной совокупности соотношений.
Когда функция ef не является дистрибу-
тивной, получение полной системы соот-
ношений становится неразрешимой зада-
чей, что вытекает из следующего утвер-
ждения.
Теорема 8. Если функция ef не
является дистрибутивной, то можно ука-
зать YU - -программу A с начальным
множеством соотношений 0N , для кото-
рой не существует алгоритма, генерирую-
щего полную систему инвариантов отно-
сительно 0N для этой YU - -программы.
Доказательство этой теоремы полу-
чается путем сведения данной проблемы к
модифицированной проблеме соответ-
ствий Поста [3].
Учитывая данную теорему возника-
ет естественный вопрос, а на какое множе-
ство инвариантов можно рассчитывать в
случае монотонной функции ef и какие
свойства этих множеств? Oтвет на этот во-
прос дает следующая теорема.
Теорема 9. Если алгоритм МВА
завершает свою работу после конечного
числа шагов и функция ef является моно-
тонной, то полученное в результате мно-
жество инвариантов aN для любого состо-
яния Aa является максимальной фикси-
рованной точкой решения системы урав-
нений
00
),,,(
=
),(=
NX
yXefXX
a
a
Sayua
aa
.
На завершение приведем некоторые
экспериментальные данные, полученные в
результате реализации алгоритмов МВА и
МНА.
3. Экспериментальные
результаты реализации
Эффективность применения алго-
ритмов МВА и МНА зависит от уровня
представления программы, поскольку
множества инвариантных соотношений
становятся богаче с понижением уровня
представления. Иллюстрацией этого вы-
сказывания является хорошо известная
фортрановская программа умножения
квадратных матриц размерности nn –
),,( nYXMULT :
На этом уровне алгоритмы МНА и
МВА не дают никаких соотношений, но
если применить эти алгоритмы к пред-
ставлению этой же программы на проме-
жуточном уровне, тогда U -Y программа
имеет вид представленный на рис. 1.
Верифікація програм
81
Рис. 1. YU - -программа MULT(X, Y, n)
Этот уровень представления про-
граммы получается учитывая то, что
элементы исходных матриц A и B , нахо-
дящиеся в двумерных массивах, преобра-
зуются для размещения в одномерном
массиве Z . Это преобразование выполня-
ет компилятор языка Фортран. Приве-
денная выше YU - -программа (рис. 1),
алгебра данных которой считается абсо-
лютно свободной, записанная в более
общем языке, чем язык стандартных
YU - -программ, в связи с наличием опе-
раторов манипуляции с массивами. Эти
операторы игнорируются при работе ал-
горитма.
Алгоритм МВА, будучи применен-
ным к этой YU - -программе, алгебра дан-
ных которой предполагается абсолютно
свободной, генерирует следующие инва-
рианты для состояний программы:
=
0aN ,
=
1aN ,
=
2aN ,
}*={= 13
injtNa ,
}=,=,*={= 131214
ttttinjtNa ,
}=,={= 13125
ttttNa ,
}=,={= 13126
ttttNa ,
}=,={== 13126* ttttNN
a
.
Анализируя инварианты мы можем
оптимизировать использование перемен-
ных, имеющих одинаковые значения 1t ,
2t , 3t . Так в состоянии 3a мы можем оп-
тимизировать одной переменной вместо
3-х. Оптимизированная программа имеет
вид (рис. 2).
Верифікація програм
82
Рис. 2. Оптимизированная U -Y -программа MULT(X, Y, n)
Рассмотрим YU - -программу из
рис. 3, для удобства приведенную далее.
На этой программе продемонстрируем
роботу алгоритма считая алгебру данных
кольцом полиномов [7]. Применяя алго-
ритм МВА к этой YU - -программе полу-
чаем далее приведенную цепочку вычис-
лений и инвариантные соотношения.
Рис. 3. YU - -программа УМН(x, y)
На первом этапе алгоритма МВА
генерируем начальные множества соот-
ношений. Сначала множествам соотноше-
ний для всех состояний программы при-
сваивается значение 1 ( PPP =1: ), при
этом }{= 0aToVisit .
Далее рассматривается состояние
0a из ToVisit , фиксируя }{= 0aVisited . Из
состояния 0a есть один переход
)0),:=;:=(=,1,( 10 azxuya .
Анализируя переход данного мно-
жества соотношений
1a
P присваивается:
=0)):=,:=((1,=),(:=
01
zxuefyPefP aa
.0=0,== zxu
При этом }{= 1aToVisit .
Переходим к состоянию 1a из
ToVisit , фиксируя },{= 10 aaVisited . Из
состояния 1a есть два перехода 0),=(,( 1 ua
),),:=1;:=( 1ayzzuu ),0),=(,( *
1 aua .
Исходя из Visiteda1 рассмотрению под-
Верифікація програм
83
лежит только переход из 1a в *a .
Анализируя переход ,0),=(,( 1 ua
)*a находим целесообразным заменить
этот переход следующим переходом
)0,:=,1,( *
1 aua . То есть заменить объяза-
тельное условие перехода оператором
присваивания. Множеству соотношений
*a
P присваивается:
.0}=0,={
0}):={0},=0,=({=
=),(:=
1*
zx
uzxuef
yPefP aa
При этом }{= *aToVisit .
Переходим к состоянию *a из
ToVisit , фиксируя },,{= *
10 aaaVisited .
Нет переходов из состояния *a . Исходя
из =ToVisit первый этап МВА закон-
чен. Переходим ко второму этапу алго-
ритма.
На втором этапе алгоритма на каж-
дом шаге итерации генерируем соотно-
шения для состояний. После пересекаем
множества соотношений с полученными
на предыдущем шаге. При инициализации
},{=}/{= *
10 aaaAToVisit .
Переходим к состоянию 1a из
ToVisit 0}=0,={==
1
zxuPP a . В со-
стоянии 1a есть два перехода:
)0),:=;:=(,1,( 10 azxua ,
)),:=1;:=(0),=(,( 11 ayzzuuua .
Анализируя переход ;:=(,1,( 0 xua
)0),:= 1az , множеству соотношений P
присваивается:
:=),(:=
0
yPefPP a
.0)):=;:=((1,:= zxuefP
Анализируя переход 0),=(,( 1 ua
)),:=1;:=( 1ayzzuu , множеству соот-
ношений P присваивается:
:=),(:=
1
yPefPP a
:=1;:=(0},=0,=({:= zuuzxuefP
=1{0}=0,={=)):= xuzxuyz
=)(0,=)({0}=0,= zyzyxuzyz
.0}=)(0,=0,= 2 xuxuzzuzx
Исходя из
1
= aPP присваиваем
0,=)(0,=)({:=
1
zyzyxuzPa
и
,0}=)(0,= 2 xuxuzzuzx
},{=},{:= *
1
*
1 aaaaToVisitToVisit .
Переходим к состоянию *a из
ToVisit , фиксируя }{= 1aVisited и
0}=0,={== * zxPP
a
. В состоянии
*a
есть один переход )0,:=,1,( *
1 aua .
Анализируя переход :=,1,( 1 ua
,)0,:= *a множеству соотношений P при-
сваивается.
Исходя из *=
a
PP присваиваем
0,=)(0,=1)({:=* zyzxzP
a
0}=)(0,=)( 2 uzxyuxx .
Переходим к состоянию 1a из
ToVisit , фиксируя =Visited и
0,=)(0,=)({==
1
zyzyxuzPP a
0}=)(0,= 2 xuxuzzuzx .
В состоянии 1a есть два перехода:
)0),:=;:=(,1,( 10 azxua ,
)),:=1;:=(0),=(,( 11 ayzzuuua .
Анализируя переход ;:=(,1,( 0 xua
)0),:= 1az , множеству соотношений P
присваивается:
0}=0,={:=),(:=
0
zxuPyPefPP a
=0,=)(0,=)({= zzuzxzyzyxuz
0}=0,={0}=)(0, 2 zxuxuxu
zzuzxzzyzyux 0,=0,=){(= 2
.0}=)(0,= 2 xuxu
Верифікація програм
84
Анализируя переход :=(0),=(,( 1 uua
)),:=1;:= 1ayzzu , множеству соотно-
шений P присваивается:
1;:=(,(:=),(:=
11
uuPefPyPefPP aa
.}0,={)):= zuyxyyzz
Исходя из
1
= aPP присваиваем
}0,={:=
1
zuyxyPa
и
:=ToVisit },{=},{ *
1
*
1 aaaaToVisit .
Переходим к состоянию *a из
ToVisit , фиксируя }{= 1aVisited и
0,=)(0,=1)({== * zyzxzPP
a
.0}=)(0,=)( 2 uzxyuxx
В состоянии *a есть один переход
)0,:=,1,( *
1 aua .
Анализируя этот переход множе-
ству соотношений P присваивается:
zxyPuPefPP a {:=0):=,(:=
1
.}0,={}0,= zxy
Исходя из *=
a
PP присваиваем :=*a
P
}0,={:= zxy .
Выполняя действия по алгоритму
мы заметили, что с каждой новой итераци-
ей размерность базисов
1a
P и *a
P остается
неизменной, также как и один из много-
членов этих базисов. Это многочлен
0=zuyxy в 1a и 0=zxy в 0a . Как
мы видим из постановки задачи инвариант
xyz = подтверждает правильность про-
граммы. В этом примере работа автомати-
ческого доказчика не понадобилась.
Рассмотрим еще один пример про-
граммы которая вычисляет
y
y
m
z
n
y m
z
1
1=
1=
по входным параметрам m и n . На высо-
ком уровне YU - программы показана на
рис. 4.
Рис. 4. YU - программа
y
y
m
z
n
y m
z
1
1=
1=
Верифікація програм
85
Рассмотрим роботу алгоритма МВА
для программ над абсолютно свободными
алгебрами данных.
Инициализируем }{:= 0aToVisit .
Переходим к состоянию 0a из ToVisit ,
фиксируя }{= 0aVisited . Анализируем пе-
реход )1),:=0,:=2(,( 10 aysuma , множеству
соотношений
1aP присваивается:
=1)):=0,:=2(,(:=
01
ysumPefP aa
,1}=0,=2{= ysum
ведь =
0aP .
При этом }{= 1aToVisit .
Переходим к состоянию 1a из
ToVisit , фиксируя },{= 10 aaVisited . Ана-
лизируем переход )1),:=0,:=1(,( 21 azsuma ,
множеству соотношений
1aP присваива-
ется:
=1)):=0;:=1(,(:=
12
zsumPefP aa
1)):=0;:=1(1},=0,=2({ zsumysumef
.}=1,=2,=10,=2{ zyzsumsumsum
При этом }{= 2aToVisit .
Переходим к состоянию 2a из
ToVisit , фиксируя },,{= 210 aaaVisited .
Продолжая выполнение первого этапа
МВА, в результате получаем следующие
базисы соотношений:
,=
0aP
,1}=0,=2{=
1
ysumPa
,}=1,=2,=10,=2{=
2
zyzsumsumsumPa
,}=,=
1,=,2=10,=2{=
3
z
a
zxzy
zxsumsumsumP
,}=1,=
,=,0=11,0=2{=
4
y
z
a
zxy
mzzsumsumsumP
.}=,=
,=,0=1,00=2{=
1
*
zxny
mzzsumzsumP zz
a
Рассмотрим выполнение второго
этапа алгоритма. При инициализации
},,,,{= *
4321 aaaaaToVisit .
Переходим к состоянию 1a из
ToVisit 0}=0,={==
1
zxuPP a . В со-
стоянии 1a есть два перехода :=2(,( 0 suma
)1),:=0,:= 1ay , )1),:=(,( 14 ayya .
Анализируя переход :=2(,( 0 suma
)1),:=0,:= 1ay , множеству соотношений
P присваивается:
0,:=2(,(=),(:=
0
sumefPyPefPP a
1}=0,=2{=1)):= ysumy .
Анализируя переход yya :=(,( 4
)1), 1a , множеству соотношений P при-
сваивается:
=2({:=),(:=
4
sumefPyPefPP a
1,=,=,0=11,0= ymzzsumsum z
0}=0,={1)):=(},= zxuyyzx y
=){(=0}=0,=1{ zyuxyzxu
xuuuzzuzxzzy 20,=0,=0,= 22
,00=2{=0}=2 2 zzsumxxxu
.}=1,1=,=,0=1 1zxymzzsum z
Исходя из
1
= aPP присваиваем
,00=2{1}=0,=2{:=
1
z
a zsumysumP
=}=1,1=,=,0=1 1zxymzzsum z
и },,,{=}{:= *
4322 aaaaaToVisitToVisit .
Переходим к состоянию 2a из
2,=10,=2{==
2
sumsumsumPPToVisit a
}=1,= zyz .
В состоянии 1a есть два перехода
)1),:=0,:=1(,( 21 azsuma .)1),:=(,( 23 azza
Анализируя переход 0,:=1(,( 1 suma
)1),:= 2az , множеству соотношений P
присваивается:
Верифікація програм
86
=1)):=0,:=1(,(:=
1
zsumPefPP a
1)):=0,:=1(,( zsumefP
.1}=0,=1{= zsum
Анализируя переход 1),:=(,( 3 zza
)2a , множеству соотношений P присваи-
вается:
0,=2({:=),(:=
3
sumefPyPefPP a
},=,=1,=,2=1 zzxzyzxsumsum
1,=2,=10,=2{=1)):=( zsumsumsumzz
,2=10,=2{}= zzsumsumsumzy
.=}=1,=,= yyxyyyz
Исходя из
2
= aPP присваиваем
:=
2aP
и },,{=}{:= *
433 aaaaToVisitToVisit .
Переходим к состоянию 3a из
10,=2{==
3
sumsumPPToVisit a
}=,=1,=,2= zzxzyzxsum .
В состоянии 1a есть один переход
)),:=,1:=1(,( 32 azzzsumsuma yy .
Анализируя переход :=1(,( 2 suma
)),:=,1:= 3azzzsum yy , множеству соот-
ношений P присваивается:
0,=2{=),(:=
2
sumyPefPP a
,=1,=,2=1 zyzxsumsum
,1:=1(,(}= yz zsumsumefzx
.}={=)):= yy zxzz
Исходя из
3
= aPP присваиваем
}={:=
3
y
a zxP
и
},,{=},{:= *
4242 aaaaaToVisitToVisit .
Переходим к состоянию 2a из
ToVisit . Исходя из того, что =
2aP не
рассматриваем это состояние.
Переходим к состоянию 4a из
=11,0=2{==
4
sumsumsumPPToVisit a
.}=1,=,=,0= yz zxymzz
В состоянии 1a есть один переход
.)),:=,1/2:=2(,( 43 amxxsumsumsuma y
Анализируя переход
,:=,1/2:=2(,( 3
ymxxsumsumsuma
4:= ), ),z m a
множеству соотношений P присваивает-
ся:
1,0=2{=),(:=
3
sumsumyPefPP a
}=1,=,=,0=1 yz zxymzzsum
,1/2:=2(},=({ xsumsumsumzxef y
.}=,={=)):=,:= yy zxmzmzmx
Исходя из неравенства базисов
4
= aPP присваиваем
}=,={:=
4
y
a zxmzP
и
},,{=},{:= *
4151 aaaaaToVisitToVisit .
Переходим к состоянию 1a из
ToVisit . Исходя из того, что =
1aP не
рассматриваем это состояние.
Переходим к состоянию
*a из
,00=2{== *
z
a
zsumPPToVisit
.}=,=,=,0=1 1zxnymzzsum z
В состоянии
*a есть один переход
),:=,( *
4 anya .
Анализируя переход ),:=,( *
4 anya ,
множествy соотношений P присваивает-
ся:
Верифікація програм
87
=)):=(,(:=
4
nyPefPP a
,=,0=1,00=2{= mzzsumzsum zz
=)):=(},=,=({}=,= 1 nyzxmzefzxny y
.}=,={= nymz
Исходя из неравенства базисов
*=
a
PP присваиваем }=,={:=* nymzP
a
.
Множество ToVisit пустое по этому алго-
ритм заканчивает свою работу.
Pезультатом выполнения алгоритма
будет соотношения состояниям програм-
мы и базисы инвариантов:
,=
0aP
,=
1a
P
,=
2aP
,}={=
3
y
a zxP
,}=,={=
4
mzzxP y
a
}=,={=* mznyP
a
.
Полученные базисы инвариантов
могут являться входными параметрами для
автоматического доказателя. Поскольку в
состоянии 3a используется главная опера-
ция суммирования xsumsum 1:=1 Таким
образом инвариант
yzx := указывает, что
сумма считается правильно. В состоянии
4a выполняется операция деления на x и
правильными есть условия
yzx = и mz = ,
т. е. деление выполняется правильно отно-
сительно постановки задачи. Инварианты
в
*a дают возможность проверить условия
выхода из программы. Но в отличие от
предыдущего примера программы на низ-
ком уровне инварианты в рассмотренном
примере слабее.
Результаты реализации. Для реа-
лизации алгоритма МВА над абсолютно
свободной алгеброй данных использован
язык Java и использована библиотека
ANTLR для построения представления
выражений в виде дерева. Структура клас-
сов разделена на представление YU - про-
граммы и реализацию методов аппрок-
симации. Представлением YU - програм-
мы является класс YU - программы, со-
стоящий из ориентированного графа.
Вершины этого графа – объекты класса
состояний YU - программы, а ребра –
объекты класса переходов в YU - про-
грамме. Класс переходов в YU - програм-
ме включает в себя список выражений для
рассматриваемой алгебры, реализованных
в виде отдельного класса.
Реализации алгоритмов МВА и
МНА базируется на абстрактном классе
итерационного алгоритма. Этот класс со-
держит список пар вида состояния YU -
программы и базис множества соотноше-
ний в этом состоянии. Этот же класс со-
держит три метода: метод выполнения ша-
га алгоритма, метод проверки условия
окончания работы алгоритма и метод об-
хода состояний программы.
Для получения ориентировочных
оценок быстродействия алгоритма автома-
тически генерируется YU - схема про-
граммы в предположении абсолютно сво-
бодной алгебры, имеющей большое коли-
чество вершин и переходов. При этом
обеспечивается условие непустоты множе-
ства инвариантов программы.
Такой программой послужила про-
грамма из примера 1. В этой программе
добавлено еще одно ветвление от вершини
1. В этом ветлении, в автоматическом ре-
жиме, добавлялись новые состояния и ко-
пии ребра
)),:=1;:=(0),=(,( 11 ayzzuuua ,
составляющие цепочку с одинаковыми
операторами присваивания. В этом случае,
схема теряла свой алгоритмический
смысл, но позволяла оценить бытсродей-
ствие алгоритма в зависимости от размера
YU - схемы.
Целью эксперимента являлось
определение зависимости количества эле-
ментарных операций в МВА от таких па-
раметров: количества состояний схемы,
количества переходов между состояниями,
количества переменных и количества опе-
раций присваивания в программе. Резуль-
таты выполнения эксперимента представ-
лены ниже в таблице.
Верифікація програм
88
Таблица. Показатели быстродействия МВА
N
Кол-во
состояний
Кол-во
переходов
Кол-во
переменных
Кол-во
присваиваний
Кол-во операций
1. 7 8 3 14 432
2. 31 40 3 70 5564
3. 91 120 3 210 9271
4. 211 280 3 490 24559
5. 6001 8000 3 14000 1500078
Реализация алгоритма МВА для
кольца полиномов является более слож-
ной. Принято решение использовать более
высокоуровневый, с математической точки
зрения, инструмент, это вычислительный
пакет Maple. В этом случае для представ-
ления достаточно внутренних типов Maple.
Функция пересечения двух базисов мно-
жеств равенств в силу теоремы [7] реали-
зована с помощью пакета Groebner и явля-
ется креугольным камнем данной реализа-
ции. Реализация алгоритма обхода состоя-
ний программы практически является
транслированной реализации обхода, ис-
пользующийся для абсолютно свободных
алгебр.
Выводы
В статье приведено доказательство
полноты множества генерируемых соот-
ношений инвариантов при условии дис-
трибутивности операции ef для языка
равенств. Показано отсутствие полного
множества инвариантных соотношений в
случае не дистрибутивности операции ef
относительно операции пересечения.
Одним из основных результатов
проведенных исследований есть реализа-
ция методов МВА и МНА и их экспери-
ментальная апробация. Проиллюстриро-
вана эффективность методов на низком
уровне представления программ и их сла-
бая эффективность на высокоуровневом
представлении. Приведен пример работы
алгоритма МВА для программ, алгебрами
данных которых являются кольца поли-
номов. Алгоритм МВА показал себя
более интересным с практической точки
зрения.
Современные программные техно-
логии выдвигают все более высокие тре-
бования к возможностям верификации
программ. Учитывая это, предложенные
методы нуждаются в дальнейшем разви-
тии. Проведенные исследования указыва-
ют три направления развития: расшире-
ние алгебры данных, переход к объектно
ориентированному представлению пере-
менных, представления условий в виде
языка неравенств. Расширение работы ал-
горитмов МВА и МНА на более сложные
алгебры данных позволит анализировать
более сложные формулы в операторах
присваивания. На практике наиболее ис-
пользуемыми являются условия в виде не-
равенств, поэтому инварианты будут бо-
лее точными, если учесть эти дополни-
тельные условия на ветвлениях YU - схем
программ.
Проведение таких исследований да-
ет возможность вплотную приблизится к
верификации сложных программ, которые
используют объектно ориентированные
языки программирования на высоком
уровне. Решение этих задач может найти
применения в таких верификационных
комплексах как JPF (http://babelfish.
arc.nasa.gov/).
1. Максимец А.Н. Верификация программ:
состояние, проблемы, экспериментальные
результаты I // Проблеми програмування.
– 2013. – № 4. – С. 53–63.
Верифікація програм
89
2. Летичевский А.А. Эквивалентность и оп-
тимизация программ // Труды междунар.
симпозиума по теоретическому програм-
мированию. – Новосибирск. – 1972. –
С. 166–180.
3. Kam J.B., Ullman D.J. Monotone data flow
analysis frame works // Acta Inform. – 1978.
– N 3. – P. 305–318.
4. Годлевский А.Б., Капитонова Ю.В., Кри-
вой С.Л., Летичевский А.А. Итеративные
методы анализа программ // Кибернетика.
– 1989. – № 2. – C. 9–19.
5. Летичевский А.А. Об одном подходе к
анализу программ // Кибернетика. – 1979.
– № 6. – C. 1–8.
6. Годлевский А.Б., Капитонова Ю.В., Кри-
вой С.Л., Летичевский А.А. Итеративные
методы анализа программ. Равенства и не-
равенства // Кибернетика. – 1990. – № 3. –
С. 1–9.
7. Maksymets O.M. Upper approximation me-
thod for polynomial invariants Theoretical
and Applied Aspects of Cybernetics // Pro-
ceedings of the 2nd International Scientific
Conference of Students and Young Scientists.
Computer Science Section. – Kyiv: Bukrek. –
2012. – P. 45–47.
Получено 07.03.2013
Об авторе:
Максимец Александр Николаевич,
аспирант.
Место работы автора:
Киевский национальный университет
имени Тараса Шевченко,
факультет кибернетики.
Тел: +38 050 9852274.
E-mail: maksymets@gmail.com
|