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

Московский государственный университет имени М.В. Ломоносова Факультет вычислительной математики и кибернетики

005007454

Захаров Владимир Анатольевич

ПРОБЛЕМА ЭКВИВАЛЕНТНОСТИ ПРОГРАММ: МОДЕЛИ, АЛГОРИТМЫ, СЛОЖНОСТЬ

Специальность 01.01.09 — Дискретная математика и математическая кибернетика

АВТОРЕФЕРАТ

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

1 2 ЯНВ 2012

Москва — 2011

005007454

Работа выполнена на кафедре математической кибернетики факультета вычислительной математики и кибернетики Московского государственного университета имени М.В. Ломоносова

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

академик HAH Украины Лети невский Александр Адольфович

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

Ломазова Ирина Александровна

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

Соколов Валерий Анатольевич

Ведущая организация Учреждение Российской академии наук

Институт систем информатики им. А.П. Ершова

Сибирского отделения РАН (ИСИ СО РАН)

Защита состоится 02 марта 2012 г. в 11.00 на заседании диссертационного совета Д 501.001.44 при Московском государственном университете имени М.В. Ломоносова по адресу 119991, ГСП-1, Москва, Ленинские горы, МГУ, 2-й учебный корпус, факультет ВМК, ауд. 685.

С диссертацией можно ознакомиться в библиотеке факультета ВМК МГУ Автореферат разослан 29 ноября 2011 г.

Ученый секретарь диссертационного совета профессор

Трифонов Н. П.

Общая характеристика диссертационной работы

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

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

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

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

С проблемой эквивалентности программ сталкиваются при решении ряда задач системного программирования и компьютерной безопасности; к их

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

Принципиальная трудность задач семантического анализа программ объясняется тем, что в любой «естественной» универсальной системе программирования любое нетривиальное функциональное свойство программ нерекурсивно (теорема Райса-Успенского). Этот факт не отменяет возможности получения эффективно проверяемых достаточных условий функциональной эквивалентности программ, однако, ни одно из этих достаточных условий не будет необходимым. Систематический подход к поиску эффективно проверяемых достаточных условий эквивалентности программ и построению систем эквивалентных преобразований был предложен и развит в работах A.A. Ляпунова, Ю.И. Янова, А.П. Ершова, В.М. Глушкова, A.A. Летичевского, Р.И. Подловченко, В.К. Сабельфельда, М.С. Патерсона, 3. Манны, Ш. Грейбах, Р. Милнера. Эти работы привели к созданию и развитию теории схем программ, в рамках которой сформировалась общая методика построения и применения моделей программ для решения проблем эквивалентности и эквивалентных преобразований. Основные положения этой методики таковы.

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

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

3). Выделяется подкласс £Т> моделей программ М{сг), в которых задача проверки эквивалентности схем программ 7г' ж" имеет приемлемое решение. Для моделей программ семейства £Т> разрабатываются эффективные алгоритмы проверки эквивалентности схем программ.

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

а) выбрать модель программ М(<то), соответствующую этой системе программирования;

б) выбрать в классе ЕТ> минимальную по отношению аппроксимации модель программ М(01), удовлетворяющую условию М(<?о) Е -^(о"]);

в) воспользоваться алгоритмом проверки эквивалентности схем программ в модели М(а1).

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

Цель диссертационной работы — решение следующих задач.

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

2. Разработать общий метод построения эффективных алгоритмов проверки эквивалентности программ в рассматриваемых формальных системах вычислений.

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

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

Научная новизна и практическая ценность работы. Диссертационная работа представляет собой теоретическое исследование. Все результаты, представленные в ней, являются новыми и получены автором самостоятельно.

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

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

Апробация работы Результаты исследований, изложенные в диссертационной работе, были представлены и обсуждены на следующих научных форумах: Международные конференции «Проблемы теоретической кибернетики» (Горький 1988, Волгоград 1991, Саратов 1993, Ульяновск 1996, Нижний Новгород 1999, Казань 2002, Пенза 2005, Казань 2008, Нижний Новгород 2011), Международные конференции «Дискретные модели в теории управляющих систем» (Красновидово 1997, Красновидово 1998, Краснови-дово 2000, Ратмино 2003, Москва 2004, Москва 2009), Международный семинар «Дискретная математика и ее приложения» (Москва 1988, Москва 2001, Москва 2004, Москва 2007), Международная алгебраическая конференция памяти А.Г.Куроша (Москва 1998), Всероссийская научная конференция «Методы и средства обработки информации» (Москва 2005), Международная школа-семинар «Синтез и сложность управляющих систем» (Санкт-Петербург 2006), Научно-практическая конференция «Информационная безопасность» (Таганрог 2006, Таганрог 2007), Международная конференция «Логика, методология, философия науки» (Обнинск, 1995), International Colloquium on Automata, Languages and Programming (Aalborg 1998), Mathematical Foundations of Computer Science Workshop on Grammar Systems (Brno, 1998), Logic Colloquium 2000 (Paris 2000), Fundamentals of Computation Theory-Workshop on Formal Languages and Automata (Iassy 1999), International Conference «Machines, Computations, and Universality» (Chisinau 2001), International Workshop on Program Understanding (Алтай 2003, Новосибирск 2009), Congress of Mathematics of Serbia and Montenegro (Petrovac, 2004), International Conference on Implementations and Applications of Automata (Kingston 2004, Sophia Antipolis 2005), International Workshop «Automata, algorithms, and information technologies» (Киев, 2010)

Публикации. Материал диссертации опубликован в 60 печатных научных трудах (включая 15 публикаций в изданиях из списка ВАК): 20 статей в журналах и периодических изданиях, 40 статей в сборниках научных трудов и тезисов конференций.

Структура и объем работы. Диссертационная работа содержит 438 страниц машинописного текста; она состоит из 7 глав, включая введение и заключение. Список литературы содержит 550 наименований.

КРАТКОЕ СОДЕРЖАНИЕ ДИССЕРТАЦИИ

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

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

В разделе 2.1 описана пропозициональная модель вычислений последовательных императивных программ; она является центральным объектом изучения всей работы. Эта модель программ представляет собой интеграцию и развитие двух концепций построения формальных моделей последовательных (операторных) программ, восходящих к схемам программ Ляпунова-Янова, — теории дискретных преобразователей Глушкова-Летичевского и теории алгебраических моделей программ Подловченко.

Последовательные пропозициональные программы определяются над конечными множествами базовых операторов А и базовых предикатов V. Базовые операторы обозначают элементарные вычислительные действия, осуществляющие преобразования данных. Конечные последовательности базовых операторов называются А-цепочками. Базовые предикаты обозначают элементарные отношения на множестве данных. Всякий набор истинностных значений всех базовых предикатов называется логическим условием. Множество всех логических условий предикатов из V обзначается записью Ср.

Определение 2.1.1. Пропозициональная последовательная программа — это конечная размеченная система переходов 7г — (V,start,stop,Т, В), компонентами которой являются

• V — конечное множество точек программы, V Ф 0,

• start — точка входа в программу, start € V,

• stop — точка выхода из программы, stop £ V,

• Т : (V \ {stop}) х Ср —>■ V — тотальная функция переходов из одних точек программ в другие;

• В : V \ {stop} -> А* — функция привязки, ставящая в соответствие каждой точке программы, за исключением точки выхода, Л-цепочку.

