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

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

На правах рукописи

Костылев Егор Вячеславович

АЛГОРИТМЫ АНТИУНИФИКАЦИИ И ИХ ПРИМЕНЕНИЕ ДЛЯ ВЫЧИСЛЕНИЯ ИНВАРИАНТОВ ПРОГРАММ

Специальность 01 01.09 - дискретная математика и математическая кибернетика

АВТОРЕФЕРАТ диссертации на соискание учёной степени кандидата физико-математических наук

Москва - 2008

003454068

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

Научный руководитель: кандидат физико-математических наук,

доцент

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

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

профессор

Эльяр Эльдарович Гасанов,

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

Владимир Анатольевич Башкин.

Ведущая организация: Математический институт имени В.А. Стекло-

ва Российской Академии наук.

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

С диссертацией можно ознакомиться в библиотеке факультета ВМиК МГУ. С текстом автореферата можно ознакомиться на официальном сайте факультета ВМиК Московского государственного университета имени М. В. Ломоносова http://www.cs.msu.su в разделе «Наука» - «Работа диссертационных советов» -«Д 501.001.44».

Автореферат разослан ноября 2008 г.

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

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

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

Актуальность темы. Задача антиунификации (англ. generalization) была впервые рассмотрена в работах Г. Д. Плоткина1 и Дж. Рейнольдса2. Она состоит в том, чтобы для двух заданных выражений Ei и Е2 отыскать наиболее специальное выражение Eq, примерами которого являются оба выражения Ei и Ег, то есть существуют подстановки tfj и $2, для которых выполняются равенства Е\ = Erfi и Е2 — Такое выражение Eq называется наименее общим шаблоном выражений Е\ и Е2.

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

Задача антиунификации исследовалась значительно меньше. В ряде работ были предложены различные алгоритмы антиунификации, и в некоторых случаях была исследована сложность этой задачи В частности, было установлено, что в том случае, когда термы представляются в виде деревьев, задача антиунификации подстановок является NC-полной (в отличие от задачи унификации, которая относится к числу Р-полных задач). Также было показано, что если суммарный размер деревьев, представляющих термы, не превышает числа N, то антиунификацию можно провести за время C?(log2 N) с использованием N/\og2N процессоров в модели параллельных вычислений EREW PRAM. В этой же работе было показано, что в том случае, когда нескольким процессорам разрешается одновременно проводить операции считывания и записи, относящиеся к одной и той же ячейке общей памяти (модель параллельных вычисле-

'Plotkin G D A note on inductive generalization Machine Intelligence, 1970, v. 5, N 1, 1970, pp 153 163 'Reynolds J.С Transformational sj stems and the algebraic structure of atomic formulas. Machine Intelligence, v S, N 1, 1970, pp. 135 -151

3Robinson J A. A machine-onented logic babed on the resolution princpie Journal of the ACM, v. 12, N 1,

1965, pp 23-41.

J

ний CRCW PRAM), антиунификацию для древесных термов можно провести за время 0(log N) с использованием N/ log N процессоров. Однако сложность задачи антиунификации в том случае, если для представления термов используются структуры данных, отличные от деревьев, ранее не исследовалась.

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

Э3/1З1/2... Byk(vj. = <i Л v2 = t2 А ... Л vn = tn),

где vi%v2,.. ■ ,vn — переменные программы, a t\,t2,... ,tn — некоторые термы. Особый интерес представляет наиболее специальный сильный инвариант в классе инвариантов равенства, то есть такая формула, из которой в свободных (эрбрановских) интерпретациях логически следуют все инварианты равенства в этой точке.

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

4Apt К R , Olderog Е -R. Vérification of Sequential and Concurrent Programa Springer, 1997, 364 p

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

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

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

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

Основные результаты работы и научная новизна.

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

5Сабельфельд В К. Полиномиальная оценка сложности распожавания логико-термалыюй зквивалентно-сти Доклады АН СССР, 1979, т 249, N 4, с 793-796

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

3. Предложена концепция метаподстановки, обобщающая понятие подстановки, и установлены основные алгебраические свойства метаподстановок.

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

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

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

Апробация работы. Представленные в диссертации результаты докладывались на семинаре факультета ВМиК МГУ по теоретическим вопросам программирования под руководством Р. И. Подловченко и В. А. Захарова, на ХШ-й международной школе-семинаре «Синтез и сложность управляющих систем» (2002, Пенза), на VIII-м международном семинаре «Дискретная Математика и ее приложения» (2004, Москва), на всероссийской конференции студентов, аспирантов и молодых ученых «Технологии Microsoft в теории и практике программирования», (2005, Москва), на XIV международной конференции «Проблемы теоретической кибернетики», (2005, Пенза).

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

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

КРАТКОЕ СОДЕРЖАНИЕ РАБОТЫ Во введении приведено общее описание задачи антиунификации выражений (термов, формул, подстановок) и смежных с ней задач. Представлен обзор проведенных ранее исследований этих задач, сформулированы основные задачи и цели диссертационной работы. Рассмотрены возможные применения алгоритмов антиунификации, в том числе исследуемое в этой работе применение антиунификации для вычисления инвариантов программ.

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

В разделе 1.1 приведены определения базовых понятий, используемых в диссертации. Пусть Т = ■. •, /т™'} ~ конечное множество функциональных символов конечных валентностей П\,..., пт, а X и У - произвольные множества переменных. Терм - это (1) либо переменная из У; (2) либо выражение /^(¿1, • ■. ,£п), гДе 6 Т, а ¿1,... ,4„ - термы. Множество термов обозначается Тегт[У,Р]. Конечной подстановкой называется любое отображение $: X —» Тегт[У, .Т7], для которого множество переменных Оот($) — {х 6 X \ х} конечно. Каждая конечная подстановка г? может быть представлена множеством пар {х\1гд{х\),..., хп/<д{хп)}, где {х\,... ,хп} = Оот{д). Множество всех конечных подстановок обозначается ЭнЬя^Х, У, Композиция 1е ЗиЬ&[Х,У,1] подстановок $ 6 БиЬь^Х,У,?) и £ е ЗиЬ8г[У,У,Т) определяется равенством — 6 X. На множестве БиЬз^Х, У, Т] вводится предпорядок С:

$1 Е е БьЬ^У, У, Т\ : ч92 =

Этот предпорядок порождает отношение эквивалентности ~ и индуцирует на фактор-множестве частичный порядок Частично упорядоченное множество (ЗиЪв1\Х,У,!Р]/ <) образует полную решетку. Операция | взятия точной нижней грани в этой решетке называется операцией антиунификации подстановок. Традиционным представлением термов и подстановок являются корневые ориентированные помеченные упорядоченные деревья и наборы (леса) из

таких деревьев соответственно. Более компактной формой их представления являются ациклические ориентированные графы (АОГ), полученные из деревьев и лесов склеиванием всех изоморфных поддеревьев. Не содержащий несовпадающих изоморфных поддеревьев АОГ называется редуцированным. Размером N{d) подстановки i? называется количество вершин в представляющем ее редуцированном АОГ.

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

Теорема 1.3. Сложность алгоритма антиунификации nodcmanoeoK'MST равна O(NlogN), где N - размер выходной подстановки. Теорема 1.4. Если в множестве Т найдется функциональный символ валентности т, т > 1, то существует такая последовательность пар подстановок (t?i, $'{),...,О,... из Subst[X, У, Т], что

\N(^)-N(fn)<N^niK),n> 1.

Следствие 1.5. Сложность задачи антиунификации подстановок, представленных АОГ, оценивается сверху величиной 0{N2 log N), а снизу - величиной tt(N2), где N - суммарный размер исходных подстановок.

Раздел 1.3 посвящен параллельным алгоритмам антиунификации подстановок, представленных АОГ. В его начале представлена схема алгоритма распознавания точного антиунификатора MSTPChk. С использованием этого алгоритма доказана следующая теорема.

