Поиск инвариантов для программ с булевыми массивами тема автореферата и диссертации по математике, 01.01.09 ВАК РФ

¿изииБиъь <иъг>и.'г)ьт^зил иао-изм) ими^ьимизг'

ь'иьлгииэм-твг» ьд. ищвтгизиви-ил) ТПРЦЫТЪЬРГ» ьъизьбаэ

ргв оа

1 3 ЯИВ да

РСшцр^ (чрш^тОрп^ аач зг.бВ1.э.об

МпифшО^шй ЦрНЬО

ьъ^арьиъз11ьрь пгпъпи ртиааг> еилл^иггиьрп^ т^иад^ьрь ¿.штиг

ЦЧииОик}¡11ртор 1 гиО а. 01. 09

и итрЬСилф^ш^шО фршишршОгорх пО

рЫ|Сшйгф сффшЦшО иллгфВшСф илрЬ0ш(ипип1)»|шС

иЬг|11ш!}|1р

ЬрЬшО - 1096

ИНСТИТУТ ПРОБЛЕМ ИНФОРМАТИКИ И АВТОМАТИЗАЦИИ НАЦИОНАЛЬНОЙ АКАДЕМИИ НАУК РЕСПУБЛИКИ АРМЕНИЯ

На правах рукописи УДК 51.681.3.06

Костанян Армен Грачевич ПОИСК ИНВАРИАНТОВ ДЛЯ ПРОГРАММ С БУЛЕВЫМИ МАССИВАМИ

Специальность А.01.09 Математическая кибернетика и математическая логика

Автореферат диссертации на соискание ученой степени кандидата Физико-математических наук

Ереван - 1996

Работа выполнена в Ереванском государственном университете

Научные руководители: член корреспондент АН Украины.

доктор физико- математических наук.

профессор Летичевский A.A.

академик HAH Республики Армения.

доктор технических наук, профессор Шукурян Ю. Г.

Официальные оппоненты: доктор физико- математических наук.

профессор Заславский И. Д.

кандидат физико- математических наук.

доцент ТоноянР. Н.

Ведущая организация: Ереванский каучно-исследовательский

институт Математических Машин

') .,' 'J ¡Г 'i: ..:,!!' . ''

Зашита состоится ХС - 199^- г. в ——

часов на заседании специализированного совета 037 "Математическая кибернетика и информатика" в Институте проблем информатики и автоматизации Национальной АН РА по адресу : 375044. г. Ереван, ул. П. Севака. 1.

С диссертацией можно ознакомиться в научно-технической библиотеке института.

tZ. Q й%

Автореферат разослан-3-р-^ 1996г.

Ученый секретарь специализированного совета канд. эк. наук. ст. н. с. , Мелконян А. Е.

ОБЩАЯ ХАРАКТЕРИСТИКА РАБОТЫ

Актуальность темы. Одной из ключевых проблем теоретичес-ого и практического программирования является проблема ерификации. которая состоит в том, чтобы по заданным тверждениям ° и о о программе р доказать истинность р после ыполнения р при условии, что перед ее выполнением истинно

общем случае проблема эта алгоритмически неразрешима, а оиск решений в частных случаях требует глубокого предваря-ельного анализа. В работах Флойда и Хоара было показано, то верификация программы сводится к нахождению существенных нвариантов для определенных ее точек, то есть таких утвер-дений, которые выполняются всякий раз при прохождении через ги точки процесса вычисления.

А. А. Летичевским был предложен метод автоматического оиска инвариантов из текста программы с учетом структуры лгебры данных. В работах его учеников этот метод был рименен к ряду конкретных алгебр. Указанные исследования роводились для программ с простоя памятью.

В данной работе предлагается развитие метода автомати-эского поиска инвариантов применительно к программам с /левыми массивами, что принципиальным образом расширяет Зласть его применения. Последнее особенно актуально в зязи с получающими все более широкое распространение авто-атическими системами распознавания визуальных и речевых анных, составления экономических планов и расчетов, раз-1ботки игровых стратегий и т. д., использующими булевые ассивы больших размеров.

Цель работы. Целью диссертационной работы является юработка базовых алгоритмов для методов верификации и химизации программ, работающих с булевыми массивами. )лее конкретно

- построение математической модели для программ с г левы ми массивами;

- выбор представляющих практический интерес форм инва-тнтов;