Точки программы соответствуют ее линейным участкам; в каждой точке v выполняется последовательность операторов B(v). Совокупность переходов из каждой точки v программы соответствует оператору ветвления, передающего управление в точки T(v, Д) в зависимости от набора А, Д € Ср, истинностных значений базовых предикатов.

Трассой, исходящей из точки v в программе тт, называется всякая последовательность пар

tr = (иь Дх), (и2, Дг), ■ • •, К Д.)»(Vi+li Д«+1). в которой Vi = v и для любого i,i > 1, выполняются следующие отношения: Vi е V, Ai € Ср и vi+i = T(vi,Ai). Трасса, исходящая из точки входа start, называется начальной. Начальная трасса называется полной, если она бесконечна или завершается такой парой (vn, Дп), что T(vn,An) = stop.

Семантика пропозициональных последовательных программ описывается посредством шкал и моделей пропозициональной динамической логики. Интерпретации базовых операторов задают динамические шкалы.

Определение 2.1.3. Динамическая шкала задается тройкой Т~ (5, йо, Я), состоящей из

— непустого счетного множества состояний данных 5',

— начального состояния данных во, во € 5,

— всюду определенной функции преобразования данных Я: Л х 5 —> 5.

Функция преобразования данных Я распространяется на множество .Д-цепо-чек посредством равенств Я*(г, э) = я и Я*(аИ, й) = Я*(к, Я(а, в)) для любых «4-цепочек к, операторов о и состояний данных я. Состояние данных з" называется вычислимым из состояния данных в' на шкале Т (для обозначения этого отношения используется запись в' в"), если в" — В.*(к, я') для некоторой .4-цепочки /1. Для каждой операторной цепочки И запись [/г]/- обозначает состояние данных в = Я* (/г, йо), вычислимое на шкале Т из начального состояния данных йо при выполнением операторов Д-цепочки /г.

В диссертационной работе особое внимание уделено двум классам шкал — упорядоченным и полугрупповым. Динамическая шкала Т называется упорядоченной, если отношение вычислимости является отношением частичного порядка. Шкала Т называется полугрупповой, если множество ее состояний данных образует моноид (Б, о, Л), порожденный множеством базовых операторов Л] при этом нейтральный элемент моноида Л играет роль начального состояния данных, а функция преобразования данных Я определяется равенством Я(а, й) = в о а для любых базовых операторов а и состояний данных е.

Полную интерпретацию всех элементов пропозициональных программ задают динамические модели.

Определение 2.1.4. Динамической моделью М, базирующейся на шкале Т, называется пара (Т, £), в которой { : Б XV —> {0,1} — оценка базовых предикатов на шкале Т.

Для каждого состояния данных s и базового предиката р оценка £,(s,p) определяет значение истинности предиката р в состоянии данных s. Оценку базовых предикатов £ на шкале JF можно распространить на множество логических условий С-р: будем использовать запись £(s) для обозначения логического условия Д = {t(s,Pl),Z(s,P2), ■ ■ .

Определение 2.1.5. Всякое множество динамических моделей а называется динамической семантикой программ. Динамическая семантика, все модели которой базируются на одной и той же шкале, называется однородной динамической семантикой.

Для обозначения однородных динамических семантик, базирующихся на шкале Т, используется запись вида o(J-, L), где L — множество допустимых оценок базовых предикатов. Множество всех моделей, базирующихся на шкале Т, обозначется записью

Определение 2.1.6. Вычислением программы тг = (V, start, stop, В, Т) в модели М = (S, so, Я, Q называется максимальная последовательность пар

сотр(ж, М) = (и0, s0), (üi, Si),..., (ví, s¿), (t'i+i, si+1),...

удовлетворяющая следующим условиям:

— vo = start, so — начальное состояние данных;

— для любого i, г > 1, выполняются равенства s¡ — R*(B(ví-i), s¿_i) и w¿ = T(vi-i,£(si)).

Если вычисление comp(iг, М) завершается парой (stop, sjv), то оно считается успешным, а состояние данных sa¡ называется результатом вычисления и обозначается записью [comp(it, М)]. Если сотр(ж,М) — бесконечная последовательность, то это вычисление называется бесконечным, и его результат [сотр(7Г, М)] считается неопределенным.

Определение 2.1.7. Две программы тс\ и 7Г2 называются

— эквивалентными в динамической модели М (обозначается it\ к2), если \comp(iri, М)} = [compfa, М)]\

— эквивалентными в динамической семантике а (обозначается 7Гх тгг), если отношение -п\ 7Г2 выполняется для любой модели М из <т;

— эквивалентными на динамической шкале Т (обозначается яг), если выполняется отношение ~<т(Л

Определение 2.1.8. Динамическая семантика а2 аппроксимирует динамическую семантику (71 (обозначается о\ С 02), если для любой пары 7Г1 и 7г2 выполняется соотношение 7Г1 7Г2 =Ф- я^ тг2 . Динамические семантики с] и о"2 называются равносильными (обозначается и\ — сг2), если выполняются оба соотношения <тх С сгг и <72 С <у\,

В диссертационной работе для модели вычислений последовательных пропозициональных программ исследуются две основные задачи. Задача проверки аппроксимируемости динамических семантик. Для двух заданных семантик (множеств динамических моделей) о\ и <г% выяснить, аппроксимирует ли семантика а2 семантику <71: а\ С <72 ? Задача проверки эквивалентности программ. Для заданной динамической семантики а и пары последовательных пропозициональных программ я-! и 7Г2 выяснить, эквивалентны ли эти программы в семантике а\ 7Г1 щ ?

Для решения первой из этих задач на множестве динамических семантик введено отношение гомоморфного сужения. Для динамической семантики а запись когп(а) обозначает множество всех динамических моделей, каждая из которых является гомоморфным образом какой-либо динамической модели из множества ст. Динамическая семантика 0\ является гомоморфным сужением динамической семантики стг, если выполняется включение <71 С /10771(02). Достаточное условие аппроксимируемости динамических семантик описывает

Теорема 2.1.9. Для любой пары семантик 01,02 верно соотношение 0\ С /гото(а2) о\ С .

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

Для решения задачи проверки эквивалентности программ с каждым вычислением сотр(п, М) программы тг ассоциируется трасса £г(7г, М) в программе я — путь в системе переходов, исходящий из точки входа, — реализуемая в динамической модели М. На множествах начальных трасс в программах введено отношение совместности трасс: трассы tri и tr2 в программах щ и 7Г2 совместны в динамической семантике а, если для некоторой динамической модели М, М 6 сг, последовательности in и tr-} являются префиксами трасс tr(ir\, М) и £г(тг2, М). В терминах отношения совместности трасс сформулированы необходимые и достаточные условия эквивалентности программ (теорема 2.1.5); на их основе в главе 5 разработаны новые методы и алгоритмы проверки эквивалентности программ.

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

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

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

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

Так же, как и для последовательных программ, интерпретации базовых операторов и предикатов в рекурсивных программах задаются при помощи моделей пропозициональной динамической логики (структур Крипке). Подобно тому, как это было сделано в разделе 2.1 для последовательных программ, в разделе 2.2 определены понятия вычисления рекурсивной программы и результата вычисления, введены отношение эквивалентности рекурсивных программ в заданной динамической модели М и на множестве динамических моделей (в динамической семантике) а, сформулирована задача проверки эквивалентности. Также представлен ряд утверждений о свойствах трасс в пропозициональных рекурсивных программах, позволяющих установить необходимые и достаточные условия эквивалентности рекурсивных программ в зависимости от устройства пар совместных трасс в сравниваемых программах. Как показано в разделе 6.3, новые методы проверки эквивалентности последовательных программ можно адаптировать для решения проблемы эквивалентности в некоторых классах рекурсивных программ.

В разделе 2.3 исследована взаимосвязь между системой вычислений последовательных программ, введенной в разделе 2.1, и стандартными схемами программ — математической моделью императивных программ, определенной в рамках формализма логики предикатов первого порядка. Устройство интерпретаций языка пропозициональной динамической логики программ позволяет использовать хорошо изученные полугруппы конечных подстановок для вложения стандартных схем программ в пропозициональную модель вычислений последовательных программ. Как показано в разделе 6.4, предложенный способ вложения открывает новые возможности использования алгебраических особенностей полугрупп конечных подстановок для построения эффективных (в т. ч. полиномиапьных по времени) алгоритмов проверки эквивалентности для некоторых классов стандартных схем программ.

Введенная в разделе 2.1 модель вычислений последовательных программ может применяться для решения задач анализа программ в разных парадигмах программирования. В заключительном разделе 2.4. второй главы диссертационной работы на основе этой модели вычислений введена пропозициональная модель потоковых программ, проводящих вычисления в режиме оперативного взаимодействия с внешней средой. Главная особенность потоковых программ состоит в том, что в их вычислениях нет обратной связи между состояниями управления (точками) программы и состояниями данных. Потоковые программы моделируют вычисления алгоритмов, работающих в оперативном режиме (режиме on-line). Трасса вычисления потоковой программы определяется последовательностью событий (запросов), которая не зависит от состояний данных, преобразуемых операторами программы в ответ на поступающие события. Предложенная модель потоковых программ имеет тесную связь с моделью вычислений обобщенных детерминированных конечных автоматов-преобразователей (transducers). Как показано в разделе 6.5, предложенные в главе 4 методы проверки эквивалентности последовательных программ применимы также и для решения проблемы эквивалентности потоковых программ.

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

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

1. К какому типу отношений порядка принадлежит отношение аппроксимации в различных классах динамических семантик пропозициональных программ?

2. В каких классах динамических семантик выполнимость требования а\ С Нот(а2) является не только достаточным, но необходимым условием аппроксимируемости семантик?

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

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

Чтобы иметь возможность сравнивать динамические семантики программ и установить структуру отношения аппроксимации Е, выделена особая разновидность динамических семантик — насыщенные семантики. Динамическая семантика сг называется насыщенной, если для любой динамической модели М верно соотношение М о а ф аИ {М}. Каждый класс равносильности динамических семантик содержит единственную насыщенную семантику и сг'. Для насыщенных динамических семантик справедлива

Теорема 4.1.9. Класс насыщенных семантик программ с отношение аппроксимации С образует полную дистрибутивную решетку, в которой отношение аппроксимации совпадает с отношением гомоморфного сужения.

Следствие 4.1.10. Совокупность динамических семантик программ с отношением аппроксимации С образует квазирешетку.

В разделе 4.2 изучен вопрос о совпадении отношений аппроксимации и гомоморфного сужения для однородных динамических семантик, все модели в которых базируются на одной и той же шкале. Интерес к этому классу динамических семантик обусловлен тем, что 1) однородные динамические семантики описываются наиболее просто — интерпретация базовых операторов и допустимые оценки базовых предикатов специфицируются независимо друг от друга, и 2) именно однородные динамические семантики пропозициональных программ соответствуют свободным (эрбрановским) интерпретациям в теории стандартных (первопорядковых) схем программ и интерпрета-

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