Теорема 1.16. Проблема проверки равенства г] = д' [ ß" для любых представленных редуцированными АОГ подстановок rj, и т?2 из Subst[X, У, Т] принадлежит классу сложности

В алгоритме MSTPChk существенно используется структура АОГ, представляющего подстановку г\, поэтому использовать его для вычисления точной нижней грани подстановок невозможно. Далее в том же разделе представлена схема алгоритма построения точного антиунификатора MSTPCmp.

Теорема 1.19. Алгоритм MSTPCmp для произвольных подстановок и г?" из SubstlX^,^, представленных редуцированными АОГ, вычисляет редуцированный АОГ, представляющий подстановку Т) — ft' | с использованием 0(N5) процессоров за время 0(\og2N), где N = max(N(i}'), 7V($")).

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

В начале раздела описана математическая модель одномодульных программ. Пусть задано конечное множество функциональных символов J17. Программа П определяется тройкой множеств {V, С, Ор), в которой (1) V ~ {vi,..., fn} — это упорядоченное конечное множество переменных, которые будем называть рабочими; (2) С = {entry, Zj,..., Zr} — конечное множество точек программы, в котором выделена точка входа entry; (3) Op — множество операторов вида (Zj : v := t : Z2), где Zi,Z2 £ С, h ф entry, w e V, и i € Term[V,F]. Для каждого оператора (ii : v :— t : I2) положим Beg(op) — l\ и End(op) = I2. Трасса tr в программе П — это конечная последовательность точек и операторов, такая что (1) либо tr = (entry); (2) либо tr ~ (entry,...,I',op,l) в том случае, если ¿г' = {entry,...,/') — это трасса в программе П, а ор = (I' : v := t : I) — оператор из Ор (в этом случае будем использовать запись tr = tr'+(op, I)). Множество трасс, оканчивающихся в точке1, обозначим TV(Z). Каждому оператору op = (l\ : v := t. I2) сопоставим подстановку шор — {v/t} из V, а каждой трассе tr = (entry, opi,l\,..., k-\, opt, lt) — подста-

новку r)(tr)=Lj0Pt... uim из Subst[V, V, J^.

Пусть / = {Dj, fi"\..., fmm\ = } — алгебраическая система первого порядка сигнатуры Т = f[ni\ ..., /т с предметной областью Dj, оценкой функциональных символов f[n>\-..,fmm^ и предикатом равенства =. В дальнейшем систему I будем называть интерпретацией. Оценка произвольного множества переменных Q в интерпретации I — это отображение а : Q —> £>/. Множество оценок Q в интерпретации I обозначим 11/(2). Для любого терма t е Term[Q, и произвольной оценки сг е £/(<2) запись t[a\ указывает значение, принимаемое термом t в интерпретации I, когда значения переменных t определяются оценкой а. Для произвольных множеств переменных Q и Q',

оценок а £ Ej(Q) и ег' 6 S/(Q')> переменной v 6 Q и терма t е Term[Q',.F] значение оценки сг[г> <— /[а']] 6 E;(Q) для переменной г; полагается равным í[a'], а для любой другой переменной из Q — значению ст.

Состоянием в программе П = {V, С,, Ор] называется произвольная пара (¿,£т), в которой Z е £ и ст € S/(V). Пусть tr - трасса в программе П, а сто оценка из множества E;(V). Вычисление comp(tr,ao) трассы tr для начальной оценки сто ~~ это последовательность состояний и операторов, удовлетворяющая следующим требованиям: (1) если tr = (entry), то comp(tr,aо) = ((entry, сто)); (2) если tr = tr' + {op, I) и при этом известно, что comp(tr', со) — ((entry,<т0),•••,(¿',<7')), то

comp(tr, (т0) = {(entry, <т0),..., (I', У), op, (I, о> <- í[ít']])).

Формула логики предикатов Ф(У), зависящая от переменных программы, называется инвариантом в точке I программы П = {V, £, Ор} для интерпретации I, если для любой трассы tr 6 Tr(l), ведущей в точку I, и произвольной оценки Со £ £r(V) вычисление comp(tr,aо) = ((entry, сто),... ,ор, (I, ст)) порождает оценку (т переменных V, при которой формула Ф(У) выполняется в интерпретации I, то есть верно соотношение I f= Ф(У)[<т]. Инвариант Ф(У) называется инвариантом равенства, если он имеет вид:

3yi3y2... 3yk(vi = h Л v2 = f2 A • • • A vn = t„),

где f, e Term\y,F\, 1 < г < n, y3 <E >*, 1 < j < к. Пусть F¡(I) - произвольное множество инвариантов в точке I для интерпретации I. Инвариант Ф(У) 6 F/(¿) назовем наиболее специальным в F;(¿) если для любого инварианта Ф'(У) 6 F/(Z) верно 7 [= (Ф(У) —► Ф'(У))[сг]. Формулу Ф(У) назовем сильным инвариантом в точке I, если Ф(У) является инвариантом для любой интерпретации I. Инвариант является сильным тогда и только тогда, когда он является инвариантом для эрбрановской интерпретации /[У, =

Для любой точки I программы П = {V, С,Ор} рассмотрим подстановку

Щ = Wr(/) №r){vily\.....Уп/уп}).

10

Каждой подстановке $ = {«l/ti, ■■■>vn/tn} из Subst[V,У,F] сопоставим формулу ФДУ) = Зу\... = ti Л ... Л vn = in), где у\,...,ут € У - все переменные встречающиеся в термах ..., tn.

Теорема 1.27. Формула Фад(У) является наиболее специальным сильным инвариантом равенства программы П = {V, С, Ор] в точке I.

Показано, что набор подстановок д(I), I е С, является наименьшим решением системы уравнений с переменными 0;:

Г2(П) • < ^ор^Вед(ор), I & £,1ф entry,

\ ©entry = {ui/yi, ■ - - , Vn/Vn}-

Решение этой системы может быть получено при помощи стандартных итерационных методов, широко используемых при решении задач статического анализа программ6. В то же время, для произвольной точки I инвариант равенства Фад(у) строится непосредственно из АОГ подстановки д{1).

Целью второй главы является разработка обобщения понятия конечной подстановки, которое

(1) охватывает операции композиции и ангиуннфикации,

(2) удовлетворяет более широкому спектру алгебраических законов,

(3) пригодно для вычисления инвариантов многомодульных программ.

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

В разделе 2.1 даны определения базовых понятий главы - контекста, мета-контекста и метаподстановки, - введены операции композиции и антиунификации (взятия точной нижней грани) в решетке метаподстановок и установлены их основные алгебраические свойства. Далее для краткости запись А = .А'+.4" будет использоваться для обозначения того факта, что для множеств Л, Л1 и Л" верны соотношения Л'И Л" = Л и Л'Г) Л" = 0. Пусть заданы (1) два множества предметных переменных Vi = {и1,..., vn,...} и Уг; (2) конечное множество функциональных символов К, включающее множество констант С-ц', (3) бесконечное множество служебных переменных Ы = {Di,Ufo,...}. Терм s 6 Term^UU, "Н] называется сингулярным, если (1) либо s 6 V2 U Ск\ (2) либо s = Лр1,... ,Dfe_i,s', Djfc+i,.. .,□«)) где h^ еН, s' - сингулярный терм,

"Nielson F, Nielson Н R, Hankin С. Principles of Program Analysis, Springer-Verlag, 1999, 450 p.

a Di,..., Dfe-i, Dfe+i,..., □„ G U - различные переменные, не содержащиеся в s'. Таким образом, сингулярный терм представляется ветвью в древесном представлении обычного терма; остальные ветви «обрезаны» служебными переменными. Записи Top(s) и Leaf(s) будут обозначать символы на вершине и на конце ветви, представляющей сингулярный терм s. Если для сингулярных термов s, s\ и S2 верно равенство s = si{v/s2}, где v = Leaf(s\), то для обозначения этого будем использовать запись s = S\{s2)-Контекстом назовем произвольную подстановку вида