- разработка алгоритмов поиска инвариантов заданной >рмы.

Методика исследований. Методологическим стержнем работы (ляется техника отыскания неподвижных точек систем функцио-

нальных уравнений, заданных на частично упорядоченных мно кествах. Применение этой техники основано на всесторонне! использовании понятий и методов теории множеств, абстрактно: и булевой алгебры.

Научная новизна. Построена математическая модель дл: программ с булевыми массивами в рамках которой разработан] методы автоматического поиска инвариантов определенны: типов. Это существенно расширяет класс программ, к которш можно применить имеющиеся методы верификации и оптимизации Описан класс линейных программ, допускающих эФФективну1 верификацию относительно условий, заданных в форме константны: равенств.

Практическая дэаность работы. Полученные в работе резуль таты могут быть использованы для создания автоматически: систем диагностики и оптимизации прикладного и системное программного обеспечения. Их можно использовать также дл, организации параллельных процессов обработки информации Результат по верификации линейных программ может послужит основой автоматического проектирования тестов для аппаратны: и программных средств. »

Аппгюбация работы и публикации. Основные положения : результаты работы обсуждались и докладывались на семинара: по теории автоматов и автоматизации программирования Институте кибернетики им. В. М. Глушкова АН Украины, на семи нарах по теоретическому программированию в Киевском и Ереван ском госуниверситетах. на Закавказской научно-техническо конференции молодых ученых и специалистов "Информатика вычислительная техника", на общем семинаре Института проблез информатики и автоматизации HAH Армении, на заседани Армянского Математического Общества.

По теме диссертации опубликованы 4 научные статьи.

Структура работы. Диссертационная работа состоит и введения, четырех глав', заключения и списка цитируемо литературы из 42 наименований. Объем работы составляет 7 страницы печатного текста.

СОДЕРЖАНИЕ РАБОТЫ

Высокие требования, предъявляемые к надежности прог-ммпого обеспечения приводят к необходимости стогого матема-ческого доказательства правильности программ. В зависимости категории ошибок, можно говорить о синтаксической и семан-ческой правильности. Вопросы распознавания синтаксической авильности хорошо исследованы в теории формальных языков, ачительно более сложной является задача установления *антической правильности, или, как принято говорить, эификации программы.

Исторически первой системой верификации явился метод дуктивных утверждений Флойда. Суть его состоит в следующем, эграмма в некоторых точках снабжается утверждениями относи-пьно состояния своих переменных, которые выполняются, когда равление достигает этих точек. Далее строится цепь имплп-ций, при помощи которой показывается, что из истинности одного условия следует истинность утверждения, приписанного эвой контрольной точке и т. д., из истинности утверждения, аписанного последней контрольной точке, следует истинность ¿одного условия. Опираясь на идеи Флойда, Манна предложил эмализм, дающий возможность свести отдельные этапы процесса жфикации к доказательству теорем в исчислении предикатов звого порядка.

Идеи Флойда и Манны нашли дальнейшее развитие в соматическом подходе, предложенном Коаром. В терминах ¡троенного им исчисления был сформулирован метод частичной >ификации структурированных программ. Хоар писал: "Прог-■ширование является точной наукой в том смысле, что | свойства программы и все последствия ее выполнения всяком данном оборудовании могут быть, в принципе, ¡едены из самого текста программы чисто дедуктивными ¡суждениями".

Наиболее ответственным моментом в процессе верификации всех указанных случаях является синтез индуктивных ¡ерждений. На основе расширения понятия индуктивного ¡ерждения было введено понятие инварианта, под которым гимается не зависящее от входных спецификаций условие, >ажающее фактическое отношение между переменными прог-шы. Помимо доказательства правильности, инварианты в

дальнейшем стали широко применяться и для доказательст! других утверждений о программах, а также для решения зад; оптимизации и синтеза. ,