Теорема 4.2.11. Существуют такие однородно насыщенные семантики ci, <У\ Ç а{Т\) и (72, 02 Ç <7(^2), что С а^, но неверно, что а\ С homfa)-

Эта теорема свидетельствует о том, что класс однородных динамических семантик при всей простоте и естественности его устройства «алгебраически несовершенен». Вместе с тем, если шкала F обладает свойством конечной представимости (для любого состояния данных s множество Д-цепочек {h : [/г]= s} конечно) или свойством обратимости (для любой Д-цепочки h существует такая цепочка /г-1, для которой верно равенство [hh~l]jr = \е)?), то для любой пары однородно насыщенных семантик а, а С а{Т) и а', а' С верно соотношение о' Qa -Ф=Ф а' С hom(a) (теоремы 4.2.20 и 4.2.21).

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

Теорема 4.3.9. Существуют такие динамическая семантики, для которых стандартная однородная аппроксимация не является наиболее точной однородной аппроксимацией.

Теорема 4.3.10. Существуют динамические семантики, не имеющие наиболее точной однородной аппроксимации

На основании этих теорем показано (утверждения 4.3.11 и 4.3.12), что некоторые пары однородных семантик не имеют точных нижних и точных верхней граней по отношению аппроксимации С. Тем самым было установлено, что квазиупорядоченное по отношению аппроксимации семейство однородных динамических семантик не является квазирешеткой, и в нем отношение аппроксимации отличается от отношения гомоморфного сужения.

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

1) установить условия совместности начальных трасс в программах, вычисления которых определяются в семантиках заданного класса;

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

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

4) выделить классы распознающих машин (и соответствующие им классы динамических семантик), для которых проблема пустоты имеет небольшую вычислительную сложность.

В основу этого метода положена следующая идея. Для проверки экива-лентности программ щ необходимо проверить, что каждая пара сов-

местных в семантике а трасс в программах яг,П2 имеет одинаковый результат. Но внимания заслуживают не вычисляемые этими программами состояния данных «1 и ¿2, а степень их отличия с^ьвг)- Можно выбрать подходящую математическую структуру (алгебру, полугруппу, автомат) £>, элементы которой выступают в роли оценок степени отличия между состояниями данных динамической шкалы Т = (5, во, Л), потребовав при этом, чтобы в выбранной структуре Б были определены

- интерпретация базовых операторов, обеспечивающая гомоморфное отображение Т х Т в £>,

— подструктура Д), которая гарантирует выполнимость для любых состояний данных «г, 82 соотношения 51 = вг ¿>(^1, вг) € Д).

Тогда возникает возможность построить машину (автомат, размеченную систему переходов и др.) К{ъ\, тгг, £>), которая воспроизводит ^-совместные вычисления программ я-! и 7Гг, оперируя лишь с элементами структуры £). Выделенная подструктура Д) обеспечивает проверку условий совместности программных трасс, а также наделяег систему К{-к\,-кч, Щ следующим важным свойством: программы и щ неэквивалентны на шкале Т в том и только том случае, когда хотя бы один из прогонов машины А"(тгь яг, £>) завершается вычислением элемента, не принадлежащего Д). Таким образом, задача проверки эквивалентности программ щ и 7г2 оказывается равносильной проблеме невычислимости (недостижимости) машиной К(щ,П2,0) ни одного элемента из О \ Д>. Поскольку предлагаемый подход предусматривает построение вспомогательной машины, воспроизводящей пары совместных вычислений анализируемых программ, этот метод решения проблемы эквивалентности программ получил название метод совместных вычислений.

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

ных динамических шкалах. Характерная особенность этих шкал состоит в том, что все базовые операторы выполняют на этих шкалах необратимые преобразования. Для упорядоченных шкал в качестве подходящих структур Д устанавливающих степень отличия состояний данных шкалы, могут быть выбраны детерминированные двухленточные автоматы и системы полугрупп специального вида — критериальные системы. Главное преимущество такого выбора состоит в том, что соответствующие системы А'(л"т, тг^, О) обладают полезным для разработки алгоритмов свойством: для произвольной пары ^"-эквивалентных программ щ и яг множество состояний, достижимых системой К(7Т1, я"2> -О)) конечно. Во многих случаях размер этого множества состояний ограничен полиномом, зависящим от размеров программ 1Г\ и 7Г2, и это создает хорошие предпосылки для построения алгоритмов, разрешающих проблему эквивалентности программ за полиномиальное время.

В разделе 5.1 введены детерминированные двухленточные односторонние машины (2-ОМ), распознающие в оперативном режиме (без использования маркеров конца слова) бинарные отношения на множестве Д-цепочек.

Определение 5.1.1. Двухлепточпой детерминированной машиной (2-БМ) называется система Б = (Е, (^х,С,)2,<7о> -Р1,уз), состоящая из

• входного алфавита Е,

• двух непересекающихся множеств внутренних состояний <31 и С,)?,