х = {vVDi, • • .,vk-ljUk^ls,vk+1lUk+l,... ,тЛ/Ц„...},

в которой (1) s - сингулярный терм и (2) di,... ... ,ПП,... - по-

парно различные переменные из U, не входящие в s. В дальнейшем будем использовать запись {... vk/s...} для обозначения контекста я указанного выше вида и полагать Dom(x) — vk. Множество контекстов с попарно непересекающимися множествами служебных переменных обозначим Cont[V\, V2, TL\. Будем говорить, что подстановка $ € .SubsifVi, V2, Н] инициализирует контекст к, если для некоторой подстановки a G Subst[U, У2, Н] выполняется равенство яа = 1?.

Пусть задано еще одно множество предметных переменных V3, а в множестве V2 выделено подмножество V2. Рассмотрим операцию композиции множеств контекстов. Для множеств контекстов К\ С ConiJVi, V2, Н] к К2 Q Cont[V2, V3, Н] положим

Кх ■ К2= ft*11 = {• • ■ • • •} е ^ь Leaf(s) $ V^}, если К2 = 0,

1 2 \{>С1Х2\Ъ е K1,X2€K2,x1K2£Cont[VhV3UVZ,?{\},eaiuK2yi0. Доказано, что для операции композиции • множеств контекстов выполняются закон ассоциативности, а также законы левой и правой дистрибутивности относительно объединения.

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

Пусть в множестве Н выделено подмножество 7i'. Два сингулярных терма Si и «2 из STerm\y2, W] называются несогласованными по множествам V2 и Н', если существуют такие сингулярные термы s, s^ и s2, для которых верны соотношения sj = «(sj), s2 = 5(5г)> Top(s'j) ф Top(s'2) и при этом справедливо одно из следующих требований: (1) Top(s[) 6 V2, или (2) Top(s2) € Ц, или (3) Top(s'i) еН'и Top(s'2) S И'. Таким образом, два сингулярных терма несогласованы, если при наложении представляющих их ветвей либо переменная из V2 накладывается на любой отличный от нее символ, либо функциональный символ из Н' накладывается на другой символ из Н'. Контексты — {.. .vl/si...} и х2 = {... v2/s2 ...} из Coni[Vi, V2,H] называются согласованными по множествам V2 и Н', если либо vl фи2, либо термы si и s2 не являются несогласованными. Множество попарно согласованных контекстов назовем метпаконтекстом.

Пусть каждое из множеств V2 пТС разбивается на два подмножества: V2 = V2 + V2 и П = W + И". Множество контекстов К С Cont[Vu V2,H] называется линейным по множеству переменных V2, если каждая переменная из V2 встречается в контекстах из К не более одного раза. Множество линейных метаконтекстов обозначим LMCont[Vi,V2, V2,Н',Н"].

Перейдем к описанию решетки линейных метаконтекстов и ее основных свойств. Рассмотрим множество LMCont[X,y, Z,T, V\, где X и У - введенные в первой главе множества рабочих и вспомогательных переменных, Т -конечное множество функциональных символов, Z - конечное множество входных переменных, аР = • ■ ■ - конечное множество процедурных символов, имеющих статус функциональных переменных. На этом множестве определим отношение предпорядка. Для любых метаконтекстов Si и S2 из LMCont[X, У, Z, Т, V] положим:

Si < S2 <=>• ЭР s LMCont\y, У, Z, Т, V), такой что S2.

Теорема 2.12. Отношение < задает предпорядок на LMCont[X, У, Z, Т, V] Предпорядок < порождает отношение эквивалентности ~ и индуцирует на фактор-множестве LMCont~[X, У, Z, Т, V] отношение частичного порядка Метаконтекст R из LMCont\y,y,Z,T, Р] назовем переименованием, если на множестве У существует такая биекция ф, что для каждой переменной у & У

верно включение {... у/ф(у)...} € Д.

Теорема 2.13. Соотношение Si ~ ¿2 для произвольных метаконтекстов Si и S2 из LMCont[X, У, Z, F, V) верно тогда и только тогда, когда существует переименование R, такое что — S2 • R-

Теорема 2.18. Множество (LMCont~\X,y,Z,T,Vобразует полную нижнюю полурешетку.

Операция взятия точной нижней грани в этой решетке обозначается символом Теорема 2.13 позволяет рассматривать линейные метаконтексты с точностью до переименований из множества LMCont[y, У, Z, Т, V].

Множество линейных метаконтекстов относительно операции композиции ■ не замкнуто. Поэтому целесообразно ввести еще одну операцию композиции метаконтекстов о, для которой указанное свойство выполняется. Пусть A4, Х2 и Х3 - конечные множества предметных переменных. Для любых метаконтекстов Si е LMConst~[Xh У,ХЪТ,Т>\ и S2 € LMCont~{X2,y,X3,F,V] положим

Si о S2 =4LeSr52 {*}■

Важным частным случаем метаконтекстов, необходимым при вычислении инвариантов равенства, являются беспроцедурные метаконтексты, то есть метаконтексты, не содержащие символов из Z U V. Для каждого метаконтекста S из LMCont~[X, У, Z,T, V] обозначим WP(S) максимальное беспроцедурное подмножество S.

Перейдем к рассмотрению свойства полноты множеств контекстов. Оно позволяет сопоставить полному метаконтексту множество подстановок, а, значит, и формулу определенного вида, что необходимо для вычисления инвариантов равенства. Множество контекстов К из Cont[Vi, V2, Щ назовем полным, если: (1) для любой переменной v £ Vi существует контекст к € К, такой что Dom(x) — v; (2) для любого контекста х = {...v/s...} из множества К, для любых сингулярных термов si, s2 и s3, таких что s = Si(fi2) и s2 = ...,□,_1,яз,□,+!,...,□„),ft^ е Н, и для любого номера j,

1 < 3 < п, в К существует контекст V = {.. .v/s'...}, где s' — si(s'2), S2 = h^iPi,..., Dj-i, S3, Dj+i,..., □„), a S3 - произвольный сингулярный терм. Как отмечалось выше, для каждого контекста я = {...v/s...} из множества К сингулярный терм s представляется ветвью в дереве некоторого терма t. Тогда

свойство полноты подразумевает, что вместе с х в К содержатся контексты л/, которые представляют все остальные ветви терма^. Полный линейный метакон-текст называется метаподсгпановкой. Множество метаподстановок обозначается ЬМЗиЪз1~\Х, У, 2, Т, V]. Доказано, что это множество замкнуто относительно композиции о и операции взятия точной нижней грани ^ в решетке ме-таконтекстов, то есть является подрешеткой решетки ЬМСогй~[Х, У, 2, Т, V]. Благодаря тому, что для метаподстановок выполняются свойства согласованности, линейности и полноты, верны следующие две теоремы. Теорема 2.33. Для операции композиции метаподстановок о выполняется закон ассоциативности.

Теорема 2.36. Для произвольных непустых множеств метаподстановок §1 С ЬМЗиЬзГ[Х1,У,Х2,^,Т] в§2 £ ЬМЗиЬзГ[Х2,У,Х3,Т,Т] верно равенство:

ih.es, 0 (%2е§2 = %1е8ь52е82 (5з О52). Следствие 2.37. В решетке метаподстановок выполняются законы левой и правой дистрибутивности композиции о относительно антиунификации

Установим теперь связь между метаподстановками и подстановками. Для этого рассмотрим важный частный случай метаподстановки. Метаподстанов-ку 5 из множества ЬМЗиЬз^[Х¡У,2,Т, Р] назовем конечной минимальной, если она конечна и любое ее собственное подмножество не является метапод-становкой. Множество всех конечных минимальных метаподстановок обозначается РЬМЗиЬзГ"[Х,У,2,Т,'Р]. Оно замкнуто относительно композиций • и о. Для каждой метаподстановки 5 из множества FLMS'u6sí~[A,, У, 2, Т, Р] существует единственная подстановка € й'иЬвГ"^, У 112,^11 Р], инициализирующая все контексты из 5. Подстановку $ из ЗиЬзЬ~[Х, У и 2,Т 1)Р] назовем линейной, если любая переменная из У встречается в ней не более одного раза. Каждой линейной подстановке г? сопоставим множество г? всех контекстов из Согй\Х,У иЯ.^и Р], которые ей инициализируются. Это сопоставление задает изоморфизм между множествами линейных подстановок и конечных минимальных метаподстановок. Для каждой метаподстановки 5 определим множество подстановок

0(5) = {<%, | 5' е РЬМЗиЪзГ[Х,У, 2,Т,Т\,3' С 5}.

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

Проекцией метаподстановки 5 на переменную х £ X назовем метаконтекст ¿¡■[¡с] = {х | х £ 3,Вот(х) = х}. Пусть в множестве поцедурных символов V выделено подмножество V' и каждому символу р^ 6 V сопоставлены множества переменных Х^ и 23 мощности п3, метаподстановка £ ЬМ8иЬ8А~[Х],У,2},Р,'Р] и переменная х, € X). Конкретизацией процедурных символов V метаподстановки 5 проекциями 51[?1],... , .^-[аУ назовем метаподстановку

_ (тц) (пц) _ _ ___ _

|[гк]ЬС°д1оР1о...од>оР'о....

В этом определении метаподстановки С^', г > 1, и С составляют ту часть метаподстановки 5, которая не содержит процедурных символов из множества V, а метаподстановки Рг, г > 1, определяются соответствующими проекциями из Зхр?!],..., [ж*]. Таким образом, конкретизация - это замена процедурных символов во всех контекстах метаподстановки на множества сингулярных термов из соответствующих проекций. Формально операция конкретизиции определяется на основе процедурных разложений контекстов и метаподстановок. При описании метода вычисления инвариантов равенства многомодульных

программ полезно следующее обозначение. Для любой метаподстановки 5 по-

(*п) ("А) _ _ («1) ("*) _ (п1) (*ч) (пО

ложим = 5 и = (5|[г1]; ^[й]]^1)!^]!'

<1> 0.

Рассмотрим свойства операции конкретизации. Теорема 2.51. Для непустого множества метаподстановок Б верно:

_ (П1) (п/.) _ Гпу) (п^)

Теорема 2.52. Для любых метаподстановок Б1 и Б2 верно:

(З'оЯ2]^ .....• ^ 1о яУ"1' ' ^ 1

^ Лад], ,3^-° ДИ' ° А!«!1'

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

Рассмотрим алфавит ЦХ, 2,Зг,Р] = Хи2ШгиРи{1,..., птвх} и {у}, где птах ~ это максимальная валентность символов из Т и Р, а у - новый символ. В множестве слов ^[Х, 2, Т, Р] выделим подмножество всех слов ЩХ, 2, Т, Р], имеющих вид ... И^г^г, где х е X, 6 УМр, 1 <

