Содержание к диссертации
Введение
1 Алгоритмы антиунификации подстановок 14
1.1 Подстановки и их представление 14
1.1.1 Подстановки, решетка подстановок 15
1.1.2 Графовые представления подстановок 18
1.2 Слолсность задачи антиунификации в классе последовательных ал горитмов 20
1.2.1 Алгоритм редукции 20
1.2.2 Алгоритм антиунификации для подстановок, представленных ациклическими ориентированными графами 23
1.2.3 Нижняя оценка сложности задачи антиунификации подстановок 28
1.3 Параллельные алгоритмы 32
1.3.1 Алгоритм распознавания точного антиунификатора 32
1.3.2 Алгоритм построения точного антиунификатора 41
1.4 Вычисление инвариантов равенства программ с использованием ан тиунификации подстановок 46
1.4.1 Модель одномодульной программы 46
1.4.2 Инварианты равенства одномодульных программ и методы их вычисления 50
2 Обобщенные подстановки 56
2.1 Метаконтексты и метаподстановки 57
2.1.1 Понятия контекста и метаконтекста 57
2.1.2 Решетка метаконтекстов 64
2.1.3 Метаподстановки и их основные алгебраические свойства . 83
2.1.4 Операция конкретизации метаподстановок 105
2.2 Антиунификация для метаподстановок 121
2.2.1 Представление метаконтекстов конечными автоматами . 121
2.2.2 Алгоритм антиунификации метаконтекстов 129
3 Инварианты многомодульных программ 141
3.1 Многомодульные программы и инварианты равенства 142
3.1.1 Модель многомодульной программы 142
3.1.2 Инварианты равенства программ и их представление мета-подстановками 148
3.1.3 Аппроксимирующие последовательности 155
3.2 Вычисление инвариантов равенства программ при помощи метапод становок 164
3.2.1 Построение аппроксимирующей последовательности 164
3.2.2 Алгоритм построения инвариантов равенства 167
Заключение 170
Литература 173
Приложение 177
- Подстановки, решетка подстановок
- Алгоритм распознавания точного антиунификатора
- Понятия контекста и метаконтекста
- Инварианты равенства программ и их представление мета-подстановками
Введение к работе
Задача антиунификации (англ. anti-unification, generalization) была впервые рассмотрена в работах [18] и [20]. В общем виде она состоит в том, чтобы для двух заданных выражений Е\ и і22 отыскать наиболее специальное выражение Е0, примерами которого являются оба выражения Е\ и _Е2, то есть существуют подстановки #! и і92, Для которых выполняются равенства Е\ = Е0д\ и 1 = -ЕЬ^2- Такое выражение Eq называется наименее общим шаблоном выражений Е\ и Е2.
Задача антиунификации двойственна гораздо более широко исследованной задаче унификации. Последняя состоит в том, чтобы для двух заданных выражении Е\ и Е2 отыскать наиболее общее выражение Е0, которое является примером обоих выражений Ei а Ео, то есть удовлетворяет равенствам Eq = Ехщ и Е0 — .% для некоторых подстановок 171 и Ш- Такое выражение Eq называется наиболее общим примером выражений Ei и Еч- Задача унификации была впервые исследована Дж. Робинсоном [21] в 1965 году в связи с созданием метода резолюций для автоматического доказательства теорем. В дальнейшем метод резолюций послужил отправной точкой для разработки концепции логического программирования, и алгоритмы унификации фактически стали основным средством вычисления логических программ. За прошедшие годы задача унификации была детально исследована. В частности, был разработан широкий спектр эффективных алгоритмов унификации [2, 12, 17, 27, 28], имеющих почти линейную сложность, а также были найдены подходящие структуры данных для практической реализации этих алгоритмов. Одной из таких структур для представления подстановок являют-
ВВЕДЕНИЕ
ся ациклические ориентированы^ графы, получаемые из деревьев «склеиванием» изоморфных поддеревьев. Важным частным случаем задачи унификации является задача метчинга (от англ. matching- приведение в соответствие). Она состоит в том, чтобы для двух заданных выражений Е0 и Е]_ отыскать подстановку ?;, удовлетворяющую равенству Е\ — Е0г).
Задача антиунификации (построения наименее общих шаблонов) рассматривалась в ряде работ [5, 10, 11, 14, 15, 18, 20, 22, 24, 25, 36]. В этих работах были предложены различные алгоритмы антиунификации, и в некоторых случаях была исследована сложность этой задачи. Так, например, в статье [10] было установлено, что задача антиунификации для термов, представленных в виде деревьев, являтся JVC-полной (в отличие от задачи унификации, которая относится к числу Р-полных задач). В статье [5] были предложены параллельные алгоритмы антиунификации для термов, представленных в виде деревьев. Было показано, что антиунификацию термов, представленных деревьями размера N, можно провести за время О (log2 N) с использованием TV/log2 N процессоров в модели параллельных вычислений EREW PRAM, не допускающей одновременное считывание и запись данных несколькими процессорами в одну и ту же ячейку памяти. В этой же работе было показано, что в том случае, когда нескольким процессорам разрешается одновременно проводить операции считывания и записи, относящиеся к одной и той же ячейке общей памяти (модель параллельных вычислений CRCW PRAM), антиунификацию древесных термов можно провести за время 0(\ogN) с использованием N/\ogAr процессоров. Однако сложность задачи антиунификации для термов, для представления которых используются структуры данных, отличные от деревьев, ранее не исследовалась.
Цель главы 1 этой работы - выяснить, какова сложность задачи антиунификации в том случае, когда рассматриваемые термы представлены ациклическими ориентированными графами. Задача антиунификации термов эквивалентна задаче антиунификации подстановок. Под подстановкой в данном случае понимается
ВВЕДЕНИЕ
отображение из одного множества переменных в множество термов, построенное над конечным множеством функциональных символов и другим множеством переменных. В параграфе 1.2.2 представлен последовательный алгоритм антиунификации подстановок, сложность которого линейно зависит от размера вычисляемого им наименее общего шаблона. Таким образом, устанавливается, что при измерении сложности алгоритмов относительно размеров исходных данных и вычисляемого результата задача антиунификации имеет почти такую же сложность, что и задача унификации, независимо от формы представления термов. В параграфе 1.2.3 дается нижняя оценка сложности задачи антиунификации для подстановок, представленных ациклическими ориентированными графами. Для этого представлен пример последовательности пар подстановок, размер наименее общих шаблонов которых квадратично зависит от размеров исходных подстановок. Полученный результат подчеркивает существенное комбинаторное отличие задачи антиунификации от задачи унификации. Известно, что размер наиболее общего примера двух выражений может экспоненциально зависеть от размеров самих выражений, если эти выражения представлены в виде деревьев. Однако в том случае, если для представления выражений использовать ациклические ориентированные графы, то размер наиболее общего примера будет ограничен величиной, линейно зависящей от размеров исходных выражений. Для задачи антиунификации все происходит наоборот: если выражения представлены в виде деревьев, то размер наименее общего шаблона двух выражений не превосходит размеров самих исходных выражений, а если для представления выражений использовать ациклические ориентированные графы (более «компактную» структуру данных), то размер наименее общего шаблона может квадратично зависеть от размеров исходных выражений. Таким образом, сложность алгоритмов антиунификации существенно зависит от способа представления исходных данных.
В разделе 1.3 рассмотрены параллельные алгоритмы антиунификации подстановок, представленных ациклическими ориентированными графами. Первый из
ВВЕДЕНИЕ
них - предложенный в параграфе 1.3.1 алгоритм распознавания точного антиунификатора - проверяет, является ли заданная подстановка г\ точной нижней гранью двух других заданных подстановок -&i и д2. Затем на основании этого алгоритма показывается, что задача распознавания точного антиунификатора для подстановок, представленных в виде ациклических ориентированных графов, принадлежит классу сложности NC. Однако применять этот алгоритм для вычисления точной нижней грани подстановок невозможно. В параграфе 1.3.2 рассмотрен второй из алгоритмов - параллельный алгоритм построения ациклического ориентированного графа, представляющего точную нижнюю грань двух подстановок, - и оценена его сложность.
Одной из основных задач статического анализа программ является задача вычисления инвариантов, то есть отношений между данными, которые выполняются для любых вычислений программы. Знание инвариантов необходимо для решения практических задач верификации, оптимизации, синтеза и реорганизации (рефакторинга) программ [1]. В то лее время, в одной и той же точке программы существует бесконечно много инвариантов различного вида. В частности, любая тождественно истинная формула может выступать в роли инварианта. Известно также, что в универсальных моделях вычислений задача проверки того, что заданная формула является инвариантом заданной программы, алгоритмически неразрешима. Поэтому в каждом конкретном исследовании, посвященном вычислению инвариантов, разумно ограничиться поиском инвариантов специального вида.
В этой работе исследуется задача вычисления инвариантов равенства, то есть инвариантов, которые представимы формулой логики предикатов первого порядка вида
Зу13у2 ... 3yk(vx = t1Av2 = t2A...Avm = tm),
где ti, /2,..., tm - некоторые термы. Основное внимание уделено построению для произвольной точки программы наиболее специального сильного инварианта в классе инвариантов равенства, то есть такой формулы, из которой в свободных
ВВЕДЕНИЕ
(эрбрановских) интерпретациях логически следуют все инварианты равенства в этой точке.
Методы вычисления инвариантов равенства существенно зависят от модели исследуемой программы. В разделе 1.4 разработан метод вычисления инвариантов равенства одномодульных программ, то есть программ, множество операторов которых не содержит вызовов процедур. В этом случае вычисление инварианта равенства естественным образом сводится к исследованной в разделах 1.2 и 1.3 задаче антиунификации подстановок, то есть к задаче вычисления точной нижней грани в решетке подстановок. Важным свойством подстановок, позволяющим использовать антиунификацию для вычисления инвариантов равенства, является выполнимость закона левой дистрибутивности композиции подстановок относительно операции антиунификации. Это свойство позволяет применять быстрые итеративные алгоритмы вычисления неподвижных точек, широко используемые при решении задач статического анализа и верификации моделей программ (см., например, [13]).
Помимо задачи вычисления инвариантов, проблема антиунификации подстановок возникает и при решении некоторых других задач анализа программ. Так, например, полиномиальный алгоритм проверки логико-термальной эквивалентности программ, предложенный В.К. Сабельфельдом [35], фактически проводит вычисление и сравнение наименее общих шаблонов термов, которые сопоставляются в качестве значений переменным анализируемых программ. В работе [3] антиунификация термов использовалась для поиска «клонов» в тексте программы, то есть фрагментов, которые могут быть получены друг из друга заменой некоторых подфрагментов. В помощью антиунификации все операторы исследуемой программы делятся на кластеры, в результате чего программу можно рассматривать как последовательность идентификаторов таких кластеров. После этого снова при помощи антиунификации в этой последовательности выделяются «похожие» подпоследовательности. В работе [14] антиунификация использовалась для вы-
ВВЕДЕНИЕ
явления широкораспространенных шаблонов формул, используемых в научных статьях. В работе [22] предложен метод суперкомпиляции функциональных программ, в котором также используется антиунификация подстановок.
Как уже говорилось выше, благодаря выполнимости закона левой дистрибутивности композиции подстановок относительно операции взятия точной нижней грани, задача вычисления наиболее специальных инвариантов равенства в произвольной точке одномодульной программы может быть решена при помощи итеративной процедуры вычисления точных нижних граней в решетке подстановок (вычисления антиунификаторов подстановок). К сожалению, подобный подход к вычислению наиболее специальных инвариантов равенства сталкивается со значительными трудностями в том случае, когда программа состоит из нескольких модулей (процедур) и содержит операторы вызова этих модулей. Это связано с тем, что в решетке подстановок не выполняется закон правой дистрибутивности композиции подстановок относительно операции взятия точной нижней грани. Поэтому формула, полученная в результате последовательной подстановки друг в друга наиболее специальных инвариантов равенства, вычисленных отдельно для каждого из модулей, будет инвариантом равенства, но этот инвариант, вообще говоря, не будет являться наиболее специальным. В главе 2 предложено обобщающее концепцию подстановки понятие регулярной метаподстановки, для которого выполняется закон правой дистрибутивности композиции относительно операции взятия точной нижней грани (операции антиунификации метаподстановок). Выполнимость этого закона, наряду с другими свойствами, позволяет исполіьзовать алгоритмы антиунификации метаподстановок для вычисления наиболее специальных линейных инвариантов равенства многомодульных программ. Термин «мета-подстановка» был выбран для обозначения введенного нами понятия потому, что оно естественным образом обобщает понятие подстановки. Его не следует путать с понятием «metasubstitution», используемым в теории переписывания для обозначения подстановок высшего порядка (см. например, [6]).
ВВЕДЕНИЕ
Базовым понятием, необходимым для определения метаподстановки, является понятие контекста. Как уже говорилось выше, любую подстановку можно представить в виде набора помеченных корневых ориентированных упорядоченных деревьев. Тогда контекстом будет любая ветвь в одном из деревьев этого набора, то есть цепь, начинающаяся корнем и заканчивающаяся любым из листьев. Регулярной метаподстановкой будем называть любое (конечное или бесконечное) множество контекстов, удовлетворяющее свойствам линейности, согласованности, полноты и регулярности. Остановимся подробнее на каждом из этих свойств, уделяя особое внимание той роли, которую они играют для решения задачи вычисления инвариантов равенства.
Множество контекстов А' называется линейным по некоторому заданному мно-otcecmey переменных, если любая переменная из этого множества встречается на листьях контекстов из К не более одного раза. Как уже говорилось выше, подстановка - это отображение из одного множества переменных Vi в множество термов, построенных над множеством функциональных символов и другим множеством переменных Vi. Для вычисления инвариантов равенства многомодульных программ необходимо разделить множество переменных V-2. на два непересекающихся подмножесгва - конечное множество Z переменных входа (формальных аргументов модуля) и бесконечное множество У вспомогательных переменных, соответствующих связанным переменным в инвариантах равенства. Мы будем рассматривать множества контекстов, линейные по множеству вспомогательных переменных У. С одной стороны, такое ограничение существенно сужает круг поиска инвариантов равенства. Полученный нашим методом инвариант равенства будет наиболее специальным не во всем множестве инвариантов равенства, а только в его подмножестве линейных инвариантов равенства. Однако в главе 3 показано, что отличие между ними будет только в переменных термов, встречающихся в инварианте, а не в структуре из функциональных символов этих термов. Это означает, что наиболее специальный инвариант равенства можно получить из наиболее специального
ВВЕДЕНИЕ
линейного инварианта равенства отождествлением некоторых связанных переменных. С другой стороны, свойство линейности множества контекстов необходимо для выполнимости закона правой дистрибутивности композиции метаподстановок относительно операции взятия точной нижней грани.
Рассмотрим теперь свойство согласованности множества контекстов. При описании свойства линейности говорилось, что множество переменных ~\?2, над которыми строятся термы, встречающиеся в необходимых для вычисления инвариантов равенства мстаподстановках, разделяется на непересекающиеся множества переменных входа Z и вспомогательных переменных 3^- Множество функциональных символов Н, встречающихся в этих термах, также распадается на два непересекающихся подмножества - множество Т функциональных символов операций (арифметических и пр.), встречающихся в программе, и множество V процедурных символов, каждый из которых соответствует одному из модулей программы. При вычислении инвариантов равенства сначала строятся метаподстановки для каждого модуля в отдельности, а затем в метаподстановке, построенной для исследуемой точки программы, все процедурные символы итеративно заменяются на соответствующие метаподстановки. Несогласованность двух контекстов возникает в том случае, когда при наложении друг на друга соответствующих им ветвей из набора деревьев, представляющих подстановки, обнаруживается, что две соответствующие вершины этих ветвей либо помечены различными функциональными (непроцедурными) символами, либо вспомогательная переменная накладывается на любой отличный от нее символ. Множество контекстов называется согласованным, если все его элементы попарно согласованы. Выполнимость свойства согласованности позволяет использовать разработанную в разделе 3.1 главы 3 технику аппроксимирующих последовательностей для определения того момента, когда необходимая для вычисления наиболее специального линейного инварианта равенства многомодульной рекурсивной программы метаподстановка уже получена. Согласованное множество контекстов называется метаконтекстом. В пара-
ВВЕДЕНИЕ
графах 2.1.1 и 2.1.2 даны строгие определения контекста и метаконтекста, а также исследованы их основные свойства. В частности, показано, что для линейных метакоптекстов на основе композиции множеств контекстов определяется нижняя полурешетка. Операция вычисления точной нижней грани в этой решетке, называемая антиунификацией метакоптекстов, является основополагающей для вычисления инвариантов равенств.
Перейдем к рассмотрению свойства полноты множества контекстов. Как уже отмечалось выше, контекст представляет ветвь одного из набора деревьев, соответствующего некоторой подстановке. Полным называется множество контекстов, которые представляют все ветви множества наборов деревьев, задающих непустое множество подстановок. Полный линейный метаконтекст называется метаподста-новкой. Выполнимость свойства полноты позволяет сопоставить любой метапод-становке некоторое множество подстановок. Полученная при вычислении наиболее специального линейного инварианта равенства мстаподстановка содержит в этом множестве всего одну подстановку (то есть является конечной минимальной). Этой подстановке естественным образом сопоставляется формула, которая и является искомым инвариантом. Помимо этого, свойство полноты необходимо для выполнения ряда алгебраических законов в множестве метаподстановок, таких как закон правой дистрибутивности композиции относительно операции взятия точной нижней грани и закон ассоциативности композиции. Строгое определение метаподстановки наряду с доказательствами основных свойств представлено в параграфе 2.1.3.
Перейдем теперь к описанию свойства регулярности метаподстановок. В отличие от подстановок, любая из которых является конечной структурой, метаподстановки могут содержать бесконечное множество контекстов. Это обстоятельство оказывается полезным для того, чтобы при локальном вычислении метаподстановки для каждого модуля программы учитывать информацию о связи между данными по всем трассам этого модуля, начинающимся в входной точке и заканчи-
ВВЕДЕНИЕ
вающихся интересующей нас точкой. Произвольного вида множество контекстов очевидно невозможно представить какой-либо конечной структурой данных. Поэтому необходимо наложить еще одно ограничение на метаподстановки, которое, с одной стороны, все еще позволяет использовать их для вычисления инвариантов равенства, и, с другой стороны, допускает конечное представление метаподстано-вок. Как говорилось выше, контекст задает ветвь в одном из деревьев набора, представляющего подстановку. PI это означает, что его можно представить в виде слова в алфавите из переменных, функциональных символов и номеров аргументов этих символов. Следовательно, каждому множеству контекстов можно сопоставить язык в таком алфавите. Метаподстановка называется регулярной, если сопоставленный ей язык является регулярным. И тогда каждую регулярную метаиодстановку можно представлять в виде конечного автомата, принимающего сопоставленный ей язык. Такое представление позволяет разрабатывать различные алгоритмы с использованием регулярных метаподстановок. В параграфе 2.2.1 дано строгое определение регулярной метаподстановки, и подробно рассмотрено ее автоматное представление. В параграфе 2.2.2 представлен алгоритм антиунификации, вычисляющий точную нижнюю грань регулярных метаподстановок, представленных конечными автоматами. Этот алгоритм широко используется для вычисления наиболее специального линейного инварианта равенства в произвольной точке многомодульной программы с рекурсивными вызовами процедур.
Подстановки, решетка подстановок
Рассмотрим конечное множество Т = {Д , ...,/т } функциональных символов фиксированных конечных валентностей щ,..., пт и произвольное множество переменных У; переменные из множества У будем называть вспомогательными. В множестве !F выделим множество С? всех функциональных символов нулевой валентности (констант). А їножество термов Тегт\У,!\ определяется традиционным образом. (1) Каждая переменная из множества 3 является термом. (2) Если /(") - функциональный символ из множества J7, a t-i,... ,tn - термы, то выражение f (ti,... ,tn) также является термом. Пусть задано еще одно множество множество переменных X, такое что множество Х\У конечно; переменные из множества X будем называть рабочими. Подстановкой называется любое отображение д:Х- Тегт[У,Р\. Если для -в множество Dorn(i}) = {х Є X і9(х) ф х} конечно, то подстановка д называется конечной. В дальнейшем мы будем называть подстановками конечные подстановки, а в тех случаях, когда речь будет идти о возможно бесконечных подстановках, специально указывать на это. Подстановки удобно представлять в виде списка связок в = {жх/і9(а:і),..., хп/д(хп)}, где {xi,... ,хп} = Dom(d). Для обозначения множества всех переменных из У, которые встречаются в термах $(xi),... ,$(хп), будем использовать запись Var(i8), а для обозначения множества подстановок с областью определения X и областью значений Тегт[У,Т\ -запись Subst\X,y,J?\. Результатом применения подстановки fi = {жі/$(жі),..., xn/-d(xn)} из множества Subst[X, У, F\ к терму t из мно- жества Тегт[Х, Т\ называется терм М, который получается одновременной заменой в t всех переменных ХІ, 1 і 71, на соответствующие термы "д(хі),1 і п. Композицией подстановок $ Є Svbst[X, У, Т\ и Є Subst[y,У , J-] называется подстановка т? из множества Subst\X,y,J \ определенная для каждой переменной х, х є X, следующим образом:
Подстановка = {yi/ti,... ,Vk/tk} из множества iS bsip , X- "І называется идсм-потентпой, если выполняется равенство = . В этом случае можно представить в виде композиции отдельных связок = {уі/і} - . {ук/tk}- Подстановка р из множества Subst[y, У, .F], которая является биекцией из множества 3 в это же множество У, называется 7іереименованием. На множестве подстановок Subst[X,ytf] определяется бинарное отношение предпорядка С: для любых подстановок -ві и #2 из множества LJM&S , [V, ?""] отношение tJiEi52 выполняется тогда и только тогда, когда существует подстановка из множества S"«6si[y, J7, J7}, такая, что верно равенство г92 = $i. Это отношение предпорядка порождает на множестве подстановок Subst[X,y, J7] отношение эквивалентности : для любых подстановок $j и $2 из множества Subst[X,У,Т] отношение верно тогда и только тогда, когда выполняются неравенства Произвольные подстановки і?і и $2 эквивалентны в том и только том случае, если существует переименование р, для которого верно равенство А = &1Р. Рассмотрим новый, не принадлежащий множеству Subst[X\У , J7], элемент Т, который также будем считать подстановкой. Расширим отношение С на множество Subs lX , ] = Subst[X,y, Т\ U {Т} следующим образом: для каждой подстановки 9 из Subst[X, У, J7] положим & С Т. Отношение предпорядка С индуцирует на фактор-множестве Subst [X, У,Т] = Substr [X ,У, Т\ / отношение частичного порядка . Частично упорядоченное множество (Subst [X, У, Т\, =) было исследовано в работах [9, 11, 15]. Это множество образует полную решетку, наименьшим элементом которой является класс эквивалентности, порожденный так называемой пустой подстановкой є = {xi/yi,... ,хп/уп}, а наибольшим - класс, порожденный элементом Т. Обозначим символами j и f соответственно операции взятия точной нижней и точной верхней грани в этой решетке.
Операция f взятия точной верхней грани в решетке (Subst [X\У , J7], ) легко сводится к задаче вычисления наиболее общего унификатора термов. Операцию взятия точной нижней грани в этой решетке будем называть антиунификацией подстановок. Нетрудно убедиться (и это было отмечено в указанных работах), что выполняется закон левой дистрибутивности операции композиции относительно антиунификации, то есть для любой подстановки 7) из множества Svbst[X, Х,Т\ и произвольных подстановок t9i и 1 из множества SubstT [X ,У, J7] выполняется равенство Фі і #?) = Фі і V#? Кроме того, решетка (Subst [X,У,F], ) обладает тем свойством, что для любой подстановки $, д Ф Т, длина любой цепи между классами эквивалентности е и i9 конечна. Это свойство называется свойством обрыва убывающий цепей. В дальнейшем в тех случаях, когда это не приводит к путанице, будем называть подстановками их классы эквивалентности и опускать в записи индекс . Пусть заданы множество функциональных символов Т и множества рабочих и вспомогательных переменных X и У. Как известно, любой терм t из множества Term [У, Т\ можно представить в виде упорядоченного ориентированного помеченного дерева. Каждая вершина этого дерева взаимно однозначно соответствует некоторому вхождению подтерма t в терм I. При этом, вершина V, соответствующая какому-либо вхождению подтерма I — / (ii, ,tn) (или t = у), помечена символом / (или, соответственно, у); из вершины V исходит п упорядоченных дуг, которые ведут в вершины дерева Vi,...,Vn, соответствующие вхождениям подтермов ti,... ,tnB терм і . Таким образом, листья дерева будут помечены вспомогательными переменными из множества У и константами из множества Cj?.
Более «компактным» способом представления термов могут служить ациклические ориентированные графы (АОГ), в которых нескольким различным вхождениям одного и того же подтерма t = f (h,..., in) (или t — у) в терм t из множества Тегт[У,Т] сопоставляется одна и та же вершина, помеченная символом /(") (или у). Представляющий терм t АОГ можно получить, если в упорядоченном ориентированном дереве, представляющем t, «склеить» друг с другом изоморфные помеченные поддеревья. Вершины, являющиеся корнями изоморфных подграфов, назовем эквивалентными. Если в АОГ G(t), представляющем терм і, не существует различных эквивалентных вершин, то АОГ Q(t) назовем редуцированным. Для любого терма t из множества Тегт[У,Т] существует один и только один представляющий его редуцированный АОГ.
Алгоритм распознавания точного антиунификатора
В этом параграфе разработан алгоритм, работающий за полилогарифмическое время с использованием полиномиального количества процессоров и решающий задачу антиунификации для подстановок, представленных в виде АОГ. Тем самым показано, что эта задача также принадлежит классу NC, то есть ее можно решить за полилогарифмическос время с использованием полиномиального количества процессоров. Для произвольных натуральных чисел т и к обозначим символом NCfc(iVm) класс задач, которые можно решить за время 0(logfe N) с использованием 0(Nm) процессоров, где N - размер входных параметров алгоритма. Мы будем использовать модель вычислений CREW PRAM (Concurrent Read Exclusive Write Parallel Random Access Mashine), то есть многопроцессорную машину с равнодоступной адресацией, в которой на каждом шаге работы алгоритма любой из процессоров может обращаться к любой ячейке общей памяти для чтения, но только один процессор может обращаться к памяти для записи. Прежде чем переходить к описанию алгоритма, дадим несколько предварительных определений. Определение 1.6. Пусть заданы множество функциональных символов Т и множества рабочих и вспомогательных переменных X и У. Пусть д - подстановка из множества Subst[X,y,Т\.
Определение 1.7. Пусть заданы множество функциональных символов Т и множества рабочих и вспомогательных переменных X и У. Пусть д\ и 1 произвольные подстановки из множества Subst[X,У,Т], а 7(А) и /() представляющие их АОГ. Наложением остовного леса Т АОГ (і9і) на АОГ G($2) назовем отображение Ш : Vertex(T) - Vertex{Q{-d2)), такое что: - для каждой переменной х из множества Хт верно равенство B(VT(x)) = Vg{,2)(x); - для каждой вершины V из множества Vertex(T) и для каждой исходящей из нее дуги (V,V) с номером г в дереве Т верно равенство B(V ) = descgi#2)(B(V),i). Заметим, что наложение остовного леса Т АОГ 0($і) на АОГ () существует не для любых подстановок ді и і92 Определение 1.8. Пусть заданы множество функциональных символов J7 и множество вспомогательных переменных У. Направленным путем Т назовем помеченное ориентированное корневое дерево, в котором - из каждой вершины исходит не более одной дуги; - единственный лист помечен символом из множества У U С ; - все нелистовые вершины помечены символами из множества Т\ - каждая дуга (U, V) помечена числом от 1 до т, где т - валентность функционального символа, являющегося пометкой вершины U. Определение 1.9. Пусть заданы множество функциональных символов Т и множество вспомогательных переменных У. Пусть Т - произвольный направленный путь, t - произвольный терм из множества ТегтІУ, 7], a Q{t) - АОГ, представляющий терм t. Наложением направленного пути Т на АОГ G(t), назовем отображение О : Vertex(T ) -+ Vertex(G(t)), такое что: - для корневых вершин Uо и VQ графов Т vs. Q{t) соответственно верно равен ство ОД) = Vb; - для каждой дуги (/, V) с номером г направленного пути Т верно равенство B(descv(U)) = descg(t)(B(U), і). Так же как и наложение остовного дерева на АОГ, не для любых направленного пути Т и терма t существует наложение Т на граф G{t). Пусть Т - ориентированное помеченное упорядоченное корневое дерево с К вершинами и корнем Vo- Нумерацией в глубину вершин этого дерева назовем отображение NDep : Vertex(T) - {1,..., К}, такое что - NDep(V0) = 1; - для любой вершины V дерева Т, для любых исходящих из нее дуг (V,Vi), (V,Vj) с номерами і и j соответственно, таких что і j, и для любых вершин V{ и V{ из поддеревьев, корнями которых являются вершины Vi и Ц-соответственно, верно неравенство NDepiyl) NDep(V). Весом дуги (U, V) дерева Т назовем количество вершин в поддереве с корнем в У.
Понятия контекста и метаконтекста
Основополагающим понятием этой главы является понятие контекста. Неформально, контекст - это ветвь в дереве, представляющем подстановку. Тогда регулярная метаподстановка - это множество контекстов, удовлетворяющее свойствам согласованности, линейности, полноты и регулярности. В этом параграфе исследуются первые два из этих свойств. Пусть V и Н - произвольные множества переменных и функциональных символов фиксированной валентности, а С-н - подмножество констант из П.; переменные из множества V будем называть предметными. Пусть U = {Пі, Пг, } - бесконечное множество переменных, такое что VfMA = 0; переменные из множества U будем называть служебными. В множестве термов Term[V U U, Н] выделим подмножество сингулярных термов STerm[V,H]. (1) Любая переменная или константа из множества VUC-н является сингулярным термом. (2) Пусть Мп) - функциональный символ из множества "Н, s — сингулярный терм из множества STerm\y,Ті], а Пі,..., Ць_ь Dfc+ii - , Пп _ различные служеб ные переменные из множества U, не содержащихся в s. Тогда терм /і(Пь ..., Dfc_i, s, Dfc+i,..., D„) также является сингулярным термом. Для сингулярного терма s внешний (самый левый в записи терма) символ из VUH назовем главным и обозначим Top(s), а внутренний (единственный принадлежащий множеству V U Сп) - назовем выделенным и обозначим Leaf(s). Кроме того, общее количество символов из множестве V U Н в сингулярном терме назовем его длиной; длину сингулярного терма s обозначим Len(s). Определение 2.1. Пусть Vi и 1 - произвольные множества предметных переменных, где Vi = {v1,..., vn,...}, а 7Ї - произвольное множество функциональных символов. Контекстом назовем любую (возможно бесконечную) подстановку вида х = {v1/Пг,...,vk-l/Uk_uvk/s, uh+1/Dk+1,..., ип/Пп,...} из множества подстановок Subst[Vi, V2 UU,Н], обладающую следующими двумя свойствами: (1) s Є STerm[V2,H}; (2) все переменные Пі,..., Пк-і, П +і,..., Dn,... различны и не встречаются в сингулярном терме s.
Множество контекстов, в которых используются попарно непересекающиеся подмножества служебных переменных, обозначим Cont[Vi, V2,7i]. Контексты будем полагать равными, если они совпадают с точностью до переименования служебных переменных из U. Поэтому в дальнейшем для обозначения контекста х = {v1/Di,..., vk 1/Ok-i, vk/s, vk+1/Ok+i,..., vn/On,...} будем использовать запись {... vk/s...}. Для произвольного контекста к — {... vk/s...} обозначим Dom(x) = vk.
Далее будут определены бинарные операции над контекстами и множествами контекстов. Учитывая, что определение контекста предполагает, что все служебные переменные должны быть попарно различны, а равенство контекстов позволяет переименовывать служебные переменные, в дальнейшем по умолчанию будет выполнятся следующее соглашение. Соглашение. Будем считать, что при рассмотрении любых наборов контекстов из множества Cont{Vi, V2,Ti] никакие два различных контекста не имеют общих служебных переменных. Длиной контекста назовем длину его сингулярного терма. Так же как для сингулярных термов, длину произвольного контекста к обозначим символом Len(x). Будем говорить, что подстановка $ из Subst[Vi, V2,Ti] инициализирует контекст к из Cont[VitV2,H], если существует подстановка а из Subst[U, V2,Ti], такая что хга = &. Пусть задано некоторое множество переменных или функциональных символов А. Для обозначения того факта, что это множество разбивается на два непересекающихся подмножества А и А", то есть выполняются соотношения A U А" = А и А ПА" = 0, будем использовать запись А = А + А". Определение 2.2. Пусть заданы множества предметных переменных Vi, V2 и V3 и множество функциональных символов Ті, причем V2 = V2 + V2
Пусть заданы множества предметных переменных V\ и V2, множество функциональных символов Ті и сингулярные термы s Є STermlVo fi], S\ Є STerm[Vi,H] и s2 Є STerm[V2,H]. Пусть также Leaf(si) = v, где v Є Vi. Для обозначения того факта, что сингулярные термы s,s\ и s2 связаны соотношением s = Si{v/s2}, будем использовать запись s — Si(s2).
Пусть заданы множества предметных переменных V\ и V2. Для любого множества контекстов К, К С. Cont[V\,V2,T C], и для произвольного подмножества переменных V, V С V2, обозначим Vary (К) множество выделенных символов контекстов из множества метаконтексты, если это понятно из того, каким множествам они принадлежат. Утверждение 2.9. Пусть заданы множества предметных переменных Vi, V2 и Vi и множество функциональных символов Ті; такие что V2 = V2 + V2, V3 = V3 + V" и Ті = Ті + Ті". Пусть таксисе заданы метаконтексты Мі u М2 из множеств MCont{Vi,V2,V%,Ti ,Ti"] и MCont[V2, V3,V {,Ti ,Ti"\ соответственно. Тогда множество контекстов М = М\ М2 состоит из попарно согласованных контекстов, то есть М Є MCont\yuV V2VJV",Ti ,Ti"\. Доказательство этого утверждения приведено в приложении на станице 195. Определение 2.10. Пусть заданы множества предметных переменных Vi и V2 и множество функциональных символов Ті, такие что V2 = V2 + V2 . Множество К контекстов из Cont[Vi, V2,Ti] назовем линейным по V2, если каждая переменная из множества V2 встречается в контекстах множества К не более одного раза, то есть для любых различных контекстов щ = {... v1/si...} и х2 = {... v2/s2 ..} из К, таких что Leaf(si) Є V2 и Leaf(s2) Є V2, верно неравенство Leaf{s\) Ф Leaf(s2).
Инварианты равенства программ и их представление мета-подстановками
В этом параграфе мы сначала напомним общее определение инварианта программы в точке, а также определения частных случаев инвариантов - инварианта равенства, наиболее специального инварианта в множестве и сильного инварианта. Кроме этого, определим еще один частный случай инварианта - линейный инвариант равенства. После этого покажем, что задачу вычисления наиболее специального инварианта в множестве сильных линейных инвариантов равенства можно свести к задаче вычисления метаподстановки определенного вида.
Пусть / - интерпретация, a F/(/) - произвольное множество инвариантов в точке I модуля М для этой интерпретации. Инвариант Ф(У) в точке I назовем наиболее специальным в множестве F/(Z) если Ф(У) Є F/(Z) и для любого инварианта Ф (У) Є F/(l) формула Ф (У) следует из Ф(У), то есть для любой оценки а имеет место выполнимость / h (Ф0 ) - nV))[a]. Как и ранее, формулу Ф(У) назовем сильным инвариантом в точке I модуля М программы П, если Ф(У) является инвариантом в точке I для любой интерпретации /. Тогда инвариант будет сильным в том и только том случае, когда он будет инвариантом для эрбрановской интерпретации 1[У, Я = {Тегт[У, Т\, Л(П1),..., /» ,= }, то есть когда функциональные символы интерпретируются в свободной алгебре термов сигнатуры Т. Заметим, что для любого множества переменных Q произ вольная оценка а из i[y,j (Q) по определению является подстановкой из шюжс-CTBaSubst[Q,y,f]. Основной задачей этой главы является разработка метода вычисления наиболее специального в множестве сильных линейных инвариантов равенства для произвольной точки I многомодульной программы П. Сведем эту задачу к вычислению метаподстановки определенного вида. Пусть М - модуль завершаемой программы П с множествами рабочих переменных V и переменных входа Вм, а I - точка этого модуля. По свойству завершаемое программы, множество Тг(1) непусто. Обозначим 5(/) следующую метаподстановку: S(0 =Wi (0 S(tr). (3.1)
Определение 3.5. Пусть X произвольное конечное множество рабочих переменных, У - бесконечное множество вспомогательных переменных, а Т - конечное множество функциональных символов. Для каждой подстановки $ из множества SubsV\X,У\Т] назовем линеаризацией единственную линейную подстановку Ып{$) из множества LSubst [X\У\ F], для которой существует переименование с отождествлением Л из Subst [y,y, !F\, такое что выполняется соотношение Lin(&)\ = д.
Таким образом, на основании теоремы 3.10 и утверждения 3.11 заключаем, что для вычисления наиболее специального сильного линейного инварианта равенства в произвольной точке I модуля М завершаемой программы П достаточно построить метаподстановку S (l) — S(l) 0. Эта метаподстановка является конечной минимальной, потому что S(l) является точной нижней гранью непустого множества конечных минимальных метаподстановок, a S (l) не содержит процедурных символов и переменных из множества Вм- В следующем параграфе мы рассмотрим метод вычисления метаподстановки S (l).
Множество трасс Tr(l) в общем случае может быть бесконечным, поэтому воспользоваться для вычисления S (l) непосредственно определением 3.6 нельзя. В этом параграфе будет предложен метод вычисления подстановки S (l) с помощью аппроксимирующих последовательностей - последовательностей метаподстановок, автоматные представления которых, как будет показано в параграфе 3.2.1, можно строить с использованием алгоритма антиунификации MContMST непосредственно из конкретной модели многомодульной программы.
Определение 3.12. Пусть задана произвольная программа П. Рассмотрим любой модуль М = {р "\ V, v, С, Trans, Calls} этой программы с множеством рабочих переменных V = {vi,... ,vn}, множеством переменных входа Вм и точками входа entry и выхода exit. Локальной трассой Itr в модуле М назовем конечную последовательность точек и операторов этого модуля, определенную индуктивно согласно указанным ниже условиям. Наряду с этим, каждой локальной трассе Itr сопоставим конечную минимальную метаподстановку R(ltr) из множества FLMSubst [V,У мі іТІН)}, которая описывает соотношение между значениями рабочих переменных в начале и конце локальной трассы Itr.