• начального состояния

• множества допускающих состояний Г, Г С (¿¡и и

• частично определенной функции переходов : (С^ и<2г) (<21 и<3г)-

Машина прочитывает пару слов ««1 и щ, записанных на лентах 1 и 2. Когда машина £) пребывает во внутреннем состоянии q, д £ г = 1,2, она прочитывает очередную букву х (если таковая есть) слова помещенного на ленте г, и переходит в состояние с/ = <р(д,х). Пара слов (и>х, гУг) допускается машиной Б, если она считывает оба слова и ю2, записанные на ее лентах, и оказывается по прочтении этой пары слов в допускающем состоянии.

Более формально поведение машины D определяется следующим образом. Прогоном 2-DM D называется последовательность пар

а = («о, (91, xi),..., (qn, хп),...

удовлетворяющая соотношениям qo — начальное состояние, % £ Qi U Q2, Xi е Е и qi+1 = <p(qi,Xi) для всех г, г > 0. Если эта последовательность оканчивается парой (q„,xп), то говорят, что прогон а достигает состояния 4 — <P(fh, хп). Для каждого <5 £ {1,2} можно выделить подпоследовательность

Cts = {linXii), • • ■ 1 (QikJ^ik)' ■ ■ • >

прогона о, состоящую из всех тех пар (qi^Xi.) последовательности а, которые удовлетворяют условию qtj € Qs. Тогда ¿-проекцией прогона а называется слово а[5] = xitxi2.. .xik — Пара слов w\,wo в алфавите £ допускается машиной Д если существует прогон а, достигающий допускающего состояния q, q £ F, и проекциями этого прогона являются слова гщ, ги2- Запись Ец обозначает множество всех пар слов, допускаемых 2-DM D.

Считается, что 2-DM D описывает динамическую шкалу F, если Ев =

{(ЛьЛг) : =

Теорема 5.1.4. Динамическая шкала Т может бить описана некоторой 2-DM тогда и только тогда, когда Т — упорядоченная шкала.

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

В разделе 5.2 описана концепция комбинированной машины К{iri,7r2, D) (определение 5.2.1), реализующая представленную выше идею метода совместных вычислений. Комбинированная машина #(714, яъ, D) — это 2-DM, состоящая из трех взаимодействующих частей — программ 7Гь 7Г2 и 2-DM D, описывающей ту шкалу Т, которая задает интерпретацию базовых операторов этих программ. На вход этой двухленточной машины подается пара последовательностей вида (?;ь Д1), (г>2, Д2),..., записанных на ее лентах. Со-

стояния управления (мета-состояния) комбинированной машины К(к1, яг, Б)

— это четверки вида {У1,Ь2,д, 2), где и2 — точки в программах и Я2, д

— это внутреннее состояние 2-БМ В, a,Z — это элемент множества Ср и {±}, используемый для проверки согласованности трасс, поступающих на вход комбинированной машины. Компоненты тл, тгг проверяют, являются ли последовательности, записанные на входных лентах, начальными трассами в программах 7Гх и Я2. Компоненте В отводится роль синхронизатора, позволяющего прочитывать до конца только такие пары начальных трасс, которые совместны на шкале Т. Основным результатом раздела 5.2 является

Теорема 5.2.4. Если 2-ЭМ В описывастп шкалу Т, то я"! тг2 тогда и только тогда, когда комбинированная машина К(тт\,П2,В) А: распознает пустое бинарное отношение и

В: в каждом бесконечном прогоне бесконечно часто считывает данные на обеих лентах.

В разделе 5.3 выявлены некоторые характерные особенности устройства комбинированных машин К(7Гх,7г2, Б) для эквивалентных программ тт\ и 7г2, проводящих вычисления на упорядоченной динамической шкале Т, описываемой 2-ОМ В. Основное внимание уделяется специальным мета-состояниям комбинированных машин — когерентным мета-состояниям. Мета-состояние (г>1, д, 2) комбинированной машины К{Я), щ, В) называется когерентным, если д — это допускающее состояние управления 2-ОМ О. Особенности поведения комбинированных машин описывают две теоремы.

Теорема 5.3.5. Если яг, то любой бесконечный прогон комбинированной машины К(л1, щ, И) проходит через когерентные мета-состояния бесконечно часто.

Теорема 5.3.8. Если щ яг, и 2-БМ Б имеет N допускающих состояний, то комбинированная машина К(-П1,ТТ2,В) на каждом участке длины N(1^11 + |я>>|) любого прогона проходит, хотя бы через одно когерентное мета-состояние.

Следствием этих теорем является основной результат раздела 5.3:

Теорема 5.3.9. Если упорядоченная шкала Т описывается 2-DM D, имеющей конечное множество F допускающих состояний, и программы щ и 7Го эквивалентны на шкале Т, то число мета-состояний комбинированной машины А'(7Г1,7Г2, D), достижимых из начального мета-состояния, ограничено величиной

В разделе 5.4 приведены оценки сложности задачи проверки эквивалентности пропозициональных последовательных программ, семантика базовых операторов которых определяется упорядоченными динамическими шкалами, и описаны алгоритмы решения этой задачи. В основу алгоритмов, разрешающих отношение эквивалентности программ на упорядоченных шкалах, положены теорема 5.2.4, позволяющая свести проблему эквивалентности программ к задаче проверки пустоты комбинированной машины, и теорема 5.3.9, оценивающая размер комбинированной машины в зависимости от размера анализируемых программ и количества допускающих состояний 2DM D, описывающей упорядоченную шкалу. Чтобы придать оценкам сложности наибольшую общность, алгоритмы проверки эквивалентности реализуются релятивизованными машинами Тьюринга, снабженными двумя оракулами Ed и Un- Оракул Ер — это бинарное отношение на множестве Л-цепочек, распознаваемое 2-DM D, а Up — это множество всех таких четверок Л-цепочек (h\, h'2, Ы[, Щ), что по прочтении обеих пар {h\,h'^} и (h'(, /i'2') 2-DM D переходит в одно и то же состояние управления.

Теорема 5.4.1. Если упорядоченная шкала J- описывается 2-DM D с конечным множеством допускающих состояний, то задача проверки неэквивалентности программ 7Tj. фу -■> принадлежит релятивизованному классу сложности NPEd.

В частности, эта теорема верна для всякой полугрупповой упорядоченной шкалы, обладающей свойством левого сокращения, т. к. она может быть описана 2-DM с единственным допускающим состоянием.

Теорема 5.4.5. Если шкала Т может быть описана 2-ОМ с конечным множеством состояний (двухленточным детерминированным конечным автоматом), то задача проверки эквивалентности программ я"! щ принадлежит классу сложности МЬОСБРАСЕ.

Полинимиальные по времени алгоритмы проверки эквивалентности программ можно получить в тех случаях, когда на динамические шкалы и/или описывающие их 2-БМ налагаются другие ограничения.

Пусть ]¥(п) — некоторая неубывающая функция натурального аргумента. Считается, что 2-БМ О имеет У/-ограниченную ширину, если для любой пары Д-цепочек и И?, длина которых не превосходит п, множество состояний управления машины Д из которых она может достичь допускающего состояния при прочтении .А-цепочек /¡,) и к2, содержит не более \У(п) элементов.