гл — пЦ1 ^ < I < £ 2иС и{у}, а С- множество констант в-^иР. Представлением контекста к — {... ,х//г]"и)(..., ц ■., г,...), ■ ••)>•■ •} из СопЬ[Х,У и 2, Ри Р], 6 ^и Р, 1 < I < к, назовем слово го(х) = ... из Е*{Х,2,Т,Р\, где г' = у если г € У или г' = г если г £ 2 и С. Представлением множества контекстов К С Сотй[Х, У и 2,ЗгиР], назовем язык Ь(К) = | к е К). Такое представление является однозначным для метаконтекстов из ЬМСогй~[Х,У,2,!Р,Р]. Линейное множество контекстов К С Соп^Х, У и 2, Т и Р] назовем регулярным, если язык регулярен. Множества регулярных линейных метаконтекстов и регулярных метаподстановок обозначаются ЯЬМСоп^[Х ,У, 2, Т, Р] и У, 2, Т, V) соответственно. Доказано, что эти семейства замкнуты относительно операций композиции о и ■ и антиунификации Л. Таким образом, для описания регулярных метаконтекстов можно использовать конечные автоматы. Состояния такого автомата разделяются на две группы: (1) основные состояния - состояния, переходы в которые осуществляются по символам из множества 2 и Т и Р и {у} и начальное состояние; (2) вспомогательные состояния - состояния, переходы в которые осуществляются по символам из множества X и {1,... ,птах}. Автомат, представляющий множество контекстов называется приведенным, если (1) все переходы в любое основное состояние осуществляются по одному и тому же символу, (2) в каждое вспомогательное состояние ведет один и только один переход, (3) для каждого символа

rg2 U {у} существует одно и только одно финальное состояние. Для каждого регулярного множества контекстов существует представляющий его приведенный автомат. Разработан алгоритм антиунификации метаконтекстовМСо^МЗТ, для которого верна следующая теорема.

Теорема 2.64. Алгоритм MContMST для приведенного автомата, представляющего регулярное множество контекстов К, строит представляющий ме-таконтекст S {х} приведенный детерминированный автомат.

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

Пусть задано множество функциональных симоволов Т. Пусть ^(П) - это множество процедурных символов мощности к, такое что Р(П) П Т = 0. Многомодульная программа П - это множество, модулей мощности к, такое что каждый модуль М определяется шестеркой ,v, С, Trans, Calls}, в ко-

торой: (1) р^ £ ~P(U) - уникальный среди всех модулей процедурный символ, называемый именем модуля; (2) V = {ui,...,vn} ~ упорядоченное конечное множество рабочих переменных; (3) v £ V - специально выделенная переменная, называемая выходной; (4) С = {entry,exit,¿i,...,lr} - конечное множество точек модуля, в котором выделены точки входа entry и выхода exit; (5) Trans - множество преобразователей вида (Zj : v := t : l2), где lul2 £ L, 1г ф exit, 12 ф entry, v £ V и t £ TermlV,?}-, (6) Calls - множество вызовов вида (l\ : v := callqw(ti,... ,tm) : l2) где li,l2 £ C, h ф exit, l2 ф entry, v £ V, q{m) £ Р(П) и tu...,tn £ Term\V,F\. Множеством операторов назовем множество Op = Trans U Calls. Для каждого оператора op = (li : v E : l2) положим Begiop) = l\ и End(op) = l2. Каждому модулю M = (pW ,V,v,L,Trans,Calls} сопоставим упорядоченное множество переменных входа Вм — {bi,...,b„} и метаподстановку ¡Зм из множества FLMSubst~[V, У, 0], такую что рм = {i>i/i>i,..., vnlbn}.

Каждому оператору ор из Ор сопоставим метаподстановку шор из множества FLMSubst~[V,y,V,T,V{Yl)}, такую что = {v/t}, если op = (h : v := t : l2) - преобразователь из множества Trans, и = {v/q^ih,... ,tm)}, если