Для поиска инвариантов Килдаллом был предложен итератш ный метод, получивший название метода глобального анали: потока данных. Суть его состоит в том, что на начальном ша! итерации контрольным точкам программы приписываются некоторь тривиальные инвариантные условия, которые усиливаются I последующих шагах с учетом преобразований, выполняемых процессе перехода из одной контрольной точки в другук Независимо от Килдалла, аналогичный метод был предложи А. А. Летичевским, где он был дополнен идеей учета свойсч алгебры данных, что позволяет получать более сильнь инварианты. В работах его учеников С. Л. Кривого, С. Г. Ракп и М. С. Львова были разработаны алгоритмы поиска инвар! антных равенств для абсолютно свободных алгебр, векторнь пространств, областей целостности; инвариантных равенств неравенств для линейных и нелинейных вычислений в упор; доченных полях. В связи с тем, что описание итеративно! метода и проводимые в его рамках исследования относили« исключительно к программам с просто? памятью, А. А. Лет1 чевскнм была поставлена задача их распространения на про1 раммы со структурированной памятью, что составляет содержанг дайной "работы. ■ 1,1 • 11

Для рассмотрений нами выбрана модель с двухкомпонент ной информационной средой, первую компоненту состояний коте рой образует набор значений переменных массивов, а вторую -набор значений простых переменных, используемых для индексацв массивов и называемых индексными. Вычисления над индексным переменными рассматриваются на Функциональном уровне поэтому алгебра индексов не уточняется, а для задания вычис лений над массивами использована булева алгебра. В рамка данной модели оказалось возможным проведение исследований е верификации линейных программ. Задача эта была предложен С. К. Шукуряном в рамках работ по автоматическому проектирс ванию тестов для вычислительных систем.

Работа состоит из введения, четырех глав и заключения.

Во введении дается обзор литературы и результатов относящихся к данной тематике, обосновываются актуальность

научная новизна и практическая ценность работы. Рассматривается краткое содержание работы по главам.

В первой главр определяется модель программ, обрабатывающих булевы массивы и описывается концепция итеративного поиска инвариантов.

Вводится понятие структуры данных, как отображения вида 5,- с—>о; где с — область расположения, ° -- область значений. Множество всех структур данных, расположенных на с и принимающих значения в обозначается гсс- со _

Считаются заданными два алфавита: алфавит 1 индексных переменных и алфавит х переменных массивов. Переменным ^ и сопоставляются области их значений и <гая:>о.

Первая задается как подмножество целых чисел, а вторая определяется как множество гсж^тсхэ, ю структур данных, расположенных на »««псхз и принимающих значения в ЕЧ0- 1 У. Область »»тсхз задается как множество целочисленных координатных наборов, длина которых совпадает с размерностью Вводятся обозначения к^ал о и <уахсх>*ххх<гыоо. МНОЖеСТВО ^лЛХЭ

изоморфно множеству гсхэ. еэ структур данных, расположенных на множестве «»илсхэ^хсс] | хех. свлэо-тсхэ компонент массивов и принимающих значения в Е. Элементы множеств «ал:" я <г<исю называются состояниями соответственно индексных переменных и переменных массивов.

Информационная среда в определяется как множество состояний вида ь=<5> 2>, где * и я состояния соответственно индексных переменных и переменных массивов. Подмножества множества в зазываются информационными множествами.

Для задания вычислений над информационной средой вводится понятие индексно-скалярной формулы — Формулы алгебры логики, построенной из индексных условий (условий, зависящих от гадексных переменных) и скалярных переменных. Последние записываются в форме где ? — набор индексных

выражений (выражений, зависящих от индексных переменных), 1ринимающий значения в . Определяется логическое

значение фсьэ, принимаемое индексно-скалярной формулой Ф на зостоянии информационной среды ь.

Вводится базис состоящий из множеств ° элементарных условий и * элементарных операторов. В качестве элементарных условий берутся индексно-скалярные формулы, а в качестве

элементарны! операторов — двухкомпонентные операторы вид. у»<». \>, где ^ и операторы преобразования состояни] соответственно индексных переменных и переменных массивов Оператор ^ определяется как множество одновременно выпол няемых присваивании вида а--т. где , г — индексно выражение; а оператор ® -- как множество одновременн< выполняемых присваиваний вида где — скалярная

переменная, V — индексно-скалярная формула. Значение опера тора у на состоянии ь=<*. определяется как состояни-

2'>вв такое, что г' есть состояние индексных пере менных, получаемое в результате применения оператора к = а — состояние переменных массивов, получаемое в результате применения оператора « к ь.