Теорема 5.4.7. Если шкала Т описывается 2-БМ И полиномиально ограниченной ширины, то задача проверки эквивалентности программ тгг принадлежит релятивизованному классу сложности РТ1МЕе° .

Шкала Т — (5, «о, Я) называется инъективной, если интерпретация операторов Н(а, ■) является инъективным отображением для любого базового оператора а, а 6 Л. В частности, упорядоченная полугрупповая шкала является инъективной тогда и только тогда, когда она обладает свойством правого сокращения.

Теорема 5.4.10. Если инъективная шкала Т описывается редуцированной 2-ИМ П, имеющей конечное множество допускающих состояний, то задача проверки эквивалентности программ щ яг принадлежит релятивизованному классу сложности РТ1МЕЕ°'и°.

В разделе 5.5 описан алгебраический вариант метода совместных вычислений. Здесь для оценки отличия состояний данных с>(.31, б'г) полугрупповой шкалы Т используются моноиды (полугруппы), образующие критериальную систему К. Четверка К — (\У, и, ги+,«/). состоящая из моноида в котором выделены подполугруппа II и пара элементов ги+,ги*, является критериаль-

ной системой для полугрупповой упорядоченной шкалы Т, если существует такой гомоморфизм <р : Т X Т II, что для всякой пары состояний данных ^1,32 выполняется соотношение б'1 = в2 ги+ * </з((.$1, «2)) *ии* = е. На

основе этой системы для пары проверяемых программ 7Г1 и щ строится размеченный корневой ориентированный граф совместных вычислений Г(7Ть7Г2). Всякий маршрут, исходящий из корня этого графа, соответствует паре совместных вычислений программ щ и 7г2 в некоторой ^-модели М. В графах совместных вычислений выделено особое множество опровергающих вершин.

Теорема 5.5.5. Программы щ и щ эквивалентны на полугрупповой упорядоченной шкале Т тогда и только тогда, когда из корня графа совместных вычислений Г(я"1,7Г2) не достижима ни одна опровергающая вершина.

Из этой теоремы следует, что в том случае, когда шкала Т имеет конечную полугрупповую систему, графы совместных вычислений Г(тг1,7Гг) конечны, и задача проверки эквивалентности программ т^х тгг принадлежит классу сложности 1^ШСЭРАСЕ. Но разрешающие алгоритмы полиномиальной сложности можно получить и для некоторых бесконечных критериальных систем. Критериальная система К = (V/, II, т+, V)*) для полугрупповой шкалы Т называется обратимой, если для каждого элемента х из класса смежности и * 11)' существует не более одного элемента у из класса смежности ги+ * и, для которого выполняется равенство у * х = е. Тогда в том случае, когда полугрупповая упорядоченная шкала имеет обратимую критериальную систему К, в которой проблема тождеств разрешима за полиномиальное время, задача проверки эквивалентности программ 7П тгг принадлежит классу сложности РТ1МЕ (следствие 5.5.10).

Метод критериальных систем используется в главе 6 для построения алгоритмов проверки эквивалентности программ в других моделях вычислений — рекурсивных программ и стандартных (первопорядковых) программ.

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

1. всякая полу групповая шкала, вложимая в группу, может быть описана 2-БМ 1-ограниченной ширины (утверждения 5.6.1 и 5.6.2);

2. всякая полугрупповая шкала, которая вложима в полугруппу, обладающую свойствами левого сокращения и наиболее общего левого унификатора, имеет обратимую критериальную систему (теорема 5.6.5).

Проверка эквивалентности программ существенно упрощается, если динамические шкалы, определяющие интерпретацию базовых операторов, обладают помимо свойства упорядоченности некоторыми дополнительными свойствами. В разделе 5.7 рассмотрена задача проверки эквивалентности программ на уравновешенных динамических шкалах, характерная особенность которых состоит в том, что любые операторные цепочки, вычисляющие одно и то же состояние данных, обязаны иметь одинаковую длину. Показано, что уравновешенные шкалы могут быть описаны одноленточными машинами. Благодаря этой особенности, теоретико-автоматный и алгебраический варианты метода совместных вычислений могут быть существенно упрощены, а верхние оценки сложности задачи проверки эквивалентности программ на уравновешенных шкалах оказываются существенно меньше (в п2 раз) аналогичных оценок сложности для проверки эквивалентности программ на упорядоченных (но не обязательно уравновешенных) шкалах, описываемых двух-ленточными машинами (теоремы 5.7.8 и 5.7.9).

Примеры некоторых одноленточных и двухленточных детерминированных машин, описывающих упорядоченные шкалы, представлены в разделе 5.8. В этих примерах рассмотрено устройство машин, описывающих упорядоченные шкалы, соответствующие

1) свободной полугруппе базовых операторов (пример 5.8.1);

2) свободной коммутативной полугруппе (пример 5.8.2);

3) полугруппе условно равносильных операторов (пример 5.8.3) с множеством определяющих соотношений вида аЬ — ас;

4) полугруппе подавляемых операторов (пример 5.8.4) с множеством определяющих соотношение вида аЪ = Ъ.

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

В разделе 5.9 приведены примеры критериальных систем для некоторых классов полугрупповых шкал. В этих примерах описаны критериальные системы для уравновешенных полугрушювых шкал, соответствующих

1) свободной полугруппе базовых операторов (пример 5.9.1);

2) свободной коммутативной полугруппе базовых операторов (пример 5.9.2);

3) свободной частично коммутативной полугруппе базовых операторов (пример 5.9.3).

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

В разделе 6.1 исследована задача проверки эквивалентности пропозициональных последовательных программ в однородных семантиках сг(Т, Ь) с определенными ограничениями на множества Ь допустимых функций оценки базовых предикатов. Вначале рассмотрены однородные динамические семантики сг(3-, Ь), базирующиеся на упорядоченных шкалах, в которых множества Ь допустимых функций оценки специфицируются конечными детерминированными автоматами-преобразователями, определенным образом согласованными со шкалами ¡Р. Однородные динамические семантики такого вида получили название автоматных семантик. Показано, что для проверки эквивалентности программ щ в автоматной семантике а(Т, Ь), базирующейся на упорядоченной шкале Т, можно ввести комбинированные двухленточные детерминированные машины, аналогичные тем, которые были введены в разделе 5.2. Для введенных таким образом комбинированных машин оказывается справедливым утверждение, аналогичное теореме 5.2.4, а

также все те вытекающие из нее утверждения, представленные в разделе 5.3,; на основании которых в разделе 5.4 были разработаны эффективные алгоритмы проверки эквивалентности последовательных пропозициональных программ. Таким образом, удалось выделить классы однородных семантик Ь), базирующихся на упорядоченных шкалах, для которых задача проверки эквивалентности программ тгх Щ может быть решена за счет сравнительно простой модификации метода совместных вычислений. Однако для некоторых других однородных семантик применение предложенного подхода требует внесения в него более существенных изменений. В качестве примера в разделе 6.1 исследована проблема эквивалентности программ в однородной динамической семантике с перестановочными операторами и монотонными функциями оценки предикатов. Для решения этой задачи предложен модифицированный вариант метода совместных вычислений, при помощи которого построен полиномиальный по времени разрешающий алгоритм.

Теорема 6.1.11. Задача проверки эквивалентности программ щ и жг в однородной динамической семантике с перестановочными операторами и монотонными функциями оценки предикатами разрешима за время, оцениваемое величиной п9№\\'Р\)) где п = тах(|7Г]|, |тг2|).

В разделе 6.2 алгебраический вариант метода совместных вычислений распространен на рекурсивные программы. Показано, что для линейных рекурсивных программ проблема эквивалентности тх\ пг может быть сведена к проблеме достижимости опровергающих вершин в графе совместных вычислений Г(7Г1,7Г2), построенном на основе критериальной системы К = (Ш,и,'Ш+,и!*) для упорядоченной полугрупповой шкалы Т (теорема 6.2.7), подобно тому, как это было осуществлено в разделе 5.6 для последовательных программ. Если критериальная система К обладает дополнительным свойством сильной обратимости, которое проявляется в однозначной разрешимости уравнений вида х\ * у = е и у * х% — е для любых элементов из классов смежности ги+ * С/ и [/ * ш* соответственно, то справедлива

Теорема 6.2.11. Если полугрупповая уравновешенная шкала Т имеет критериальную систему К = (И7, Г/, и)'}, обладающую свойством сильной обратимости, и в моноиде IV проблема тождества разрешима за полиномиальное время, то проблема эквивалентности линейных рекурсивных программ на шкале Т принадлежит классу сложности со — NP.

Приведены примеры 6.2.1 и 6.2.2, иллюстрирующие применение метода совместных вычислений для проверки эквивалентности рекурсивных программ на некоторых шкалах. Для того чтобы уменьшить сложность разрешающего алгоритма, на критериальную систему К приходится налагать дополнительные ограничения: требуется, чтобы критериальная система К = 1л+, ю*) для упорядоченной полугрупповой шкалы базировалась на разрешимой группе ИЛ В этом случае справедлива

Теорема 6.2.16. Если полугрупповая уравновегиенная шкала Т имеет критериальную систему К = (И;, V, и)*), где XV — конечно порожденная группа, в которой проблема равенства слов разрешима за время, полиномиальное относительно длин слов, то задача проверки эквивалентности линейных рекурсивных программ на шкале Т разрешима за время, полиномиальное относительно размеров программ.

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

задача проверки эквивалентности программ с операторами выбора режима вычисления является PSPACE-полной алгоритмической проблемой (теоремы 6.3.8 и 6.3.9). На основе этого результата показано, что и для многих других неупорядоченных шкал задача проверки эквивалентности программ является PSPACE-трудной задачей (теорема 6.3.10).

В разделе разделе 6.4 исследована проблема эквивалентности стандартных схем программ. Как показано в разделе 1.3, эта проблема может быть сведена к задаче проверки эквивалентности пропозициональных последовательных программ, семантика которых определяется на основе полугруппы конечных подстановок. Поэтому метод совместных вычислений применим для построения алгоритмов проверки эквивалентности в модели вычислений стандартных схем программ. На основе этого метода выделен новый класс стандартных схем программ с разрешимой проблемой эквивалентности — класс ортогональных схем программ.

Два терма считаются ортогональными, если ни один из них не является подтермом другого. Подствновка в : Var —> Term называется ортогональной, если 1) она не является переименованием, 2) все термы в (а;) не являются основными термами, и 3) для любой пары различных переменных х, у термы в(х),в(у) ортогональны. В ортогональных схемах программ любая подстановка в ~ {xi/ti,... ,xn/tn}, которая соответствует последовательной композиции операторов присваивания линейного участка программы, является ортогональной. Показано, что множество ортогональных подстановок с операцией композицией, пополненное тождественной подстановкой е, образует моноид (теорема 6.4.3), упорядоченный (следствие 6.4.5) а также обладающий свойствами левого сокращения (следствие 6.4.7) и наиболее общего левого унификатора (утверждение 6.4.11). Таким образом, на основании теорем 5.4.7 и 5.6.5 справедлива

Теорема 6.4.12 Задача проверки эквивалентности ортогональных стандартных схем программ разрешима за полиномиальное время.

В последнем разделе 6.5 шестой главы показано, как можно адаптировать метод совместных вычислений для проверки эквивалентности потоковых программ. Главная особенность потоковых программ, отличающая их от рассмотренных ранее вычислительных моделей последовательных и рекурсивных программ, состоит в том, что в вычислениях потоковых программ нет обратной связи между последовательностями состояний управления (точками) программы и состояний данных. Трасса вычисления такой программы определяется последовательностью событий (запросов), которая не зависит от состояний данных, преобразуемых операторами программы в ответ на поступающие события. Поэтому для описания динамических шкал можно использовать одноленточные детерминированные машины (1-DM). В то же время, для потоковых программ неверна теорема 2.1.5 о приведении произвольной программы к нормальной форме, и на каждом шаге вычисления потоковая программа может выполнять не одно базовое действие, а некоторую конечную последовательность операций. Поэтому комбинированные машины для потоковых программ вынуждены обрабатывать на каждом отдельном шаге своего прогона не отдельные буквы (базовые операторы), а конечные слова (Д-цепочки). Для потоковых комбинированных машин доказана теорема 6.5.2 о сводимости проблемы эквивалентности потоковых программ 7Ti, тг2 на произвольной шкале Т, описываемой 1-DM D, к проблеме пустоты соответствующей потоковой комбинированной машины D). Также

установлены достаточные условия (теорема 6.5.4) разрешимости проблемы пустоты потоковых комбинированных машин за полиномиальное время. На основании этих условий доказана теорема

Теорема 6.5.6 Если полугрупповая шкала JF вложима в конечно порожденную группу, в которой проблема тождества wi = w-i разрешима за время t(n), то задача проверки эквивалентности потоковых программ 7Ti 7Г2 разрешима за время 0(n2t(n2)), где п = max(|7Ti|, 17Г21)-

В заключительной главе 7 перечислены основные результаты, полученные в диссертационной работе.

Основные результаты

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

2. Установлен тип отношения аппроксимации в различных классах динамических семантик пропозициональных программ.

3. Установлены достаточные условия существования для заданной динамической семантики ее наиболее точной аппроксимации в классе однородных динамических семантик.

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

5. На основе метода совместных вычислений установлены достаточные условия, которым должна удовлетворять динамическая семантика, задающая интерпретацию операторов программ, для того чтобы задача проверки эквивалентности последовательных программ принадлежала классу сложности со-ИР.

6. На основе метода совместных вычислений установлены достаточные условия, которым должна удовлетворять динамическая семантика, задающая интерпретацию операторов программ, для того чтобы задача проверки эквивалентности последовательных программ принадлежала классам сложности КЬООБРАСЕ или РТ1МЕ.

7. Применением метода совместных вычислений доказана разрешимость

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

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

9. Предложена модификация метода совместных вычислений, при помощи которой доказана РБРАСЕ-полнота задачи проверки эквивалентности последовательных программ с операторами засылки констант.

10. Методом совместных вычислений установлены достаточные условия разрешимости задачи проверки эквивалентности унарных линейных рекурсивных программ и выделены классы динамических семантик, в которых указанная задача принадлежит классу сложности РТ1МЕ.

11. При помощи метода совместных вычислений выделен класс стандартных схем программ, в котором задача проверки эквивалентности принадлежит классу сложности РТ1МЕ.

12. При помощи метода совместных вычислений установлены достаточные условия разрешимости задачи проверки эквивалентности потоковых программ (обобщенных конечных автоматов-преобразователей) и выделены классы динамических семантик, в которых указанная задача принадлежит классу сложности РИМЕ.

Публикации по теме диссертации

1. Захаров В.А. Схемы Янова с автоматными сдвигами // Тезисы докладов VIII Международной конференции «Проблемы теоретической кибернетики». - 1988. — с. 101-102.

2. Захаров В.А. Автоматные модели программ // Доклады АН СССР. — 1989. — т.309, N 1, — с. 24-27.

3. Захаров В.А. Условия свободной схемы в формальных моделях программ // Тезисы докладов IX Международной конференции «Проблемы теоретической кибернетики». — 1991. — с. 94-96.

4. Захаров В.А. Формальные модели и свободные схемы программ // Программирование. — 1992. — N 2. — с. 10-24.

5. Захаров В.А. Об одном критерии сравнения операторных формальных моделей / / Программирование. —1993. — N 4. — с. 1225.

6. Захаров В.А. Об одном типе эквивалентности схем программ // Методы и системы технической диагностики, Саратовский государственный университет. — 1993. — вып.18. — с.68-70.

7. Захаров В.А. Об отношении аппроксимируемости семантик операторных программ // Вестник Московского университета. — Серия 15, вычислительная математика и кибернетика. — 1994.

- N 3. — с. 54-60.

8. Захаров В.А. О свободных схемах в формальных моделях программ // Математические вопросы кибернетики, Вып. 5. — М.:Наука, 1994. — с. 208-239.

9. Захаров В.А. Условия сглаживаемости операторных формальных моделей программ // Программирование. — 1994. — N 5.

— с. 23-40.

10. Захаров В.А. Эквивалентные преобразования схем программ в моделях, порожденных формулами динамической логики // Материалы XI международной конференции "Логика, методология, философия науки Институт философии РАН. — 1995 — т. II. — с. 137-142.

11. Захаров В.А., Подловченко Р.И. Полиномиальный алгоритм разрешения эквивалентности схем программ // Тезисы докладов XI Международной конференции «Проблемы теоретической кибернетики». — 1996. — с. 6869.

12. Подловченко Р.И., Захаров В.А. Быстрые алгоритмы распознавания эквивалентности в моделях операторных программ с коммутирующими операторами // Сборник "Компьютерные аспекты в научных исследованиях и учебном процессе.— М.:Изд-во МГУ, 1996. — с. 3-8.

13. Захаров В.А. Полиномиальный алгоритм разрешения проблемы эквивалентности унарных линейных рекурсивных схем программ // Труды II Международной конференции «Дискретные модели в теории управляющих систем». — 1997. — с. 26-29.

14. Подловченко Р.И., Захаров В.А. Полиномиальный по сложности алгоритм, распознающий коммутативную эквивалентность схем программ // Доклады РАН, серия Информатика. — 1998. - т. 362, N 6. — с. 27-31.

15. Захаров В.А. Быстрые алгоритмы разрешения эквивалентности операторных программ на уравновешенных шкалах // Математические вопросы кибернетики, вып.7. — М.:Физматлит, 1998. — с. 303-324.

16. Захаров В.А. О проблеме эквивалентности операторных схем на упорядоченных полугрупповых моделях // Сборник трудов III Международной конференций «Дискретные модели в теории управляющих систем», Красновидово-98. - 1998. - с. 36-40.

17. Захаров В.А. Аппроксимация абстрактных семантик формальными моделями программ // Дискретная математика. — 1998.

— т. 10, вып. 4. — с. 119-141.

18. Захаров В.А. О проблеме эквивалентности пропозициональных программ над полугруппами // Kurosh Algebraic Conference'98, Abstracts of Talks. - 1998. - c. 170-172.

19. Zakharov V.A.. An efficient, and unified approach to the decidability of equivalence of propositional program schemes // Lecture Notes in Computer Sciencc. - 1998. - v. 1443. - p. 247-258.

20. Захаров В.А. Об одном критерии сравнимости формальных моделей программ // Сборник трудов семинара по дискретной математики и ее приложениям, (2-4 февраля, 1998 г.), М.: Изд-во механико-математического факультета МГУ. - 1998. - с. 107-109.

21. Захаров В.А. Быстрые алгоритмы разрешения эквивалентности пропозициональных операторных программ на упорядоченных полугрупповых шкалах // Вестник Московского университета, сер. 15, Вычислительная математика и кибернетика.

— 1999, N 3. — с. 29-35.

22. Захаров В.А. Об эффективной разрешимости проблемы эквивалентности линейных унарных рекурсивных программ // Математические вопросы кибернетики, вып. 8. — М.:Наука, 1999.

— с. 255-273.

23. Захаров В.А. О разрешимости проблемы эквивалентности в одном классе операторных программ // Сборник "Прикладная математика и информатика вып. 5. - Изд-во ВМиК МГУ, 1999. - с. 90-100.

24. Zakharov V. A. On the decidability of the equivalence problem for orthogonal sequential programs /7 Grammars. — 1999. — v. 2, N 3. — p. 271-281.

25. Захаров В.А. О проблеме эквивалентности унарных металинейных рекурсивных схем // Тезисы докладов XII международной конференции «Проблемы теоретической кибернетики», Часть 1. — 1999. — с. 78.

26. Захаров В.А. Общие методы построения разрешающих алгоритмов для проблемы эквивалентности пропозициональных операторных программ // Сборник трудов IV Международной конференции «Дискретные модели в теории управляющих систем», Красновидово-00. — 2000. — с. 25-29.

27. Захаров В.А., Соколова К.А.. О разрешимости проблемы эквивалентности в одном классе металинейных унарных рекурсивных программ // Сборник трудов IV Международной конференции «Дискретные модели в теории управляющих систем», Красновидово-00. — 2000. — с. 29-31.

28. Захаров В.А. О проблеме эквивалентности для схем программ с операторами засылки констант // Сборник трудов IV Международной конференции «Дискретные модели в теории управляющих систем», Красновидово-00. - 2000. - с. 153-154.

29. Захаров В.А., Кузюрин Н.Н., Холодов А.Н., Шабанов JI.B., Шокуров А.В. Эффективные алгоритмы и их программные реализации // Труды Института Системного программирования: Том 1. - М.:ИСП РАН, 2000. - с. 115-124.

30. Zakharov V.A.. On the decidability of the equivalence problem for monadic recursive programs // Theoretical Informatics and Applications. — 2000. — v. 34, N 2. - p. 157-171.

31. Zakharov V.A. On the approximation relation on dynamic logic models // Abstracts of contributed papers, Logic Colloquium 2000, Paris, La Sorbonne, 23-31 juillet 2000. - 2000.

32. Захаров В.А. О проблеме эквивалентности операторных программ на одном классе уравновешенных шкал // Материалы VII Международного