op = (h : v := callq{m){t\,... ,tm) : - вызов из множества Calls.

Определим понятие трассы в модуле, одновременно с этим сопоставляя каждой трассе tr метаподстановку S(tr) из FLMSubst~[V, У, Вм, Т^П)] определенного вида. Трасса tr в модуле М - это конечная последовательность точек и операторов, такая что: (1) либо tr = (entry); в этом случае положим S(tr) = ¡вм; (2) либо tr = (entry,op, End(op)), если tr' = (entry,..., I'} - это трасса в модуле М, а ор - преобразователь из Trans; в этом случае положим S(tr) = ZjopoS{tr'); (3) либо tr = (entry,...,/', op, entry к,..., exit к, End(op)), если tr' = (entry,...,l') - это трасса в модуле М, op - вызов некоторого модуля К с именем q^ и точками входа entry^- и выхода exit к, a trjc = (entryjj-,... ^xittf) - трасса в модуле К; в этом случае положим S(tr) = uUi(i; j] о S(tr'). Множество всех трасс, оканчивающихся в точке I, обозначим Тг{1). Модуль М назовем завершаемым, если для любой его точки I существует оканчивающаяся в I трасса. Программу П назовем завершаемой, если завершаемы все ее модули.

Пусть заданы интерпретация I и программа П. Состоянием в модуле М = {р("),У = {vi,... ,vn},v,С,Trans,Calls} этой программы называется произвольная пара (/,ст), в которой I £ С и а Е S/(V). Подобно тому, как это было сделано в первой главе для одномодульных программ, для произвольной трассы tr в модуле М и любой начальной оценки сто 6 S/(V) определяется понятие вычисления comp(tr, сто) в этом модуле. Вычисление - это последовательность состояний и операторов, в которой точки состояний и операторы определяются трассой tr, а оценки состояний - начальной оценкой и преобразованиями, осуществляемыми операторами.

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

$(V) = 3j/i3j/2 • • ■ 3yk(vi = ti A v2 = t2 A ... A vn = tn),

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

Линеаризацией подстановки if £ Subst~{X, У, F] назовем линейную под-

становку Lin{$) из того же множества, для которой существует переименование с отождествлением Л, такое что Lin(i9)A = Для каждого модуля М = {У"', V = {ui,..., vn}, v, £, Trans, Calls} с множеством переменных входа Вм = {¿i)...)bn} определим метаподстановку р*и, соответствующую подстановке р*м = {h/yi,...,bn/yn} е где уи...,уп- различные переменные из ЗЛ Каждой метаподстановке S € LM Subst~\y, сопоставим подстановку = &Рм) € LSubst~\y,y,F] и формулу

Щ(уи..., v„) = 3yi... 3ут(/\ v = Щу)), где (г/1,..., ут] = УагуЩ).

v&V

В дальнейшем вместо Фу(«1,■■■ ,vn) будем использовать запись Ф^У). Для каждой точки I программы П определим подстановку

3(0 =Wrr(i) S(tr).

Теорема 3.10. Для любой точки I программы П формула Ф^^У) - это наиболее специальный сильный линейный инвариант равенства el. Утверждение 3.11. Верно равенство = Ф£,(У); где S* = S о р^.

Таким образом, для вычисления наиболее специального сильного линейного инварианта равенства в точке I достаточно построить метаподстановку S*(l). Покажем, как можно построить эту метаподстановку. Сначала определим понятие локальной трассы в модуле, одновременно с этим сопоставляя каждой локальной трассе Itr метаподстановку R(ltr) определенного вида Локальная трасса Itr в произвольном модуле М программы П с точкой входа entry -это конечная последовательность точек и операторов этого модуля, такая что

(1) либо Itr = (entry); положим для этой локальной трассы R(ltr) = (5М\

(2) либо Itr = (entry, ...,Beg (op), op, End{op)), в том случае, если Itr' = (entry,..., Beg(op)) - это локальная трасса в модуле М, а ор оператор в этом модуле; положим для этой локальной трассы R(ltr) = wop о R(ltr'). Для произвольной точки I модуля М обозначим LTr(l) множество всех локальных трасс в М, оканчивающихся в /, и определим подстановку R(l) =JJ-игитг(1) R(ltr). Теорема 3.14. Пусть П - это программа, состоящая из модулейМ\,..., Mk Пусть для каждого модуля Mt, 1 < i < к, - это его имя, и, - его переменная выхода, a exit, - его точка выхода. Тогда для любой точки I этой

программы верно равенство

_ _ pf«i) pH*)

Следствие 3.16. Для точки I выполняется соотношение

_ __0>l) (nt)

Пусть П - это программа, состоящая из модулей ..., Мк. Для каждого модуля М,, 1 < г < к, рассмотрим его имяр'"1', переменную выхода?, и точку выхода exit,. Аппроксимирующей последовательностью в точке I программы называется последовательность метаподстановок Е(П, I) = Щ,..., Щ,..., определяемая равенствами

Теорема 3.20. Пусть I - это произвольная точка завершаемой программыП, а Е(П,Z) = Яд,..., Щ,... - аппроксимирующая последовательность в этой точке. Тогда существует номер do, do > 0, такой что для као/сдого d, d> do, верно равенство WP(Rj) = S*(l).

