Verification of programs: status, problems and experimental results. I

Prombles in programming 2013; 4: 53-63

Gespeichert in:

Bibliographische Detailangaben
Datum:	2025
1. Verfasser:	Maksymets, A.N.
Format:	Artikel
Sprache:	Russian
Veröffentlicht:	PROBLEMS IN PROGRAMMING 2025
Schlagworte:	UDC 51.681.3
Online Zugang:	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/741
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!
Назва журналу:	Problems in programming
Завантажити файл:

Institution

Problems in programming

id	pp_isofts_kiev_ua-article-741
record_format	ojs
resource_txt_mv	ppisoftskievua/1d/43ffa1decc902cfbb36d8adb5acfb71d.pdf
spelling	pp_isofts_kiev_ua-article-7412025-04-16T13:52:57Z Verification of programs: status, problems and experimental results. I Верификация программ: состояние, проблемы, экспериментальные результаты. I Maksymets, A.N. UDC 51.681.3 УДК 51.681.3 Prombles in programming 2013; 4: 53-63 Представлен углубленный обзор проблем верификации программного обеспечения. Рассмотрены методы верификации реактивных и функциональных систем. Даны основные определения для представления и анализа программ. Приведено краткое описание методов верхней и нижней аппроксимации.Prombles in programming 2013; 4: 53-63 PROBLEMS IN PROGRAMMING ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ ПРОБЛЕМИ ПРОГРАМУВАННЯ 2025-04-16 Article Article application/pdf https://pp.isofts.kiev.ua/index.php/ojs1/article/view/741 PROBLEMS IN PROGRAMMING; No 4 (2013); 53-63 ПРОБЛЕМЫ ПРОГРАММИРОВАНИЯ; No 4 (2013); 53-63 ПРОБЛЕМИ ПРОГРАМУВАННЯ; No 4 (2013); 53-63 1727-4907 ru https://pp.isofts.kiev.ua/index.php/ojs1/article/view/741/793 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-16T13:52:57Z
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. I
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. I
title_short	Verification of programs: status, problems and experimental results. I
title_full	Verification of programs: status, problems and experimental results. I
title_fullStr	Verification of programs: status, problems and experimental results. I
title_full_unstemmed	Verification of programs: status, problems and experimental results. I
title_sort	verification of programs: status, problems and experimental results. i
title_alt	Верификация программ: состояние, проблемы, экспериментальные результаты. I
description	Prombles in programming 2013; 4: 53-63
publisher	PROBLEMS IN PROGRAMMING
publishDate	2025
url	https://pp.isofts.kiev.ua/index.php/ojs1/article/view/741
work_keys_str_mv	AT maksymetsan verificationofprogramsstatusproblemsandexperimentalresultsi AT maksymetsan verifikaciâprogrammsostoânieproblemyéksperimentalʹnyerezulʹtatyi
first_indexed	2025-07-17T09:58:32Z
last_indexed	2025-07-17T09:58:32Z
_version_	1850410429648470016
fulltext	Верифікація програм © А.Н. Максимец, 2013 ISSN 1727-4907. Проблеми програмування. 2013. № 4 53 УДК 51.681.3 А.Н. Максимец ВЕРИФИКАЦИЯ ПРОГРАММ: СОСТОЯНИЕ, ПРОБЛЕМЫ, ЭКСПЕРИМЕНТАЛЬНЫЕ РЕЗУЛЬТАТЫ. I Представлен углубленный обзор проблем верификации программного обеспечения. Рассмотрены мето- ды верификации реактивных и функциональных систем. Даны основные определения для представле- ния и анализа программ. Приведено краткое описание методов верхней и нижней аппроксимации. Введение Тематика данной статьи, как видно из названия, касается проблемы верифика- ции программного обеспечения. Верифи- кация программ – один из самых трудных (если не самый трудный) этапов разработ- ки программного обеспечения. Трудность данного этапа состоит в том, что от разра- ботчика, кроме знаний программистского характера, требуются знание и владение методами современной алгебры, логики, комбинаторики, теории чисел и других смежных областей. Кроме данных субъек- тивных факторов имеются и объективные факторы, связанные с тем, что в настоящее время имеющиеся методы верификации не находятся на достаточном уровне разви- тия, позволяющим верифицировать систе- мы индустриальных размеров. Сложность программного обеспечения постоянно су- щественно возрастает, а методы его анали- за отстают. Когда речь идет о методах вери- фикации и обоснования программного обеспечения, то имеются в виду прежде всего формальные методы. К данным ме- тодам в последнее время наблюдается повышенный интерес, поскольку опыт разработчиков программного обеспечения показывает, что из 5-ти, 6-ти инвестируе- мых проектов на рынок попадает один, максимум два программных продукта. Причем характерной особенностью дан- ных продуктов является то, что они по- строены на хорошей теоретической основе с обоснованием каждого шага разработки. Последнее обстоятельство позволяет ви- деть перспективы дальнейшего развития данного программного продукта или всей системы в целом, направления этого раз- вития, цели и задачи, решаемые с его по- мощью. Программные системы на сего- дняшний день делят на два класса: класс функциональных систем и класс реактив- ных систем. К первому классу относятся системы, которые должны работать в ко- нечном времени и имеющие вход и выход (т. е. реализуют вычисление некоторой функции), а ко второму – системы, кото- рые должны работать потенциально бес- конечное время, реагируя в процессе свое- го выполнения на внешние и внутренние раздражители. К сожалению, методы ве- рификации свойств первых систем совер- шенно не применимы к верификации свойств вторых систем, что привело к то- му, что для обеих классов разрабатывают- ся разные методы. Исследования в области формаль- ных методов верификации идут в основ- ном в двух направлениях: 1) дедуктивная верификация или доказательство теорем [1–3]; 2) алгоритмическая верификация с помощью разрешающих процедур, по- добных процедурам проверки выполни- мости логических формул на модели [4, 5], символического моделирования [6] или символическое выполнение траекто- рий [7]. Краткий обзор методов верификации Методы верификации реактивных систем. Одним из наиболее важных и пер- спективных методов верификации реак- тивных систем является метод проверки на Верифікація програм 54 модели. Суть этого метода состоит в том, что верифицируемая система пред- ставляется в виде математической моде- ли, а ее ожидаемые свойства в виде формул подходящего формального логи- ческого языка. Процесс верификации сво- дится к проверке формул спецификации на модели системы. Если процесс провер- ки прошел успешно, то на данной модели ошибки в реальной системе на обнаруже- но (это не означает, что они в ней отсут- ствуют), в противном случае обнаружива- ется ошибка и, что очень важно, система верификации генерирует путь, ведущий к данной ошибке. Важным преимуще- ством этого метода является его автома- тическое выполнение, что привело к то- му, что многие этапы верификации для многих формальных логических языков превратились в стандартные процедуры и успешно используются в фирмах, кото- рые разрабатывают не только программ- ное обеспечение, но и микропроцессор- ную технику (например, AMD, IBM, Intel) [8]. Кроме того, данный метод приме- ним к системам по размерам близким к индустриальным, благодаря манипуля- циям с моделью, уменьшающих число ее состояний. В качестве математической модели выбирается модель конечного автомата, работающего со словами бесконечной дли- ны. Как правило это конечные автоматы Бюхи или обобщенные автоматы Бюхи (автоматы Мюлера). А в качестве фор- мального логического языка выбираются языки линейной темпоральной логики [9] или более общие языки (язык ветвящего- ся времени CTL , или его обобщение CTL и т. п.). Выбор автоматной модели объяс- няется тем, что как сама модель, так и спецификация реальной системы пред- ставляются в виде конечного автомата Бюхи. Для языков, распознающих этими автоматами, разрешимы многие важные свойства, в частности, свойство включения одного языка в другой и свойство пустоты языка. А эти свойства позволяют эффек- тивно выполнять верификацию специфи- цированных свойств на модели системы. Благодаря разрешимости проблем вклю- чения языков и пустоты языка для ко- нечных автоматов над деревьями, метод верификации на модели расширяется на спецификации в языках логик ветвящего- ся времени (CTL , CTL ). Кроме чисто ав- томатных методов с успехом использу- ются и методы базирующиеся на свой- ствах частичных порядков, а также на символическом выполнении [7]. Описанию данной техники посвя- щены монографии [10, 11]. Второй широко используемой ма- тематической моделью являются сети Петри (СП) и их модификации: цветные, временные, гибридные СП. Эти модели наиболее адекватно представляют парал- лельные и распределенные системы. На тему СП имеется обширная литература, среди которой отметим наиболее извест- ные монографии [11–13]. Методы верификации функцио- нальных систем. Если верификация реак- тивных систем сводится к разрешимым свойствам теории конечных автоматов, то верификация функциональных про- грамм сводится к проблеме поиска доказа- тельства теорем в языках программных динамических логик или языке предика- тов первого порядка. Одним из первых языков программных логик был язык, предложенный Хоаром [14] и названный в его честь логикой Хоара. Основу метода Хоара составляют методы поиска и гене- рации инвариантов программных циклов с последующим использованием дедук- тивных методов доказательства утвер- ждений (теорем) о свойствах программы. Этот метод является и на сегодняшний день основным при верификации про- граммных систем функционального типа. Под проблемой (частичной) верификации систем функционального типа понимает- ся проблема, состоящая в том, чтобы по заданным высказываниям  и  о про- грамме P доказать истинность высказы- вания  на значениях выходных пере- менных программы P при условии, что значения ее входных переменных удовле- творяю т высказыванию  . Решение этой проблемы достаточно сложно и требует тщательного анализа программы, однако оно может быть суще- Верифікація програм 55 ственно облегчено, если для заданного состояния программы известны ее инва- рианты, т. е. такие утверждения, которые истинны всякий раз при прохождении процесса вычислений через это состоя- ние. Использование инвариантов при ве- рификации сводится к проблеме поиска инвариантных соотношений для заданной конструкции программы (скажем, инвари- анты цикла), а затем доказать, что из по- строенного множества соотношений сле- дует нужный предикат (постусловие), наличие которого гарантировало бы пра- вильность работы программы. За мето- дами решения данной проблемы закрепи- лось название методов потокового ана- лиза программ. Возникновение этих мето- дов связано с практической деятельностью в программировании и прежде всего с со- зданием качественного и надежного про- граммного обеспечения современных вы- числительных систем. Исторически первым методом по- токового анализа считается интерваль- ный метод, предложенный Коком, Швар- цем [15] и развитый впоследствии Аллен [16] и другими авторами. Суть данного метода сводится к представлению управ- ляющего графа программы множеством интервалов, при котором с каждым интер- валом ассоциируется некоторая локальная информация. По множеству интервалов строится новый производный граф, кото- рый снова представляется своим мно- жеством интервалов и т.д. до тех пор, по- ка он не стягивается к одной единствен- ной вершине (в этом случае исходный граф называется сводимым). Информация, сопоставленная этой единственной вер- шине, представляет собой глобальную информацию о программе в целом. Затем эта информация распространяется на ин- тервалы с помощью обратного процесса. В начале 70-х годов определился новый подход к анализу потоков дан- ных, предложенный независимо Летичев- ским [17] и Килдаллом [18]. Килдалл рас- смотрел задачу поиска в программах ин- вариантных соотношений вида 0=r , где r – переменная, а 0 – константа. В итер- ативном методе Килдалла инварианты и их последовательные приближения рас- сматриваются в виде элементов полуре- шеток, а поиск инвариантов для про- стейших фрагментов программы – ли- нейных участков – сводится к вычисле- нию значения функции, называемой функцией поиска инвариантов. Эта функ- ция по линейному участку и множеству соотношений на его входе строит некото- рое множество соотношений на выходе данного линейного участка. Килдалл де- тально исследовал случай, когда функция поиска инвариантов является дистрибу- тивной относительно основной операции полурешетки, предложил алгоритм и ал- гебраическую трактовку поиска такого рода соотношений. Вскоре после выхода в свет рабо- ты Килдалла, Кам и Ульман [19], критиче- ски рассмотрев подход Килдалла и его ал- горитм, заметили что этот алгоритм дает полные множества соотношений только лишь в абсолютно свободных алгебрах, т. е. когда не учитываются никакие свой- ства операций алгебры данных про- граммы. Было показано, что генерация полных систем соотношений вида cr = , где c – константа, невозможна, если заме- нить требование дистрибутивности требо- ванием монотонности функции поиска ин- вариантов. Если не предполагать алгебру данных абсолютно свободной, то дистри- бутивность функции поиска вариантов, вообще говоря, не имеет места и множе- ства инвариантов, получаемые с помощью алгоритма Килдалла, не являются полны- ми. Кам и Ульман детально исследовали свойства алгоритма Килдалла в случае монотонной функции, установили нераз- решимость задачи построения полной си- стемы инвариантов в общем случае и предложили некоторое усовершен- ствование алгоритма Килдалла. Также до- казано, что как алгоритм Килдалла, так и предложенный ими алгоритм дает един- ственное, хотя и отличное от полного множество инвариантов. В работах как Килдалла, так и Кама, Ульмана рассматривались задачи одностороннего анализа потока данных, т. е. задачи, в которых свойства состояния программы определяются исключительно свойствами его предшественников (прямая Верифікація програм 56 задача потокового анализа) или, наоборот, только свойствами его наследников (об- ратная задача потокового анализа). В.Н. Касьянов [20] рассмотрел более об- щую задачу потокового анализа, в которой имеются зависимости свойств состояний и их наследников друг от друга. Более общая постановка задачи поиска инвариантных соотношений сде- лана А.А. Летичевским [21], где предла- галось генерировать инвариантные соот- ношения типа равенств, неравенств, ква- зиравенств и квазинеравенств с учетом свойств алгебры данных, над которой ра- ботает рассматриваемая программа. Поз- же были разработаны методы верхней и нижней аппроксимации для генерации инвариантных соотношений, а также и соответствующие данным методам алго- ритмы. Эти алгоритмы дают полные мно- жества инвариантов типа равенств tt = , где tt , – выражения составленные из переменных, констант и операций алгеб- ры данных, для программ над такими алгебрами данных как векторные про- странства, свободные абелевы группы и коммутативные полугруппы, а также и для абсолютно свободных алгебр. По- следняя из алгебр тесно связана с поняти- ем логико-термальной эквивалентности схем программ над памятью. Детальное исследование методов поиска инвариан- тов для программ над абсолютно свобод- ной алгеброй данных выполнено С.Л. Кривым [22] и В.К. Сабельфельдом [23]. В результате, на базе методов потоково- го анализа, построены полные системы преобразований для такого класса про- грамм относительно логико-термальной эквивалентности, введенной В.Э. Итки- ным [24]. Важный практический и теорети- ческий шаг в развитии методов поиска инвариантов внесли Халбвош и Куазо [25], рассмотревшие задачу поиска инва- риантов типа линейных равенств и нера- венств. Они, используя методы линей- ной алгебры и линейного программиро- вания, предложили алгоритмы генерации инвариантных соотношений такого типа. Эти алгоритмы генерировали хотя и не- полные, но достаточно богатые множества инвариантов, чем существенно расшири- ли сферу применения методов потоково- го анализа программ. Дальнейшее разви- тие данный подход получил в методе абстрактных интерпретаций программ с последующим применением методов ма- тематического программирования (в час- тности, линейного программирования) [26]. Дальнейшее развитие методы по- токового анализа нашли при анализе про- грамм, алгебры данных, являющихся ком- мутативными кольцами или полями. Раз- работка алгоритмов поиска инвариантов для таких программ дает возможность оптимизировать и частично верифициро- вать многие программы вычислительной математики. Основная трудность – это вы- числительная сложность алгоритмов ре- шения основных задач поиска инвариан- тов в программах над такими алгебрами. Для того, чтобы получать более или менее практичные алгоритмы, необ- ходимо ограничивать степень полиномов (или степень инвариантов). Эти ограниче- ния, вообще говоря, хотя и существенные, но на практике вполне удовлетворитель- ны, так как в большинстве случаев до- статочно ограничиться инвариантами ма- лых степеней. Так задача генерации инва- риантов в виде полиномов частично была решена Мюллером и Сайдлом [27] для ограниченных степеней инвариантов. Отметим одно интересное исполь- зование методов потокового анализа в со- четании с методами верификации про- грамм путем символического выполнения [28]. Они использовались в индуктивном методе диалогового синтеза инвариантных утверждений в заданных точках про- граммы, суть которого состоит в после- довательном объединении и ослаблении предикатов, генерируемых при прохож- дении символического выполнения через эти точки. В настоящее время в области разви- тия методов потокового анализа имеется заметный прогресс, связанный с получени- ем эффективных алгоритмов, обобщаю- щих как алгоритмы Килдалла, Кама и Ульмана, так и другие [29]. Верифікація програм 57 Как уже отмечалось, важность раз- вития методов потокового анализа про- грамм заключается прежде всего в их практической ценности. На базе алгорит- мов потокового анализа разработаны мно- гие алгоритмы оптимизации. Среди них, в первую очередь, стоит отметить алгорит- мы поиска и удаления избыточных выра- жений, алгоритмы оптимального распре- деления регистров, редукции программ и алгоритмов с учетом дополнительной ин- формации (задача смешанных вычислений [30]), оптимизации процедур с учетом входа и выхода, введение дополнительных точек входа в процедуры и т. д. Можно рассматривать также и об- ратную задачу: по имеющимся входному предикату (предусловию) и выходному предикату (постусловию) синтезировать программу, входные данные которой удо- влетворяют предусловию, а выходные данные – постусловию. Такую постановку задачи и некоторые подходы к ее решению можно найти в книгах Абрамова С.А. [31] и Е. Дейкстры [32]. Необходимые понятия и определения U -Y -схема программы над па- мятью. Понятие схемы программы, рас- сматриваемое в этом разделе, представляет собой наиболее распространенную мате- матическую модель программы, которая получается, если абстрагироваться от кон- кретной информационной среды, над ко- торой она работает. Пусть D – некоторое множество, на котором определены операции сигнату- ры  , предикаты сигнатуры  и в кото- ром принимают свои значения переменные из конечного множества },,{= 1 mrrR  (память). Пара ),( D представляет собой универсальную  -алгебру, которая будет называться алгеброй данных, а частичное, вообще говоря, отображение вида DRb : – состоянием памяти. Множе- ство всех состояний памяти B будем называть информационной средой. Обозначим ),( RT  –  -алгебру термов над R . Отображение b можно продолжить на все множество ),( RT  , если положить ))(,),((=)),,(( 11 mm rbrbtrrtb  . При этом, если ),1,2,=()( mirb i  неопределенно, то левая и правая части считаются неопределенными, а равенство двух выражений истинно тогда и только тогда, когда обе части принимают одина- ковые значения или обе не определены. Рассмотрим множество выражений вида ),,( 1 nttu  , где u – символ n -арного предиката из  , а ),(,,1 RTtt n  . Каж- дое такое выражение определяет преди- кат на множестве B . Значение этого предиката при заданном состоянии памя- ти Bb определяется как )(),,( 1 bttu n ))(,),((= 1 ntbtbu  . Пусть ),,( RU означает множество всех таких выраже- ний, U – множество пропозициональных булевых функций от выражений из ),,( RU . Элементы множества ),,( RU будем называть базовыми условиями над памятью R , a элементы множества U – элементарными условия- ми над памятью R . Оператором присваивания назы- вается выражение вида: ))(:=,),(:=(=))(:=(= 11 rtrrtrrtry mm , где ),,(= 1 mrrr  , a )(,),(1 rtrt m ),( RT  , Rrr m ,,1  . Каждый оператор присваивания y задает некоторое преоб- разование на множестве B . Преобразова- ние, выполняемое y на B , определяется равенством bby =)( , где       },,{если),( },,{если),( =)(= 1 1 mii mii rrrrb rrrtb byb   , где mi ,1,2,=  . Если nyyyg  21= – произведе- ние операторов присваивания, то ему со- ответствует преобразование gy , равное последовательной суперпозиции преоб- разований, соответствующих операторам Верифікація програм 58 nyyy ,,, 21  . Пусть ),( RY означает мно- жество всех операторов присваивания. Элементы данного множества будем назы- вать базовыми операторами. Пара )),(),,,((  RYRU назы- вается стандартным базисом над памятью R , определенным сигнатурой ),(  . Ес- ли ),(),,,(  RYYRUU , то стан- дартной U -Y -схемой программы над па- мятью R (или просто U -Y -схемой про- граммы) называется множество состояний A схемы программы вместе с множеством переходов AYFUAS  )( и двумя выделенными состояниями: начальным 0a и заключительным a , где )(YF означает множество всех слов в алфавите Y . Слова в алфавите Y , т. е. композиции базовых операторов, будем называть элементарны- ми операторами. Пусть Scyudbyua ),,,(),,,,( 11 . Если da = , a cb = или 1= yy  , то состоя- ние a называют ветвлением, если же cb = , а da = или 1= yy  , то состояние b называют слиянием. Если Sbyua ),,,( , то говорят, что данный переход ведет из состояния a в состояние b . Состояниe 0a характери- зуется тем, что в S нет ни одного перехо- да, ведущего в 0a . Путем ),( bal , ведущим из состояния a в состояние b , длины n называется последовательность состояний baaaa n =,,,= 121  , связанных перехо- дами niayua iiii ,1,2,=),,,,( 1  . При этом путь из состояния a в состояние b назы- вается линейным участком, если для всех ni 1,2,...,= в множестве переходов S име- ется единственный переход, ведущий из состояния ia в 1ia . Состояние a называ- ют входом линейного участка, а состояние b – выходом. Процесс выполнения U -Y -схемы программы при заданном начальном со- стоянии памяти Bb 0 – это последовате- льность пар вида ),( 11 ba , ),( 22 ba ,…, …, ),( nn ba , где ,,=,= 0101 Aabbaa i  Bbi  , 1,2,=i и для всякой пары ),( 1ii aa состояний U -Y -схемы програм- мы в множестве S есть переход ),,,( 1iiii ayua такой, что 1=)( ii bu и )(=1 iii byb  . Процесс выполнения U -Y - схемы программы называется терминаль- ным, если он конечен и последняя пара имеет вид ),( ba , где a –заключительное состояние. U -Y -схема программы вместе с интерпретацией предикатов и заданным начальным состоянием памяти Bb 0 называется U -Y -программой. Для представления U -Y -схем про- грамм в памяти вычислительной машины удобно пользоваться управляющим гра- фом или регулярными выражениями ал- гебры алгоритмов. При представлении U -Y -схем программ над памятью управляющими графами с каждой U -Y - схемой программы связывается орграф ),(= EAG , называемый управляющим графом, дуги которого помечены следую- щим образом: если Sbyua ),,,( , то Eba ),( и помечено парой yu/ , a =)( 0aPr и =)( aPs . Помимо представления U -Y -схем с помощью управляющих графов суще- ствуют и другие способы представления. Пример. U -Y -программа умно- жения целых положительных чисел x и y посредством сложения – УМН ( yx, ) с результатом z . Текстовое представление U -Y -программы УМН ( yx, ) имеет вид: УМН( yx, ) xu := 0:=z while 0=u do 1:= uu ; yzz := ; end while А представление в виде управля- ющего графа U -Y -программы УМН( yx, ) показано далее на рисунке. Верифікація програм 59 Рисунок Инварианты в состояниях U -Y -программ Пусть A – U -Y -схема программы над памятью R , интерпретированная на области данных D (U -Y -программа), и L – язык, в котором записываются утвер- ждения о свойствах информационной сре- ды B . Относительно L будем предпола- гать, что всякое его предложение (на- зываемое также условием) может быть выражено формулой )(r языка исчисле- ния предикатов первого порядка, содер- жащей свободные переменные из кортежа ),,(= 1 mrrr  и интерпретированной на области данных D . Сигнатура этого исчисления содержит все символы сиг- натур  и  . Пусть )(ru – некоторое условие из L . Определение. Условия )(r из L называется инвариантом состояния а U -Y -программы A относительно усло- вия )(ru , если оно истинно при каждом прохождении состояния a в процессе вы- полнения программы A для тех и толь- ко тех начальных состояний памяти из B, на которых истинно условие )(ru . Усло- вие )(ru называется начальным. Если оно тождественно истинное на D , то )(r бу- дем называть просто инвариантом состоя- ния a . Содержательно инвариант )(r со- стояния a относительно условия )(ru ха- рактеризует множество BaB )( состо- яний информационной среды, дости- гающих в состоянии a заданной U -Y -программы на допустимых путях, начинающихся в удовлетворяющих нача- льному условию )(ru состояниях памяти. Схема построения множества )(aB следу- ющая. Строится множество S всех допу- стимых путей из 0a в a , реализующихся для начальных состояний из ÂuB (ха- рактеристическое множество условия )(ru ). По каждому пути ),(),,(,),,(= 1100  kkkk bababas  , где * 1 =0,> aak k , восстанавливается его операторная история – последовательность kyy ,,0  операторов, отмечающих пере- ходы на данном пути. Рассматривая за- тем композицию ks yyyy  10= (а это, как нетрудно видеть, также оператор присваивания над R ) строим множество )(= us ByB . После чего искомое множе- ство )(aB определяется как uB . Эта схе- ма, однако, неконструктивна, как в силу нерекурсивности множества S , так и в силу того, что множества вида sB могут не являться характеристическими для условий языка L . Выходом из этого по- ложения является как аппроксимация множества S некоторым объемлющим множеством путей S  , которое хотя и содержит "лишние" (недопустимые) пути, но устроено проще, так и аппроксимация множеств вида sB их подмножествами sB  – характеристическими для некоторых условий из L . Обе аппроксимации ведут к уменьшению множества )(aB , так как уменьшается каждый член пересечения s Ss B  и добавляются новые его члены. С учетом сужения множества )(aB c не- конструктивного s Ss B  до некоторого его приближения снизу можно говорить о максимальном инварианте состояния a как об условии )(r языка L таком, что (à)BBu  и для всякого другого инва- рианта )(r имеет место )()( rr  , где  означает отношение "быть след- ствием". Построение инвариантов осуще- Верифікація програм 60 ствляется генератором инвариантов в языке L . Понятие генератора включает в себя три компоненты: функцию :ef LYUL  – "эффект оператора", стру- ктуру полурешетки на множестве условий из L и описание итерационного алго- ритма. Функция ef по условиям u и u из L , истинным перед выполнением опе- ратора Yy , строит условие ),,( yuuef  , истинное на преобразованном состоянии памяти. Иногда будем рассматривать бо- лее простой вариант функции ef , когда в числе ее аргументов нет условия u (cуже- ние ),( yuuef  до )),( yuef , обуславливаю- щего переход yu/ . Заметим, что из опреде- ления функции ef вытекает, в частности, ее монотонность по первому аргументу, если множество условий N является ло- гическим следствием множества N  , то ),,( yuNef – логическое следствие ),,( yuNef  . Операция  взятия нижней грани на множестве условий языка L , вообще говоря, отличается от конъюнкции усло- вий. Если условиться называть множество условий, сопоставленных состояниям, разметкой, то итеративный алгоритм, от- талкиваясь от начальной разметки cостоя- ний (когда отметка 0a есть условие )(ru , а отметки остальных вершин – тождествен- но истинные условия), строит последова- тельность уточняющих разметок вплоть до получения некоторой стабильной размет- ки, которая и соответствует системе инва- риантов. Рассмотрим как осуществляется итерационный шаг. Итак, пусть задана текущая разметка состояний YU  - программы, LaInv )( – текущая отметка состояния a и {0,1}: Vz – функция, позволяющая отделить состояния с об- новленными отметками от остальных. Ал- горитм завершает работу, если 0)=)()(( azVa . Если же это условие не выполняется, то выбирается a такое, что 1=)(az . Затем для каждого перехода из этого состояния (их может быть один или два) строим уточнения. Уточнение для перехода ),,,( ayua  , отмеченного па- рой yu/ , состоит в том, что вычисляется эффект )),(( yaInvef , а затем нижняя грань )()),(( aInvyaInvef  и, наконец, если эта нижняя грань отлична от )(aInv  , то )(az  полагается равным 1. Уточнение перехо- дов, исходящих из состояния a , сопро- вождается изменением )(az c 1 на 0 . Описав итерационный шаг, общий для всех алгоритмов рассматриваемого класса, отметим, что в определенных си- туациях в состояниях-ветвлениях уточне- ние производится не по двум переходам, а лишь по одному. Для этого требуется, чтобы условие u или u , определяю- щее выбор альтернативы в ветвлении, было следствием текущей отметки )(aInv . Завершимость итерационного процесса обычно гарантируют условиями обрыва убывающих цепей в полурешетке языка L , что, может сказываться на качестве функции ef . Если описанный алгоритм завер- шился, то функция Inv дает совокупность инвариантов в состояниях U -Y -про- граммы. Эту совокупность будем также обозначать }{ aN , где Aa . Перейдем к более традиционной теоретико-множественной терминологии, принятой в теории программных ин- вариантов. Поскольку N и ),,( yuNef представляют некоторые предикаты на множестве D , то их можно рассматривать как отношения на D , определяемые этими предикатами. Тогда булеан )(LB удобно представлять в виде решетки относительно теоретико-множественных операций пере- сечения и объединения, которая содержит нуль  и единицу L . Выражения ),,()(),,( yuNefyuNef  в этом случае понимаются как пересечение (объедине- ние) соответствующих отношений на D , a то, что множество ),,( yuNef является ло- гическим следствием множества формул ),,( yuNef  – как теоретико-множествен- ное включение ),,(=),,( yuNefyuNef  . В дальнейшем будем следовать данным обо- значениям. Верифікація програм 61 Число различных возможных путей в программе (при наличии в ней хотя бы одного цикла) может быть бесконечным и тогда процесс построения условия состоя- ния a тоже может стать бесконечным. Тем не менее, пусть kaa ,,1  – все состояния U -Y -программы A , связанные перехода- ми ),,,( ayua iii с состоянием a и iN – множество инвариантов состояния ia от- носительно некоторого условия. Тогда, очевидно, что ),,( 1= iii k i yuNef будет инва- риантом состояния a относительно того же начального условия. Этот простой факт служит отправной точкой для построения двух итеративных методов генерации ин- вариантов [21, 33]. В первом из них, называемом мето- дом нижней аппроксимации (МНА), ите- ративный процесс задается рекуррентным соотношением ,,0,> ),,,(= 1)( ),,,( )( Aaan yuNefN n a Sayua n a      (1) а начальное приближение }{ (0) aN – равен- ствами }{= (0) 0 uN a и =(0) aN для 0= aa  . Из свойства монотонности функции ef следует, что  (1)(0) aa NN независимо от состояния a . Указанный итеративный процесс может завершиться через конеч- ное число шагов в результате стабилиза- ции последовательностей )(i aN для всех Aa или может продолжаться бесконеч- но, но достоинство этого метода, состоит в том, что, не дожидаясь стабилизации про- цесса вычислений, их можно прервать на любом шаге генерации, поскольку всякое множество )(n aN включается в множество инвариантов состояния a . В другом методе, называемом ме- тодом верхней аппроксимации (МВА), итеративный процесс задается рекур- рентным соотношением   ,,0,> ,,, = 1)( ),,,( 1)()( Aaan yuNef NN n a Sayua n a n a                (2) а начальное приближение определяется равенством }{= (0) 0 uN a и некоторой со- вокупностью простых путей, покры- вающих все множество состояний U -Y -программы A . Вычисление началь- ного приближения осуществляется вдоль этих путей, начиная с (0) 0a N : если для неко- торого Aa  уже известно (0) a N  , переход ),,,( ayua  принадлежит одному из путей заданной системы, а (0) aN еще не известно, то полагаем ),,(= (0)(0) yuNefN aa  . Из соот- ношения (2) видно, что для всякого Aa имеют место включения  (1)(0) aa NN и, следовательно, искомая совокупность инвариантов может быть получена толь- ко после стабилизации итеративного про- цесса. Поскольку процесс поиска инва- риантов может быть бесконечным, это яв- ляется недостатком метода МВА, который, однако, в случае результативного завер- шения генерирует более полные системы инвариантов чем метод МНА. Исследование методов генерации инвариантов показывает, что конечность процесса поиска инвариантов тесно связа- на с языком условий L . Наиболее распро- страненными языками условий являются языки типа равенств и неравенств, так как практически любой язык программирова- ния содержит предикаты равенства и нера- венства. Разработка методов поиска инва- риантов для этих языков сталкивается со значительными трудностями. Действи- тельно, формулы (1) и (2) предполагают алгоритмическое и, по возможности, эф- фективное решение задач пересечения множеств соотношений, проверки соот- ношения на предмет того, что оно яв- ляется следствием заданного множества соотношений и т. д. и т. п. Решение пере- численных задач уже для этих языков тре- Верифікація програм 62 бует привлечения достаточно сложных ме- тодов современной общей алгебры. Выводы В данной работе, являющейся пер- вой частью обзора методов верификации и их приложений, представлены краткие сведения истории развития и актуальных задач проблемы верификации программ. В них рассмотрена проблематика верифика- ции реактивных и функциональных си- стем, где указано место предложенного подхода в формальных методах верифика- ции. Приведены основные понятия, ис- пользуемые в этой области, а также опи- сываются свойства введенных понятий вместе с обоснованием их правильности. Намечаются дальнейшие пути развития предлагаемых методов. В следующей статье будут более детально рассмотрены методы вери- фикации и их реализация применительно к конкретным программам над конкретными алгебрами данных. 1. Kaufmann M., Manolios P., Moore J.S. Computer Aidede Reasoning: An Approach, // Kluwer Academic Publishers. – 2000. – 212 p. 2. Nipkow T., Paulson L., Wenzel M. Isa- belle/HOL: A Proof Assistant for Higher Or- der Logic, // Springer Verlag. – 2002. – LNCS. – Vol. 2283. – P. 3–51. 3. Oppen D.C., Cook S.A. Proving Assertion About Programs that Manipulate Data Struc- tures // In Proceed. Of the 7-th Annual ACM Symposium on Theory of Computing (STOC 1975). – Aluquerque. – NM. – ACM Press. – 1975. – P. 107–116. 4. Clarke E.M., Emerson E.A. Design and Syn- thesis of Synchronization Skeleton Using Branching Time Temporal Logic. In D.C. Kozen, edit // Logic of Program Workshop. – Springer Verlag. – 1981. – LNCS. – Vol. 131. – P. 52–71. 5. Queille J.P., Sifakis J. Proving Specification and Verification of Concurent Systems in CESAR // In Proceed. of the 5–th Intern. Symposium on Programming. – Springer Verlag. – 1982. – LNCS. – Vol. 137. – P. 373–351. 6. Jones R. B. Simbolic Simulation Method for Industrial Formal Verification // Kluwer Aca- demic Publishers. – 2002. – 286 p. 7. Chou C. The Mathematical Foundation of Symbolic Trajectory Evaluation. In N. Halb- wacha and D. Peled, edit // Proc. of the 11–th International Conference on Compu- ter Aided Verification (CAV 1999). – Spring- er Verlag. – 1999. – LNCS. – Vol. 1633. – P. 196–207. 8. Ray. S. Scalable Techniques for Formal Veri- ficaton // Springer Science+Business Media. – 2010. – LLC. – P. 9–57. 9. Vardi M.Y., Wolper P. An Automata– theoretic Approach to Linear Temporal Logic // Logics for Concurrency: Structure versus Automata Springer Verlag. – 1966. – LNCS. – Vol. 1043. – P. 238–266. 10. Кларк E.M., Грамберг O., Пелед Д. Вери- фикация моделей программ: Model Chcking. – M.: МЦНМО, 2000. – 416 c. 11. Карпов Ю.Г. MODEL CHECKING. Вери- фикация паралелельных и распределенных программных систем. – Санкт–Петербург: БХВ–Петербург, 2010. – 560 с. 12. Jensen K., Kristensen L.M. Colored Petri Nets: Modelling and Validation of Concurent Systsems. Springer Verlag. – 2009. – P. 384. 13. Penczek W., Polrola A. Advanced in Verifi- cation of Time Petri Nets and Timed Automa- ta. Springer Verlag. – 2006. – P. 256. 14. Hoare C.A.R. An axiomatic basis of comput- er programming // CACM. –1969. – Vol. 12. – P. 576 –580. 15. Cocke J., Schwartz J.T. Programming Lan- guage and their Compilers // Courant Institute of Mathem. Sciences. – New York University. – 1970. – N.Y. – P. 3–21. 16. Аllen F.E. Interprocedural analysis // ACM SIGPLAN Notices. – 1976. – Vol. 6, N 7. – P. 23 – 31. 17. Летичевский А.А. Эквивалентность и оп- тимизация программ // Труды междунар. симпозиума по теоретическому про- граммированию. – Новосибирск, 1972. – С. 166–180. 18. Kildall G.A. A unified approach to prog- ram optimization // Conf. Rec. of ACM Symp. on Prince. of Program Languages, Boston, Massachusetts, Oktober 1–3, 1973. – P. 194–206. 19. Kam J.B., Ullman D.J. Monotone data flow analysis frame works // Acta Inform. – 1978. – Vol. 3. – P. 305–318. 20. Касьянов В.Н. Учет априорной информа- ции при анализе свойств состояний про- грамм // Математическая теория програм- мирования. – Новосибирск: ВЦ СО АН СССР, 1985. – С. 150–157. Верифікація програм 63 21. Годлевский А.Б., Капитонова Ю.В., Кри- вой С.Л. и др. Итеративные методы анали- за программ. Равенства и неравенства // Кибернетика. – 1990. – № 3. – С. 1–9. 22. Кривой С.Л. О поиске инвариантных со- отношений в программах. // Мате- матическая теория проектирования вычис- лительных машин. – Киев: ИК АН УССР. – 1978. – С. 35–51. 23. Сабельфельд В.К. Учет свойств операций при глобальном анализе свойств программ // Математическая теория програм- мирования. – Новосибирск: ВЦ СО АН СССР. – 1985. – С. 132–149. 24. Иткин В.Э. Логико–термальная эквивале- нтность схем программ // Кибернетика. – 1972. – № 1. – C. 5–27. 25. Cousot P., Halbwochs N. Discovery of Line- ar Restraints Among Variables of Program // Conf. Record of the 5–th Annual ACM Sym- posium on Princieples of Programming Lan- guages. – USA. – 1978. – P. 84–96. 26. Cousot P. Abstract Interpretation Based Formal Methods and Future Challenges // In- formatics LNCS. – Vol. 2000, 2001. – P. 138–156. 27. Muller–Olm M., Seidl H. Computing Inter- procedurally Valid Relations in Affine Pro- grams. // Symposium on Principles of Pro- gramming Languages, 2004. 28. Костырко В.С., Бакулин А.В. Об индук- тивном синтезе инвариантных утвержде- ний и функций программ // Кибернетика. – 1986. – № 1. – C. 18–24. 29. Karr M. Affine Relationships Among Varia- bles of a Program // Acta Informatica. – 1976. – № 6. – P. 133–151. 30. Годлевский А.Б., Кривой С.Л. Применение техники смешанных вычислений к постро- ению эффективных алгоритмов унифика- ции и приведения выражений // Тезисы докл. Всесоюз. конф. "Методы трансляции и конструирования программ". – Новоси- бирск, 1988. – С. 59–62. 31. Абрамов С.А. Элементы анализа про- грамм. – М.: Наука, 1988. – С. 129. 32. Дейкстра Э. Дисциплина программирова- ния. – М.: Мир, 1975. – С. 247. 33. Летичевский А.А. Об одном подходе к анализу программ // Кибернетика. – 1979. – № 6. – C. 1–8. Получено 07.03.2013 Об авторе: Максимец Александр Николаевич, аспирант. Место работы автора: Киевский национальный университет имени Тараса Шевченко. Тел: +38 050 9852274. E-mail: maksymets@gmail.com

Verification of programs: status, problems and experimental results. I

Institution

Ähnliche Einträge