семинара «Дискретная математика и ее приложения», Изд-во механико-математического ф-та МГУ. — 2001. — с. 54-57.

33. Захаров В.А. О проблеме эквивалентности операторных программ на уравновешенных однородных обратимых шкалах // Математические вопросы кибернетики. Вып. 10. — Физматлит, 2001. — с. 155-166.

34. Zakharov V.A.. The equivalence problem for computational models: decida-ble and undecidable cases // Lecture Notes in Computer Science. — 2001. — v. 2055. - p. 133-153.

35. Захаров В.А. Вычисление инвариантов последовательных программ // Тезисы докладов XIII Международной конференции «Проблемы теоретической кибернетики», Часть 1. — 2002. — с. 68.

36. Захаров В.А., Захарьящев И.М. Об одной полисемантической модели последовательных программ // Труды V Международной конференции «Дискретные модели в теории управляющих систем», (Ратмино, 26-29 мая 2003 г.). - 2003. - с. 33-34.

37. Zakharov V.A., Zakharyaschev I.M. An equivalence-checking algorithm for polysemantic models of sequential programs // Proceedings of the International Workshop on Program Understanding (14-16 July, Altai Mountains, Russia). - 2003. - p. 59-70.

38. Захаров В.А. Об одной алгебраической модели программ, связанной с обработкой прерываний // Материалы VIII Международного семинара «Дискретная математика и ее приложения», Изд-во механико-математического ф-та МГУ. - 2004. - с. 129-131.

39. Захаров В.А., Захарьящев И.М. О сложности проблемы эквивалентности в модели программ с перестановочными и монотонными операторами // Материалы VIII Международного семинара "Дискретная математика и

ее приложения Изд-во механико-математического ф-та МГУ. — 2004. — с. 131-134.

40. Захаров В.А., Захарьящев И.М. О проблеме эквивалентности для программ с частично перестановочными и монотонными операторами // Труды VI-ой Международной конференции «Дискретные модели в теории управляющих систем», (7-11 декабря 2004 г., Москва). — 2004. — с. 105-110.

41. Zakharov V.A., Zakharyaschev I.M. On the equivalence-checking problem for polysemantic models of sequential programs // Труды Института Системного программирования: Том 6. - М.:ИСП РАН., 2004. - с. 182-199.

42. Zakharov V.A., Zakharyaschev I.M. On the equivalence-checking problem for sequential programs with partially commuting and monotonic statements // Proceedings of the XI Congress of Mathematics of Serbia and Montenegro (September 28-October 2, 2004), Petrovac, Montenegro. - 2004. - p. 79.

43. Захаров B.A., Подловченко Р.й. Проверка эквивалентности программ: модели и алгоритмы // Тезисы докладов XIV Международной конференции «Проблемы теоретической кибернетики», Пенза, 23-28 мая, 2005. - 2005.

44. Захаров В.А., Подловченко Р.И., И.М. Захарьящев, Д.М. Русаков, B.JI. Щербина. О возможности применения быстрых алгоритмов проверки эквивалентности программ для обнаружения вирусов // Труды 2-ой Всероссийской научной конференции «Методы и средства обработки информации», Москва, 2005. — 2005. - с. 414-421.

45. Zakharov V.A., Zakharyaschev I.M. On the equivalence checking problem for a model of programs related with muti-tape automata // Lecture Notes in Computer Science. - 2005. - v. 3317. - p. 293-305.

46. Podlovchenko R.I., Rusakov D.M., Zakharov V.A.. On the equivalence problem for programs with mode switching // Lecture Notes in Computer Science.

- 2006. -v. 3845 -- p. 351-352. < ■ :T

47. Захаров В.А., Щербина B.J1. О сложности распознавания эквивалентности машин Тьюринга без записи на ленту // Материалы XIV международной школы-семинара «Синтез и сложность управляющих систем» (Санкт-Петербург, 26-30 июня 2006 г.). - 2006. - с. 147-150.

48. Варновский Н.П., Захаров В.А., Кузюрин H.H., Шокуров A.B., Подлов-ченко Р.И., Щербина B.JT. О применении методов деобфускации программ для обнаружения сложных компьютерных вирусов // Известия ТРТУ, Таганрог, Изд-во ТРГУ. - 2006. - с. 53-57.

49. Podlovchenko R.I., Rusakov D. М., Zakharov V.A. The equivalence problem for programs with mode switching is PSPACE-complete // Труды Института Системного программирования: Том 11. — М.:ИСП РАН, 2006. — с. 111-135.

50. Варновский Н.П., Захаров В.А., Кузюрин H.H., Шокуров A.B. Современные методы обфускации программ: сравнительный анализ и классификация // Известия ЮФУ. — 2007. — N 1.

— с. 93-99.

51. Захаров В.А., Щербина В.Л. Об эквивалентности программ с операторами, обладающими свойствами коммутативности и подавления // Материалы 9-го Международного семинара «Дискретная математика и ее приложения», Москва, 2007. - 2007. - с. 191-194.

52. Zakharov V.A., Kuzurin N.N., Podlovchenko R.I., Shcherbina V.V. Using algebraic models of programs for detecting metamorphic mal wares // Труды Института Системного программирования: Том 12. — М.:ИСП РАН, 2007. - с. 77-94.

53. Захаров В.А., Щербина B.JI. Эффективные алгоритмы проверки эквивалентности программ в моделях, связанных с обработкой прерываний // Вестник Московского университета,

сер. 15, Вычислительная математика и кибернетика. N 2. - с. 33-41.

— 2008,

54. Захаров В.А. О проблеме эквивалентности в одном классе монадических линейных рекурсивных программ // Тезисы докладов XV-ой международной конференции «Проблемы теоретической кибернетики» (Казань, 2-7 июня, 2008 г.) - 2008. - с. 40.

55. Захаров В.А., Щербина B.JI. О сложности проверки эквивалентности программ с операторами засылки констант // Труды VIII-ой Международной конференции «Дискретные модели в теории управляющих систем», Москва, 6-9 апреля 2009 г. - 2009. - с. 369-374.

56. Zakharov V.A. Two-tape machinery for the equivalence checking of sequential programs // Proceedings of the International Workshop on Program Understanding, Novosibirsk. - 2009. - p. 28-40.

57. Захаров В.А. Проверка эквивалентности программ при помощи двухлен-точных автоматов // Кибернетика и системный анализ. — 2010. — N 4. - с. 39-48.

58. Подымов В.В., Захаров В.А. Об одной полугрупповой модели программ, определяемой при помощи двухленточных автоматов // Научные ведомости Белгородского государственного университета, Серия История. Политология. Экономика. Информатика. — 2010. — вып. 14/1, N 7. — с. 94-101.

59. Zakharov V.A. Equivalence checking of sequential programs using two-tape automata // International Workshop "Automata, algorithms, and information technologies". Abstracts. Kiev, May 19-21, 2010. - 2010. - c. 25.

60. Подымов B.B., Захаров В.А. О двухленточных машинах, описывающих полугруппы с сокращением // Материалы 16-й Международной конференции "Проблемы теоретической кибернетики Нижний Новгород, 20-25 июня 2011. - 2011. - с. 372-375. " '

Отпечатано в копицентре « СТ ПРИНТ » Москва, Ленинские горы, МГУ, 1-ый гуманитарный корпус, e-mail: globus9393338@yandex.ru тел.: 939-33-38 Тираж ) 00 экз. Подписано в печать 15.11.2011