В разделе 3.2 рассмотрен метод построения автоматных представлений элементов аппроксимирующей последовательности и предложен алгоритм вычисления инвариантов равенства многомодульных программ. Как следует из определения метаподстановки R(l) и свойств метаконтекстов, для любой точки I модуля М = {p(n\V,v, С, Trans, Calls} верно равенство R(l) =tyitreLTr(i) R{ltr) =4хезг(/) {х},1 6 гдeK(l) = \jitr€iTr{i)(R{ltr))- Подобно тому, как это было сделано в первой главе для одномодульных программ, показано, что набор языков L(K(l)), I 6 С, является наименьшим решением системы языковых уравнений с переменными X;, I £ С:

ЩМ) ■ [ Х' = U°peoPjEnd(opHL(ü°p) ■ %Веа(ор), I е С, 1ф entry, У Xentry = ЦАм)-

Автоматные представления метаподстановок ßM и ь5ор, op € Ор, легко строятся из АОГ подстановок Дм и шор, ор 6 Ор. Систему П(М) можно решать методом поиска неподвижной точки, представляя регулярные языки распознающими

их конечными автоматами. Из полученных в результате решения этой системы представлений множеств контекстов K(l), I € С, с помощью алгоритма антиунификации MGontMST можно итеративно строить все элементы аппроксимирующей последовательности в произвольной точке.

Таким образом, для вычисления наиболее специального сильного линейного инварианта равенства Ф(У) в произвольной точке I модуля М завершаемой программы П = {Mj,..., Mk} необходимо:

1. Для каждого модуля М„ 1 < г < к, построить и решить систему языковых уравнений П(М,).

2 К полученным автоматным представлениям множеств К (exit,), 1 < г < к, и К(1) применить алгоритм антиунификации MContMST и получить автоматные представления метаподстановок i?(exit,), 1 < i < к, и R(l).

3. Применяя алгоритм MContMST, итеративно строить представления членов аппроксимирующей последовательности Н(П, I) = R J,..., R*d,... до тех пор, пока беспроцедурная часть не будет полной и неизменной на протяжении d* — к х таj Len(x) шагов, где к - мощность множества V, a do - номер в начале неизменной части (как следует из теоремы 3.20, аппроксимирующая последовательность обязательно стабилизируется спустя некоторое конечное число шагов).

4. На основе автомата .4(f?Jo) построить формулу Ф(У) =

Этот алгоритм является основным результатом третьей главы. Его можно использовать для вычисления инвариантов равенства многомодульных программ.

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

ПУБЛИКАЦИИ ПО ТЕМЕ ДИССЕРТАЦИИ

[1] Костылев Е.В., Захаров В.А. Об одном обобщении подстановок применительно к задаче синтеза инвариантов программ. Материалы VIII-го Международного семинара «Дискретная Математика и ее приложения», Москва, 2004, с.134-136.

[2] Костылев Е.В. Методы вычисления инвариантов программ. Труды всероссийской конференции студентов, аспирантов и молодых ученых «Технологии Microsoft в теории и практике программирования», Москва, 2005, с.130.

[3] Костылев Е.В. О вычислении инвариантов программ. Тезисы докладов XIV международной конференции «Проблемы теоретической кибернетики», Москва, 2005, с.73.

[4] Костылев Е.В., Захаров В.А. Об одном обобщении подстановки применительно к задаче статического анализа программ. Вестник Московского Университета, 2005, сер.15, Вычислительная Математика и Кибернетика, №4, с.39-45.

[5] Костылев Е.В., Захаров В.А. О сложности задачи антиунификации. Дискретная математика, 2008, т.20, вып.1, с.131-144.

[6] Захаров В.А., Костылев Е.В. Быстрые алгоритмы антиунификации и их применение при анализе программ. Материалы XIII-й Международной школы-семинара «Синтез и сложность управляющих систем», Пенза, 2002, Часть 1, с. 76-81.

Напечатано с готового оригинал-макета

Издательство ООО "МАКС Пресс" Лицензия ИД N00510 от 01 12.99 г. Подписано к печати 29.10.2008 г. Формат 60x90 1/16. Усл.печл. 1,25. Тираж 100 экз. Заказ 622. Тел. 939-3890. Тел./факс 939-3891. 119992, ГСП-2, Москва, Ленинские горы, МГУ им. М.В. Ломоносова, 2-й учебный корпус, 627 к.

Введение

1 Алгоритмы антиунификации подстановок

1.1 Подстановки и их представление.

1.1.1 Подстановки, решетка подстановок.

1.1.2 Графовые представления подстановок.

1.2 Сложность задачи антиунификации в классе последовательных алгоритмов

1.2.1 Алгоритм редукции.

1.2.2 Алгоритм антиунификации для подстановок, представленных ациклическими ориентированными графами.

1.2.3 Нижняя оценка сложности задачи антиунификации подстановок

1.3 Параллельные алгоритмы

1.3.1 Алгоритм распознавания точного антиунификатора.

1.3.2 Алгоритм построения точного антиунификатора.

1.4 Вычисление инвариантов равенства программ с использованием антиунификации подстановок.

1.4.1 Модель одномодульной программы.

1.4.2 Инварианты равенства одномодульных программ и методы их вычисления.

2 Обобщенные подстановки

2.1 Метаконтексты и метаподстановки

2.1.1 Понятия контекста и метаконтекста.

2.1.2 Решетка метаконтекстов

2.1.3 Метаподстановки и их основные алгебраические свойства

2.1.4 Операция конкретизации метаподстановок.

2.2 Антиунификация для метаподстановок.

2.2.1 Представление метаконтекстов конечными автоматами

2.2.2 Алгоритм антиунификации метаконтекстов.

3 Инварианты многомодульных программ

3.1 Многомодульные программы и инварианты равенства.

3.1.1 Модель многомодульной программы.

3.1.2 Инварианты равенства программ и их представление мета-подстановками

3.1.3 Аппроксимирующие последовательности.

3.2 Вычисление инвариантов равенства программ при помощи метаподстановок

3.2.1 Построение аппроксимирующей последовательности.

3.2.2 Алгоритм построения инвариантов равенства.

Задача антиунификации (англ. anti-unification, generalization) была впервые рассмотрена в работах [18] и [20]. В общем виде она состоит в том, чтобы для двух заданных выражений Е\ и Е2 отыскать наиболее специальное выражение Е0, примерами которого являются оба выражения и Е2, то есть существуют подстановки и д2. для которых выполняются равенства Е\ = Е0д\ и Е2 = Ео$2- Такое выражение Е0 называется наименее общим шаблоном выражений Е\ и Е2.

Задача антиунификации двойственна гораздо более широко исследованной задаче унификации. Последняя состоит в том, чтобы для двух заданных выражении Е\ и Е2 отыскать наиболее общее выражение Е0, которое является примером обоих выражений Е\ и Е2, то есть удовлетворяет равенствам Е0 = Е\щ и Е0 — Е2ц2 для некоторых подстановок щ и г/2. Такое выражение Eq называется наиболее общим примером выражений и Е2. Задача унификации была впервые исследована Дж. Робинсоном [21] в 1965 году в связи с созданием метода резолюций для автоматического доказательства теорем. В дальнейшем метод резолюций послужил отправной точкой для разработки концепции логического программирования, и алгоритмы унификации фактически стали основным средством вычисления логических программ. За прошедшие годы задача унификации была детально исследована. В частности, был разработан широкий спектр эффективных алгоритмов унификации [2, 12, 17, 27, 28], имеющих почти линейную сложность, а также были найдены подходящие структуры данных для практической реализации этих алгоритмов. Одной из таких структур для представления подстановок являются ациклические ориентирование графы, получаемые из деревьев «склеиванием» изоморфных поддеревьев. Важным частным случаем задачи унификации является задача метчипга (от англ. matching - приведение в соответствие). Она состоит в том, чтобы для двух заданных выражений Е0 и Ei отыскать подстановку ?/, удовлетворяющую равенству Ех = Е0г).

Задача антиунификации (построения наименее общих шаблонов) рассматривалась в ряде работ [5, 10, 11, 14, 15, 18, 20, 22, 24, 25, 36]. В этих работах были предложены различные алгоритмы антиунификации, и в некоторых случаях была исследована сложность этой задачи. Так, например, в статье [10] было установлено, что задача антиунификации для термов, представленных в виде деревьев, являтся JVC-полной (в отличие от задачи унификации, которая относится к числу Р-полных задач). В статье [5] были предложены параллельные алгоритмы антиунификации для термов, представленных в виде деревьев. Было показано, что антиунификацию термов, представленных деревьями размера N, можно провести за время О (log2 А'") с использованием TV/log2 N процессоров в модели параллельных вычислений EREW PRAM, не допускающей одновременное считывание и запись данных несколькими процессорами в одну и ту же ячейку памяти. В этой же работе было показано, что в том случае, когда нескольким процессорам разрешается одновременно проводить операции считывания и записи, относящиеся к одной и той же ячейке общей памяти (модель параллельных вычислений CRCW PRAM), антиунификацию древесных термов можно провести за время О (log N) с использованием N/ log Аг процессоров. Однако сложность задачи антиунификации для термов, для представления которых используются структуры данных, отличные от деревьев, ранее не исследовалась.

Цель главы 1 этой работы - выяснить, какова сложность задачи антиунификации в том случае, когда рассматриваемые термы представлены ациклическими ориентированными графами. Задача антиунификации термов эквивалентна задаче антиунификации подстановок. Под подстановкой в данном случае понимается отображение из одного множества переменных в множество термов, построенное над конечным множеством функциональных символов и другим множеством переменных. В параграфе 1.2.2 представлен последовательный алгоритм антиунификации подстановок, сложность которого линейно зависит от размера вычисляемого им наименее общего шаблона. Таким образом, устанавливается, что при измерении сложности алгоритмов относительно размеров исходных данных и вычисляемого результата задача антиунификации имеет почти такую же сложность, что и задача унификации, независимо от формы представления термов. В параграфе 1.2.3 дается нижняя оценка сложности задачи антиунификации для подстановок, представленных ациклическими ориентированными графами. Для этого представлен пример последовательности пар подстановок, размер наименее общих шаблонов которых квадратично зависит от размеров исходных подстановок. Полученный результат подчеркивает существенное комбинаторное отличие задачи антиунификации от задачи унификации. Известно, что размер наиболее общего примера двух выражений может экспоненциально зависеть от размеров самих выражений, если эти выражения представлены в виде деревьев. Однако в том случае, если для представления выражений использовать ациклические ориентированные графы, то размер наиболее общего примера будет ограничен величиной, линейно зависящей от размеров исходных выражений. Для задачи антиунификации все происходит наоборот: если выражения представлены в виде деревьев, то размер наименее общего шаблона двух выражений не превосходит размеров самих исходных выражений, а если для представления выражений использовать ациклические ориентированные графы (более «компактную» структуру данных), то размер наименее общего шаблона может квадратично зависеть от размеров исходных выражений. Таким образом, сложность алгоритмов антиунификации существенно зависит от способа представления исходных данных.

В разделе 1.3 рассмотрены параллельные алгоритмы антиунификации подстановок, представленных ациклическими ориентированными графами. Первый из них - предложенный в параграфе 1.3.1 алгоритм распознавания точного антиунификатора - проверяет, является ли заданная подстановка г] точной нижней гранью двух других заданных подстановок и Затем на основании этого алгоритма показывается, что задача распознавания точного антиунификатора для подстановок, представленных в виде ациклических ориентированных графов, принадлежит классу сложности N0. Однако применять этот алгоритм для вычисления точной нижней грани подстановок невозможно. В параграфе 1.3.2 рассмотрен второй из алгоритмов - параллельный алгоритм построения ациклического ориентированного графа, представляющего точную нижнюю грань двух подстановок, - и оценена его сложность.

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

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

3у13у2 ■ • • 3ук(ъх = ¿1 Л г>2 = ¿2 А • ■ • Л Ут = ¿т), где ¿1, /2,., ~ некоторые термы. Основное внимание уделено построению для произвольной точки программы наиболее специального сильного инварианта в классе инвариантов равенства, то есть такой формулы, из которой в свободных эрбрановских) интерпретациях логически следуют все инварианты равенства в этой точке.

Методы вычисления инвариантов равенства существенно зависят от модели исследуемой программы. В разделе 1.4 разработан метод вычисления инвариантов равенства одномодульных программ, то есть программ, множество операторов которых не содержит вызовов процедур. В этом случае вычисление инварианта равенства естественным образом сводится к исследованной в разделах 1.2 и 1.3 задаче антиунификации подстановок, то есть к задаче вычисления точной нижней грани в решетке подстановок. Важным свойством подстановок, позволяющим использовать антиунификацию для вычисления инвариантов равенства, является выполнимость закона левой дистрибутивности композиции подстановок относительно операции антиунификации. Это свойство позволяет применять быстрые итеративные алгоритмы вычисления неподвижных точек, широко используемые при решении задач статического анализа и верификации моделей программ (см., например, [13]).

Помимо задачи вычисления инвариантов, проблема антиунификации подстановок возникает и при решении некоторых других задач анализа программ. Так, например, полиномиальный алгоритм проверки логико-термальной эквивалентности программ, предложенный В.К. Сабельфельдом [35], фактически проводит вычисление и сравнение наименее общих шаблонов термов, которые сопоставляются в качестве значений переменным анализируемых программ. В работе [3] антиунификация термов использовалась для поиска «клонов» в тексте программы, то есть фрагментов, которые могут быть получены друг из друга заменой некоторых подфрагментов. В помощью антиунификации все операторы исследуемой программы делятся на кластеры, в результате чего программу можно рассматривать как последовательность идентификаторов таких кластеров. После этого снова при помощи антиунификации в этой последовательности выделяются «похожие» подпоследовательности. В работе [14] антиунификация использовалась для выявления широкораспространенных шаблонов формул, используемых в научных статьях. В работе [22] предложен метод суперкомпиляции функциональных программ, в котором также используется антиунификация подстановок.

Как уже говорилось выше, благодаря выполнимости закона левой дистрибутивности композиции подстановок относительно операции взятия точной нижней грани, задача вычисления наиболее специальных инвариантов равенства в произвольной точке одномодульной программы может быть решена при помощи итеративной процедуры вычисления точных нижних граней в решетке подстановок (вычисления антиунификаторов подстановок). К сожалению, подобный подход к вычислению наиболее специальных инвариантов равенства сталкивается со значительными трудностями в том случае, когда программа состоит из нескольких модулей (процедур) и содержит операторы вызова этих модулей. Это связано с тем, что в решетке подстановок не выполняется закон правой дистрибутивности композиции подстановок относительно операции взятия точной нижней грани. Поэтому формула, полученная в результате последовательной подстановки друг в друга наиболее специальных инвариантов равенства, вычисленных отдельно для каждого из модулей, будет инвариантом равенства, но этот инвариант, вообще говоря, не будет являться наиболее специальным. В главе 2 предложено обобщающее концепцию подстановки понятие регулярной метпаподстановки, для которого выполняется закон правой дистрибутивности композиции относительно операции взятия точной нижней грани (операции антиунификации метаподстановок). Выполнимость этого закона, наряду с другими свойствами, позволяет использовать алгоритмы антиунификации метаподстановок для вычисления наиболее специальных линейных инвариантов равенства многомодульных программ. Термин «мета-подстановка» был выбран для обозначения введенного нами понятия потому, что оно естественным образом обобщает понятие подстановки. Его не следует путать с понятием «те[,азчЬзпЬи(лоп», используемым в теории переписывания для обозначения подстановок высшего порядка (см. например, [6]).

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

Множество контекстов К называется линейным по некоторому заданному мно-оюеетеу переменных, если любая переменная из этого множества встречается на листьях контекстов из К не более одного раза. Как уже говорилось выше, подстановка - это отображение из одного множества переменных VI в множество термов, построенных над множеством функциональных символов и другим множеством переменных V'2. Для вычисления инвариантов равенства многомодульных программ необходимо разделить множество переменных ТЛ на два непересекающихся подмножества - конечное множество 2 переменных входа (формальных аргументов модуля) и бесконечное множество 3' вспомогательных переменных, соответствующих связанным переменным в инвариантах равенства. Мы будем рассматривать множества контекстов, линейные по множеству вспомогательных переменных У. С одной стороны, такое ограничение существенно сужает круг поиска инвариантов равенства. Полученный нашим методом инвариант равенства будет наиболее специальным не во всем множестве инвариантов равенства, а только в его подмножестве линейных инвариантов равенства. Однако в главе 3 показано, что отличие между ними будет только в переменных термов, встречающихся в инварианте, а не в структуре из функциональных символов этих термов. Это означает, что наиболее специальный инвариант равенства можно получить из наиболее специального линейного инварианта равенства отождествлением некоторых связанных переменных. С другой стороны, свойство линейности множества контекстов необходимо для выполнимости закона правой дистрибутивности композиции метаподстановок относительно операции взятия точной нижней грани.

Рассмотрим теперь свойство согласованности множества контекстов. При описании свойства линейности говорилось, что множество переменных Уо, над которыми строятся термы, встречающиеся в необходимых для вычисления инвариантов равенства мстаподстановках, разделяется на непересекающиеся множества переменных входа Е и вспомогательных переменных Множество функциональных символов Н, встречающихся в этих термах, также распадается на два непересекающихся подмножества - множество Т функциональных символов операций (арифметических и пр.), встречающихся в программе, и множество V процедурных символов, каждый из которых соответствует одному из модулей программы. При вычислении инвариантов равенства сначала строятся метаподстановки для каждого модуля в отдельности, а затем в метаподстановке, построенной для исследуемой точки программы, все процедурные символы итеративно заменяются на соответствующие метаподстановки. Несогласованность двух контекстов возникает в том случае, когда при наложении друг на друга соответствующих им ветвей из набора деревьев, представляющих подстановки, обнаруживается, что две соответствующие вершины этих ветвей либо помечены различными функциональными (непроцедурными) символами, либо вспомогательная переменная накладывается на любой отличный от нее символ. Множество контекстов называется согласованным, если все его элементы попарно согласованы. Выполнимость свойства согласованности позволяет использовать разработанную в разделе 3.1 главы 3 технику аппроксимирующих последовательностей для определения того момента, когда необходимая для вычисления наиболее специального линейного инварианта равенства многомодульной рекурсивной программы метаподстановка уже получена. Согласованное множество контекстов называется метаконтекстом. В параграфах 2.1.1 и 2.1.2 даны строгие определения контекста и метаконтекста, а также исследованы их основные свойства. В частности, показано, что для линейных ме-таконтекстов на основе композиции множеств контекстов определяется нижняя полурешетка. Операция вычисления точной нижней грани в этой решетке, называемая антиунификацией метаконтекстов, является основополагающей для вычисления инвариантов равенств.

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

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

Глава 3 посвящена разработке метода вычисления наиболее специальных линейных инвариантов равенства для программ с вызовами процедур. В параграфе 3.1.1 строго введена модель итеративной недетерминированной многомодульной программы. В такой программе содержатся операторы двух видов - операторы присваивания и операторы вызова процедуры. В параграфе 3.1.2 дано определение инварианта равенства многомодульной программы и рассмотрен метод сведения задачи построения наиболее специального инварианта равенства к задаче вычисления метаподстановки определенного вида. Параграф 3.1.3 посвящен исследованию свойств такой метаподстановки. В частности, показано, что ее можно получить итеративно методом аппроксимирующих последовательностей из ме-таподстановок, сопоставленных каждому модулю. В параграфе 3.2.1 говорится о том, что автоматные представления последних легко строятся непосредственно по модели программы с помощью метода поиска неподвижной точки. В параграфе 3.2.2 приведен алгоритм вычисления наиболее специальных линейных инвариантов равенства для программ с вызовами процедур.

Основные результаты этой работы таковы.

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

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

3. Предложена концепция метаподстановки, обобщающая понятие подстановки, и установлены основные алгебраические свойства метаподстановок.

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

Заключение

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

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

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

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

Таким образом, в диссертационной работе

1. разработаны новые последовательные и параллельные алгоритмы антиунификации подстановок;

2. получены новые, более точные оценки сложности задачи антиунифиикации подстановок;

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

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

1. Apt K.R., Olderog E.-R. Verification of Sequential and Concurrent Programs. Springer, 1997, 364 p.

2. Baxter L.D. An efficient unification algorithm. Technical Report CS-73-23, Dep. of Analysis and Comp. Sci., University of Waterloo, Ontario, Canada, 1973.

3. Bulychev P., Minea M. Duplicate code detection using anti-unification. Proceedings of the First Spring Young Researchers Colloquium on Software Engineering, 2008, pp. 51-54.

4. Coppersmith D., Winograd S. On the asymptotic complexity of matrix multiplication. SIAM J. Comput., v 11, 1982, pp. 472-492.

5. Delcher A.L., Kasif S. Efficient parallel term matching and anti-unification. Journal of Automated Reasoning, v. 9, N 3, 1992, pp. 391-406.

6. Dershowitz N., Jouannaud J.-P. Handbook of Theoretical Computer Science, v. B: Models and Sematics, chapter 6: Rewrite Systems, 1990, pp. 243-320.

7. Dwork C., Kanellakis P.C., and Mitchel D.C. On the Sequental Nature of Unification. Journal of Logic Programming, v. 1, 1984, pp. 35-50.

8. Dwork C., Kanellakis P.C., and Stockmeyer L. Parallel Algorithms for Term Matching. SIAM J. Comput., v. 17, n. 4, 1988, pp. 711-731.

9. Eder E. Properties of substitutions and unifications. Journal of Symbolic Computations, v. 1, 1985, pp. 31-46.

10. Kuper G. M., McAloon K. W., Palem K. V., Perry K. J. A note on the parallel complexity of anti-unification. Journal of Automated Reasoning, v. 9, N 3, 1992, pp. 381-389.

11. Lassez J.I., Maher M.J., Marriot K. Unification revisited. In Foundations of Deductive Databases and Logic Programming, ed. J. Minker, Morgan Kaufmann, Los Altos, 1988.

12. Martelli A., Montanari U. An efficient unification algorithm. ACM Transactions on Program, Languages and Systems, v. 4, N 2, 1982, pp. 258-282.

13. Nielson F., Nielson H.R., Hankin C. Principles of Program Analysis. Springer, 1999, 446 p.

14. Oancea C.E., So C., Watt S.M. Generalization in Maple, Maple Conference, 2005, pp. 277-382.

15. Palamidessi C. Algebraic properties of idempotent substitutions. Lecture Notes in Computer Science, v. 443, 1990, pp. 386-399.

16. Pan V., Reif J. Efficient parallel solutions of linear systems. Proc. 17th Annual ACM Symposium on Theory of Computing, 1985, pp.143-152.

17. Paterson M.S., Wegman M.N. Linear unification. The Journal of Computer and System Science, v. 16, N 2, 1978, pp. 158-167.

18. Plotkin G.D. A note on inductive generalization. Machine Intelligence, 1970, v. 5, N 1, 1970, pp. 153-163.

19. Rabin M.O., Scott D. Finite automata and their decision problems. IBM J. Research and Development, v. 3, N 2, 1959, pp. 115-125.

20. Reynolds J.С. Transformational systems and the algebraic structure of atomic formulas. Machine Intelligence, v.5, N 1, 1970, pp. 135—151.

21. Robinson J.A. A machine-oriented logic based on the resolution princple. Journal of the ACM, v. 12, N 1, 1965, pp. 23-41.

22. Sorensen M.H., Gluck. R. An algorithm of generalization in positive supercompilation, Logic Programming: Proceedings of the 1995 International Symposium, MIT Press, 1995, pp. 465-479.

23. Tarjan R.E., Vishkin U. An Efficient Parallel Biconnectivity Algorithm. SIAM J. Comput., v. 14, n. 4, 1985, pp. 862-874.

24. Watt S.M. Algebraic generalization. ACM SIGSAM Bulletin, v. 39, N 3, 2005, pp. 93-94.

25. Zakharov V.A. On the refinement of logic programs by means of anti-unification. Proceedings of the 2-nd Panhellenic Logic Symposium, Delphi, Greece, 1999, pp. 219-224.

26. Ахо А., Ульман Д. Теория синтаксического анализа, перевода и компиляции. Москва, Мир, 1978.

27. Годлевский А.В., Кривой C.JI. О проектировании эффективных алгоритмов приведения автоматов для некоторых отношений эквивалентности. Кибернетика, N 6, 1989, с. 54-61.

28. Дегтярев А.И. Об использовании аксиом функциональной рефлексивности в (Р & R) процедуре опровержения. Препринт Ин-та Кибернетики АН УССР, N 75-28, 1975, 28 с.

29. Кнут Д. Искусство программирования, том 3. Сортировка и поиск. Москва, Мир, 1977.

30. Костылев Е.В., Захаров В.А. Об одном обобщении подстановок применительно к задаче синтеза инвариантов программ. Материалы VIII-го Международного семинара «Дискретная Математика и ее приложения», Москва, 2004, с.134-136.

31. Костылев Е.В. Методы вычисления инвариантов программ. Труды всероссийской конференции студентов, аспирантов и молодых ученых «Технологии Microsoft в теории и практике программирования», Москва, 2005, с.130.

32. Костылев Е.В. О вычислении инвариантов программ. Тезисы докладов XIV международной конференции «Проблемы теоретической кибернетики», Москва, 2005, с.73.

33. Костылев Е.В., Захаров В.А. Об одном обобщении подстановки применительно к задаче статического анализа программ. Вестник Московского Университета, 2005, сер.15, Вычислительная Математика и Кибернетика, №4, с.39-45.

34. Костылев Е.В., Захаров В.А. О сложности задачи антиунификации. Дискретная математика, 2008, т.20, вып.1, с.131-144.

35. Сабельфельд В.К. Полиномиальная оценка сложности распознавания логико-термальной эквивалентности. Доклады АН СССР, 1979, т. 249, N 4, с. 793-796.

36. Захаров В.А., Костылев Е.В. Быстрые алгоритмы антиунификации и их применение при анализе программ. Материалы XIII-й Международной школы-семинара «Синтез и сложность управляющих систем», Пенза, 2002, Часть 1, с. 76-81.