В качестве модели программы используется понятие интерпре тированной на множестве в схемы над базисом си. уэ Или и-*-схе мы. Схема эта задается четверкой с а. т, л"", а(1Ь # гдб а конечное множество состояний; т<=АхихУхА __ конечное множеств»

(О) <1>

переходов; » — начальное состояние; а — заключит ель ное состояние. Переход <»• у. а'>бТ записывается в вид. а иУу->*' и имеет следующую семантику: при выполнении услови. и программа переходит из состояния а в состояние а' и выполняе1 оператор у. При заданной интерпретации базовых условий 1 операторов на множестве в, и-*-схема называется и"у-программе: (поскольку булева алгебра фиксирована, для задания интерпре тации достаточно определения алгебры индексов). Для и-*-прог раммы А определяется частичное преобразование гАяа—вычис ляемое ею на множестве в.

Пусть а — и-*-программа; «иР- принимающие истннност ные значения на в условия, заданные в виде формул некоторого языка ь. программа а называется частично корректной относи тельно условий « и р, если сась^=1( гасю определено ] равно *>'3 ■* Предложенные Флойдом и Хоаром метод:

доказательства частичной корректности программ основаны а знании инвариантов для некоторых их"'состояний. Понятие эт определяется следующим образом.

| Пусть ва всех состояний информационной среды, с .которым: программа может оказаться в состоянии при начальны: состояниях среды, удовлетворяющих условию Формула р язык ь называется инвариантом состояния а относительно условия Л

ели ьев^ ксь5=1. Множество всех инвариантов состояния а тносительно л обозначается

Для сравнения элементов множества ь на нем вводится тношепие частичного порядка при котором , если ' р <р" сильнее р >. Задача поиска инвариантов формулируется ак задача отыскания достаточно больших по величине элементов ножеств I™для всех »«а.

Для ее решения, предлагается модификация итеративного етода, предложенного в *> для случая простых переменных, ыполнение шага итерации в указанной модификации сводится к

л

^строению значений функций р. ^ и I. Функция ьхиху—>ь

э ь-формуле р, выполняющейся в начале перехода, базовому

зловию " и базовому оператору у строит ^-формулу . выпол-

яющуюся в конце перегода; функция 1-2—по^ ^-формулам

, и р2 строит их нижнюю грань в Ц функция ¡-2—>ь по

-Формулам р4 и строит формулу р такую, что ^ 5 р и

^ ■» р-. В соответствии с терминологией статьи *> задача

^строения функции у называется задачей о соотношениях.

. л

адачи построения функций | и ! называются задачами о инимизации и о максимизации (аналогом задачи о минимизации *> является задача о пересечении). Каждая из перечисленных 1дач имеет множество возможных вариантов решения. Выбор >го или иного варианта ставится в зависимость от последующей шкретизации.

Во второй главе рассматривается решение задач, связанных итеративным поиском инвариантов для языка импликативных >рмул.

В параграфе 2.1 определяется конкретизация модели, ж которой в качестве базовых условий выбираются импли-1тивныб формулы, а качестве базовых операторов — элементные операторы, использующие скалярные формулы в правых ютях оператора преобразования массивов. Под скалярной >рмулой понимается индексно-скалярная формула, не содержащая щексных условий.

В параграфе 2.2 вводится язык ^ импликативных формул и ¡следуются его свойства. Элементами языка являются Формулы

Летичевский А. А. Об одном подходе к анализу программ. — Кибернетика. 1979, 6. с. 1-8.

вида & и«нк ■»■ юк1. где * — набор индексных переменных

1с« 1

нк&ч»л1:>, юк ~ скалярная формула. В такой Формуле множеств Н4. ..., н„ можно считать попарно непересекающимися, имеющим объединение, равное что позволяет говорить о разбв

ении, определяемом формулой р на множестве .

Теоремой 2.1 устанавливается, что язык ^ замкну относительно операций дизъюнкции, конъюнкции и отрицания В качестве следствия отсюда получается, что класс подмно жеств множества состояний информационной среды, являющихс областями истинности импликативных формул, образует булев алгебру множеств.

|> . I

Наряду с отношением при котором р - , если формула р сильнее формулы р. на множестве вводится также отношение при котором р р" , если разбиение, определяемое формулой р' является укрупнением разбиения, определяемого Формулой р Если р 5Т Р', то говорится, что формула р' является боле тотальной.1 чем формула р.

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

В параграфе 2.3 применительно к двум языкам — скалярны и импликативных формул, вводится понятие аппроксимации инфор мационных множеств. Аппроксимация множества определяете как формула, выполняющаяся на На множестве аппроксимаци й задается отношение порядка, при котором чем точне аппроксимация, тем больше величина формулы. Если при тако упорядочении существует наибольший элемент, то он называете наилучшей аппроксимацией множества Наилучшая аппроксимацв называется точной, если областью истинности соответствующе формулы является к. Теоремами 2.2 и 2.3 уставливается сущесч вование точной импликативной и наилучшей скалярной аппров симаций произвольного информационного множества.

В параграфе 2.4 излагается решение задачи о соотношения? Задача эта сводится к построению по импликативной формуле * базовому условию " и базовому оператору у, импликативне

аппроксимации множества «'»^ю, где *НЬеВ1 гсь:,-ись:)=1 К а гу — преобразование на множестве в, реализуемое оператором у.

Предлагается вариант решения данной задачи получаемый путем выбора точной импликативной аппроксимации множества , и выполнения над ней ряда преобразований, направленных на увеличение тотальности за счет не слишком значительного уменьшения величины. При этом возникает побочная задача построения по множеству м£*>а/аэ м скалярной Формуле '!! и базовому оператору у=<я. с однозначно действующим на м оператором скалярной аппроксимации множества где ,2>ев| ягсю.1. которая называется частной

задачей о соотношениях. Отмечается, что хотя существует принципиальная возможность построения наиболее сильного решения частной задачи о соотношениях на основании теоремы 2.3, однако сложность соответствующей формулы может оказаться слишком большой в связи с чем, задача эта требует проведения дальнейшего исследования с целью поиска решений менее сложных по объему и достаточно больших по величине.

В параграфе 2.5 исследуются задачи о минимизации и о максимизации. Задача о минимизации решается тривиально в форме наиболее сильного решения р»^ несмотря на то, что тотальность такой формулы может оказаться низкой. Возможность повышения тотальности предусматривается в процессе решения задачи о максимизации, которая сводится к построению по импликативным формулам рг1 и р2 импликативной формулы р такой, что р", ^ г £ В отличие от задачи о соотно-

шениях, здесь предлагается не готовое решения, а путь его построения, предполагающий выбор в качестве отправной точки импликативной формулы и предоставление возможности

увеличения ее тотальности вплоть до предела, определенного формулой . Реализация этой возможности осуществляется в результате ряда применений к формуле правила унификации. Для каждого такого применения существует определенная свобода выбора, в результате чего процесс повышения тотальности не является строго регламентированным.

В параграфе 2.6 рассматривается настроенный метод поиска инвариантов, при котором для некоторых состояний программы фиксируются определенные области значений индексных переменных

и ставится задача отыскания скалярных формул, выполняющихся в них. Иными словами, для таких состояний речь идет о поиске инвариантов, определяющих фиксированное разбиение на множестве указывается, что для достижения поставленной

цели достаточно в процессе решения задачи о максимизации соответствующими применениями правила унификации добиться нужного разбиения.

В третьей главе приводятся решения задач о соотношениях и о минимизации для языка шаблонов (монотонная зависимость их от входных условий, делает излишней решение задачи о максимизации).

В параграфе 3.1 определяется алгебра логики с аппроксимацией. получаемая путем добавления к множеству логических значений е.-|о. i ^ неопределенного элемента w. На расширенном множестве 2-jo. i, wj. вводится отношение аппроксимации с. при котором d с d', если d=w или d-d' (неопределенный элемент аппроксимирует все элементы, каждый из остальных элементов аппроксимирует только самого себя). Отношение 1 путем покомпонентного применения переносится на структуры данных, принимающие значения в е (в частности, на наборы элементов из ё>.

Для ^-местной Функции алгебры логики f: еп—>е определяется ее расширение до отображения ёп—>ё при помощи правила, полагающего гс*»-*«^ еслИ для каждого набора ««е", получаемого доопределением <», имеет место равенство fcoo=£ и ?cdD=wF в противном случае. Множество б вместе с расширенными Функциями алгебры логики, называется алгеброй логики с аппроксимацией. Алгебра эта является составной .частью систему .алгоритмических алгебр, введенной В. М. Глушковым.

Для данной алгебры доказываются две теоремы о суперпозиции. Теоремой 3.1 устанавливается, что суперпозиция расширенных функций алгебры логики аппроксимирует расширение суперпозиции этих функций. Для функции представленной в д. н. ф. ъ, теоремой 3.2 устанавливается, что заменой в D функций & и -1 их расширениями можно получить функцию ? тогда и только тогда, когда каждый максимальный интервал для Функции f содержится в покрытии ее носителя, определяемом формулой о. Данное обстоятельство, в частности, имеет место, если о является сокращенной д. н. ф. функции f.

В параграфе 3.2 строится алгебра частично определенных структур данных с помощью операции наложения и. Операция эта на множестве е определяется правилом аиесли и в противном случае. Далее путем покомпонентного применения она переносится на множество структур данных, принимающих значения в 2.

В параграфе 3.3 вводится язык шаблонов как язык формул вида £=<*• л>, где л£«ал:гэ, х — отображение, сопоставляющее каждому элементу из множества Л частично определенную структуру данных, расположенную на «»«осхэ. для г«=л значение л*23 можно рассматривать как разбиение множества «-»«ч^хэ на три непересекающиеся части — множества компонент массивов, равных соответственно о, 1 и Состояние информационной среды ь-<з. 2> определяется как удовлетворяющее шаблону если 2«д и хс^э с з (последнее требование означает, что структура данных = является доопределением частично определенной структуры данных

Теоремой 3.3 устанавливается, что язык шаблонов замкнут относительно операции конъюнкции; однако не замкнут относительно операций дизъюнкции и отрицания, если число компонент массивов больше единицы.

На множестве стандартным образом определяется отношение частичного порядка: чем сильнее формула, тем больше ее величина. Для шаблонов *«<и «'=<*'. Д'> утверждение равносильно тому, что и с л'Сгз для всех 2еЛ'.

В параграфе 3.4 рассматривается задача о соотношениях в следующей постановке. Даны шаблон ¿>. элементарные условие и и оператор у. Требуется найти шаблон такой, что с$сьэ=ись?=1, ь-=ьуз * Данная задача решается в двух

вариантах — наиболее сильном (теорема 3.4) и более слабом, но зато удобном в практическом осуществлении (теорема 3.5). Второй вариант решения записывается в виде выражения, использующего вычисления в алгебре логики с аппроксимацией, для выполнения которых строится расширение семантики элементарных условий и операторов.

В параграфе З.б приводится оптимальное решение задача о минимизации. Для шаблонов и таковым является существующая в их наибольшая нижняя грань. Решение это записывается в виде выражения алгебры частично определенных структур

данных,

В завершающем данную главу параграфе 3.6 рассматривается пример программы сложения двух беззнаковых двоичных чисел на котором иллюстрируется применение метода итеративного поиска инвариантов для языка

В четвертой, заключительной, главе рассматривается задача эффективной верификации линейных программ относительно условий, заданных в Форме примитивных шаблонов, каковыми являются шаблоны с единственным состоянием индексных переменных.

В параграфе 4.1 вводится язык примитивных шаблонов 1-„, Формулы которого имеют ВИД *>=<у. где геойЛХЭ, V —

частично определенная структура данных, расположенная на «»т^сх}. Состояние информационной среды ь=<э, 2-> определяется как удовлетворяющее примитивному шаблону *>=<■*. если и ^ с 2. отношение частичного порядка на множестве задается в соответствии с правилом!.,*"-<2> 5 -г'>%

если и V с .

, Д^Я формулы ВВОДИТСЯ О0ОЗНаЧеНИ6 ВС)03^ЬеВ|

для области истинности р. Информационное множество й называется константным многообразием, если существует примитивный шаблон р такой, что «=вс*о.

В параграфе 4.2 приводится постановка задачи о верификации и определяются связанные с нею понятия.

и-*-программа называется линейной, если ее схема состоит из единственного пути, ведущего из начального состояния в заключительное. Для условия « и линейной -программы р определяется полный инвариант программы р относительно « как предикат в—»-{о. 1 у, задаваемый правилом союсь'э=1 тогда и только тогда, когда существует состояние ЬвВ такое, что ас ьэ =1 и значение р на ь определено и равно ь'.

Указывается, что программа р частично корректна относительно условий « и р тогда и только тогда, когда р является логическим следствием полного инварианта программы р относительно а. Констатируется, что в случае принадлежности условий и полных инвариантов языку задача верификации получает эффективное решение, основанное на сравнении двух примитивных шаблонов.

В связи с этим, для множеств ° элементарных условий и * элементарных операторов рассматривается множество предикатов

[ьэз= <р^а. р — линейная и-г-программа}-, которое называется -замыканием языка ^. язык ^9 называется замкнутым, если каждый предикат из с ьв з представим в виде некоторой Формулы из 1-з.

В параграфе 4.3 дается ответ на вопрос о том, какова должна быть структура базиса для того, чтобы язык оказался -замкнутым.

Индексно-скалярная Формула v называется конъюнктом, если для всех гтоокн формула получаемая из Ф в результате

вычисления индексных выражений и условий на 2. эквивалентна элементарной конъюнкции компонент массивов. Множество всех конъюнктов обозначается соы.

Элементарный оператор у=<«> называется свободным, если для всех геиол правые части различных присваиваний оператора «сгэ. получаемого из а в результате вычисления индексных выражений и условий на но содержат общих существенных переменных при условии, что множество дополнено тождественными присваиваниями таким образом, что все компоненты массивов, встречающиеся в правых частях присваиваний из встречаются также в их левых частях (свойство оператора у быть свободным зависит исключительно от его первой компоненты).

I

Множество всех свободных операторов обознается

Теоремой 4.1 устанавливается, что язык <-а и-у-замкнут тогда и только тогда, когда иесол/, гягк.

В параграфе 4.4 на основании того, что множество в состояний информационной среды изоморфно вкладывается в 1-а, ставится задача расширения семантики базовых условий и операторов с тем, чтобы получить возможность проверки корректности программы р относительно примитивных шаблонов « и р путем выполнения р на « и сопоставления формулы, получаемой в результате такого выполнения, с р.

На основе использования вычислений в алгебре логики с аппроксимацией определяются два варианта такого расширения и связанные с ними две версии выполнения программ. Первый вариант применим к произвольному базису. Относящаяся к нему теорема 4.2 гласит, что линейная -программа р частично корректна относительно примитивных шаблонов «и р. если шаблон р меньше или равен шаблону, получаемому в результате первой версии выполнения р на Второй, более

сильный вариант, применим только к Оазисам, состоящим из конъюнктов и свободных операторов. Теорема 4.3 гласит, что линейная -программа р частично корректна относительно примитивных шаблонов * и р тогда и только тогда, когда шаблон р меньше или равен шаблону, получаемому в результате второй версии выполнения р на

ОСНОВНЫЕ РЕЗУЛЬТАТЫ РАБОТЫ

В диссертационной работе получены следующие результаты.

1. Разработана модель программ, обрабатывающих булевые массивы и сформулированы задачи о соотношениях, о минимизации и о максимизации, к решению которых сводится применение итеративного, метода поиску инвариантов............н | ,

2. Введены и исследованы следующие языки условий: Синдикативных Формул шаблонов ^ и примитивных шаблонов "-„.

3. Исследовано свойство аппоксимируемости информационных множеств импликативными и скалярными формулами. Доказаны теоремы о существовании точных импликативных и наилучших скалярных аппроксимаций информационных множеств.

4. Описаны эвристические подходы к решению задач о соотношениях, о минимизации и о максимизации для языка нацеленные на получение результатов, сочетающих точность аппрокимации с высокой тотальностью.

5. Развита теория вычислений в алгебре логики с аппроксимацией. Доказаны две теоремы о суперпозиции функций данной алгебры.

6. Построены монотонные решения задач о соотношениях и о минимизации для языка

7. Определено свойство замкнутости языка условий относительно базиса из элементарных условий и операторов. Доказана теорема о необходимом и достаточном условии замкнутости языка

8. Построены расширения семантики базовых условий и операторов и на этой основе сформулированы эффективные алгоритмы верификации линейных программ (частичный и полный).

Автор выражает благодарность Ю. Г. Шукуряну за постоянное внимание и поддержку в работе.

СПИСОК ОПУБЛИКОВАННЫХ РАБОТ

1. Костаняп А. Г. Построение инвариантных соотношений специального вида для программ с массивами. — Рукопись депонирована в АРМ. НИИНТИ, per. номер 23 АР-85, 12 с.

2. КостанянА.Г. Инварианты для программ с массивами: концепция построения и возможные применения. — В кн.: "Информатика и вычислительная техника", Ереван, 1986, с. 124.

3. Костанян А. Г. 00 одной задаче верификации линейных программ с булевыми массивами. — Кибернетика и системный анализ, Киев, 1995, Л»5, с. 87-94.

4. S. К. Shoukourian, А. Н. Kostanian, V. A. Margarían, A. A. Ashour. An approuch f or system Tests Design and its applications. // Proceedings of the 13-th IEEE VLSI Test Symposium, NJ, Princeton, 199S.

UirtDDOJUQhP

U-piIbQ ¿puii.li UnumuiQiiuQ "htnJuipfiuiQijiQbph npnQtttJ pntijuiQ qiiiQqiJui<5Qbprn| <5puiqpbp(i Ruuluip"

/Kosta.nl an Arnen H. ,

"Search of invariants for programms with Boolean arrays"/

Ui(ibOui|ur)un|»juiQ tfbg RbynuqrHpiJb i fc,, ( JiQi|uip|->ujQy>Qbpli npnQiJiuQ NO^lTD pmiiUiQ quiQqi|ui6Qbp oqvmiqnpdnn ipuiqphph fiuiiluip li ui(nugi{bi bQ RbipU^un. uiprnr»QpQbpp. t

1. UuinmgL(h L t pruuuiQ quiOq^u«5Qtip J2ulMnrl ¿piuqpbjifi tfnrjb i U ¿Uuil|bpujLib i hQ iunQi.nipiniQDhpti, ittnQ|nIliquigtfuiQ U iIuipu|nIfiquigiJuiG Juiu)iQ fuQrvlipDbpn, npnQg (.minJuiQQ t pbpi(nia fiQiJuipJ-iu£li(iQbp|i npnQCujG tmibpiun>tnl ilbpnriti 4(ipuinnalQ:

2. \il|uipuiqptjb i U Rbifiuiqnipijb I bQ (rJujl hlfuupjitj puiQmALbpp L^, guipinQQbpfi L^ U mpfivJfiifillil jUiPl^ODbpli La mmiluiQQhpfi ibquiObpc:

3. Ahipiuqrupi^bv t fiQVr'Iu'Sh"^ puiqtfrupiruQQbpp uimpnputiduignulQ fitful lfrljuii(>fii) ^ uljiuiiuip ptuQuidlibpfi il|igngni^: Uu(uignigijbi bQ |iC!3,r)P-iIuiglinQ puiqil™pjniOQbp(i B2qp|n|i U lunJuiqnijQ uljuiijuip uiinpnputiiluignal-Qbp(i qniwpiuiQ phnpbvJGbp:

4. L.^ ibqv||i fiimluip Ql(uipuiqpi|bv bQ uiujpnpu|nruigiJuiQ ngvnipiraQD RunJuivniipuidnipiuiQ Rfaiji qmqwljgnri umQi.nipiniQQbp|-i, iJliQIiiItiqu'giJuiQ 11 iIuipu|nIliqwgiJmQ iIuiufiQ JuClrj^pQbpJn ^ra6Uu£i ijiuippbpiul(Qbp:

5. 8uipqujgi|bi t fiui2^Uipl|nnJQbph lfibunipintQc unnpnpu(nJuigiJuiUp ifipui-lluipxuQnipjiuQ fiuiQpuiRui2tiniU: V2i)Ui£> RuiQpuiRui2i|h RuiiJujp uiujuigragijbi. t bpl(ni pbnpbiJ iptariuirjptliuQ tfuiufiQ:

6. L lbqi||i RunJuip l(Uinmgi|b t bQ uinQi.nipjniQQbp|i U U)iQ)iiIlnquig-iTtuQ iTujufnQ (uQri|ipQbpfi iTnQnifinQ it»dmuTQbp:

7. Suippui^uiQ ii(iiijiJiuQQbpfig li oujbpuin>npQbphQ puiqliiuguid Rh^p!'' RuiiJuip uui\JujQi|bi t mumJiuQQbpJi ibqilfi ltmi^mpiuiQ filing rupireQc: Uujiii-gnigi|bi t pbnpbil La ibqtlfi i)iuiljisp jUiQ UiQRpiudb2>(i b puiL|uipuip mujUuiQ(i iIuiu|iQ:

8. Muinragi|bi bQ R|iiJpuii|iQ mmiluiQQtapln U oinbpwi(>npQbp|i ubilUiQ-t(i)n4untn [¡QrmiixQnuJQhp, ripnQg R|nJuiQ ilpw &Uui4bpu|iJb i bQ qSuiifiQ ¿puiqpbph Q2i(inipiiiiQ uifminJiuQ t$>bl(tjifit| Ui[qnp^pi7bp: