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

004611645

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

Ключников Илья Григорьевич

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

05.13.11 — математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей

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

2 8 ОКТ 2010

Москва - 2010

004611645

Работа выполнена в Институте прикладной математики им. М.В. Келдыша РАН.

Научный руководитель:

кандидат физико-математических наук Романенко Сергей Анатольевич

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

член-корреспондент РАН Абрамов Сергей Михайлович

кандидат физико-математических наук, старший научный сотрудник Бульонков Михаил Алексеевич

Ведущая организация:

Институт системного программирования РАН

Защита состоится 2 ноября 2010 г. в 11 часов на заседании диссертационного совета Д 002.024.01 в Институте прикладной математики им. М.В. Келдыша РАН по адресу: 125047, Москва, Миусская пл,, 4.

С диссертацией можно ознакомиться в библиотеке Института прикладной математики им. М.В. Келдыша РАН.

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

Ученый секретарь диссертационного совета доктор физико-математических наук^/°

Т. А. По ли лова

Общая характеристика работы

Объект исследования и актуальность работы

Одним из распространенных методов формальной верификации программ, обеспечивающих полноту, является проверка на моделях программ (model checking): для многих формализации проверка на моделях программ либо доказывает, что модель всегда удовлетворяет спецификации, либо находит ошибку. Главным недостатком проверки на моделях является то, что проверяется не сама программа, а ее модель.

Другим распространенным методом проверки правильности программ является тестирование: условия корректности компоненты / кодируются в виде предиката (функции) р, и на входных данных Xi, Х2, ..., Хп проверяется истинность p(X1,f(Xi)), p(X2,f{X2)), ..., p{Xn,f(Xn)). Преимущества тестирования: рассматривается реальная система, условия корректности пишутся на том же языке, на котором написана программа. Главным недостатком тестирования является неполнота, - как правило, рассматриваются лишь некоторые входные значения, и успешное прохождение тестов не гарантирует отсутствие ошибок.

Отметим, что р{Х, f{X)) является композицией проверяемой функции / и предиката р. Существуют методы преобразования программ, способные упрощать такие композиции, в результате чего получается программа р'(Х) — ■ ■., которая легче поддается анализу, чем исходная композиция Р(Х,/(Х)).

Одним из таких методов является супер компиляция [9]. В частности, суперкомпиляция была применена А. Немытых для трансформационного анализа кэш-когерентных протоколов (закодированных на языке Рефал) [3]. Суть трансформационного подхода к анализу программ можно сформулировать следующим образом; вместо того, чтобы анализировать исходную программу, вначале преобразуем эту программу в эквивалентную ей, но легче поддающуюся анализу. Если используемый метод преобразования программ способен устранять избыточности исходной программы, то во многих случаях анализ остаточной программы становится тривиальным (например, когда получается программа, выдающая True на всех входных данных: р'{Х) = True).

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

Примером языка, удовлетворяющего этим требованиям, является язык Haskell [8]. С одной стороны программы на языке Haskell достаточно хорошо поддаются преобразованиям. С другой стороны Haskell предлагает

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

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

Цели и задачи работы

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

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

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

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

• Иметь доступный исходный код. Без этого отсутствует сама возможность убедиться в корректности реализации суперкомпилятора.

Такого сунеркомпилятора на момент начала диссертационной работы (2007 год) не существовало1. Поэтому автор поставил перед собой следующие задачи:

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

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

3. Реализовать разработанный алгоритм в экспериментальном суперкомпиляторе.

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

1 Вообще, а не только для языка Haskell.

Научная новизна работы

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

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

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

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

Практическая значимость работы

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

На основе разработанных алгоритмов и методов создан экспериментальный суперкомпилятор HOSC для ядра языка Haskell.

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

На базе суперкомпилятора HOSC создан многоуровневый суперкомпилятор TLSC, способный производить более глубокие преобразования программ, в частности, улучшать асимптотику программ.

Апробация работы и публикации

Результаты работы докладывались на следующих конференциях и семинарах:

• Международный семинар "First International Workshop on Metacom-putation in Russia, META'08", Россия, Переелавль-Залесский, 2008.

• Научный семинар по языкам программирования "Copenhagen Programming Language Seminar (COPLAS)" па факультете информатики Копенгагенского университета, Дания, Копенгаген, 2008.

• Седьмая международная конференция памяти Андрея Ершова "Perspectives of System Informatics, PSF09", Россия, Новосибирск, 2009.

• Международный семинар "International Workshop on Program Understanding, PTJ'09", Россия, Алтай, 2009.

• Объединенный научный семинар по робототехническим системам ИПМ им. М.В. Келдыша РАН, МГУ им. М.В. Ломоносова, МГТУ им. Н.Э. Баумана, ИНОТиИ РГГУ и отделения "Программироват ние" ИПМ им. М.В. Келдыша РАН, Россия, Москва, 2009.

• Семинар московской группы пользователей языка Haskell (MskHUG), Москва, 2009.

• Международный семинар "Second International Workshop on Meta-computation in Russia, МЕТА'Ю", Россия, Переславль-Залесский, 2010.

• Научный семинар ИСП РАН, Россия, Москва, 2010.

По результатам работы имеются четыре публикации, включая одну статью в рецензируемом научном журнале из списка ВАК [1], одну статью в международном периодическом издании [3], две статьи в сборниках трудов международных научных семинаров (2, 4]:

1. Ключников И.Г., Романенко С. A. SPSC: Суперкомпилятор на языке Scala // Программные продукты и системы. - 2009. - №2 (86). -С. 74-80.

2. Klyuchnikov /., Romanenko S. SPSC: a Simple Supercompiler in Scala // International Workshop on Program Understanding, PU 2009, Altai Mountains, Russia, June 19-23,2009. - Novosibirsk: A.P. Ershov Institute of Informatics Systems, 2009. - Pp. 5-17.

3. Klyuchnikov I., Romanenko S. Proving the Equivalence of Higher-Order Terms by Means of Supercompilation // Perspectives of Systems Informatics. 7th International Andrei Ershov Memorial Conference, PSI2009, Novosibirsk, Russia, June 15-19, 2009. Revised Papers. - Vol. 5947 of LNCS. - Springer, 2010. - Pp. 193-205.

4. Klyuchnikov I., Romanenko S. Towards Higher-Level Supercompilation

/ / Proceedings of the second International Workshop on Metacomputation in Russia. Pereslavl-Zalessky, Russia, July 1-5, 2010. - Pereslavl-Zalessky: Ailamazyan University of Pereslavl, 2010. - Pp. 82-101.

Структура и объем диссертации

Диссертация состоит из введения, 8 глав, заключения и списка литературы. Содержание работы изложено на 189 страницах, из них 172 страниц основного текста. Список литературы содержит 141 наименование. В работе содержится 90 рисунков и 3 таблицы.

Содержание работы

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

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

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

Суперкомпиляция была предложена в 1970-х годах В.Ф. Турчиным как метод преобразования программ, написанных на функциональном языке первого порядка Рефал.

В основе суперкомпиляции находятся следующие процедуры:

• Построение размеченного "дерева процессов", которое представляет все возможны трассы некоторого вычислительного процесса. Метки в дереве (конфигурации) представляют множества состояний вычисления.

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

• Преобразование получившегося графа в (остаточную) программу.

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

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

Рис. 1 Выражения языка SLL

е ::= е€ Ecufuv, выражение

v v € V, переменная

| с(е 1,... ,еп) се С, конструктор

| /(ех,..., еп) f е F, вызов функции

Рис. 2 Гомеоморфное вложение SLL-выражений е' < е" если е' <„ е", е' е" или е' <с е"

Вложение переменных и' щ"

Сцепление (Coupling)

h(e>[ ,...,е'п)<с h{e'{, ...,если Уг: « е>! Погружение (Diving) е 5]<г • • •, е'п) если Зг: е < е■

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

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

Основные усилия были направлены на создание работающего оптимизирующего суперкомпилятора. Практическим исследованиям по применению суперкомпиляции для анализа программ не уделялось должного внимания. Появление работающего оптимизирующего суперкомпилятора относится к середине 1990-х годов (суперкомпилятор ЭСР4). Многие части этого суперкомпилятора описаны неполностью или неформально. При использовании суперкомпилятора для анализа программ необходимо полное и формальное описание его внутреннего устройства.

В 90-е годы выходит серия работ Роберта Глюка, Морте Сёренсена, Нила Джонса, рассматривающих суперкомпиляцию для более простых, нежели Рефал, функциональных языков. Одной из целей этих работ было полное и формальное описание простого суперкомпилятора, который сохраняет семантику программы и гарантированно завершается.

Синтаксис выражений языка БЬЬ, рассматриваемого в работах Сёренсена и Глюка [7], приведен на Рис. 1.

Завершаемость суперкомпилятора гарантируется тем, что при построении дерева процессов не допускаются ветки, на которых некоторая "верх-

Рис. 3 Сравнение суперкомпиляторов

Эквива- Функции Беско- Док-во Док-во Исход-

лентные высших нечные кор- завер- ный

преобра- поряд- данные ректно- шаемо- код

зования ков сти сти

SCP4 - - - - - +

Positive SCP + - + + + -

TSG SCP + - - - - +

Jscp + - - - - -

Supero + + + - - +

Timber SCP + + - + + -

HOSC + + + + + +

няя конфигурация" С\ вкладывается в "нижнюю конфигурацию" с?. ci < С2, < - отношение гомеоморфного вложения для SLL-выражений (Рис. 2). При обнаружении таких конфигураций обобщается верхняя конфигурация - вместо нее рассматривается более общая.

Использование отношения < не допускает построения бесконечных ветвей в частичном дереве процессов в силу следующей теоремы:

Теорема 1 (Крускал, Хигман). Пусть С и F - конечные множества. В любой бесконечной последовательности SLL-выражений е\,е2,... из множества Ecufuv найдутся еj и ej такие, что г < j и ei < ej.

То есть, отношение гомеоморфного вложения < является вполне-квази-упорядочением на Ecufuv- Также в главе 1 подробно разбирается алгоритм обобщения SLL-выражений.

Суперкомпилятор для языка SLL, описанный Сёренсеном - первый суперкомпилятор, для которого доказаны теоремы корректности и завершаемое™. Позитивный суперкомпилятор для языка SLL рассматривается как пример полностью и формально описанного суперкомпилятора. То есть результатам анализа, полученным при использовании суперкомпилятора для языка SLL, в принципе, можно доверять.

В таблице на Рис. 3 сравниваются существовавшие на 2007 год2 суперкомпиляторы с точки зрения пригодности для трансформационного анализа программ по критериям, указанным в колонках. На момент начала работы над диссертацией суперкомпилятора, удовлетворяющего всем рассматриваемым критериям, не существовало. Одним из результатов данной работы явилось создание экспериментального суперкомпилятора HOSC, удовлетворяющего всем требованиям.

Входным языком суперкомпилятора HOSC является язык HLL, который формально описывается в главе 2 "Язык HLL: синтаксис и семанти-

2Когда автор начал работу над диссертацией.

Рис. 4 Синтаксис HLL-выражений

: V

переменная

| с Щ конструктор

| / глобальная переменная

| Л Щ -4 е Л-абстракция

| е\ в2 аппликация | case ео of {pi е*;} сайе-выражение

| let Vi — ei\ in e let-выражение

| (e) выражение в скобках

p :: = сщ образец

ка". Язык HLL является подмножеством ядра языка Haskell и выбран таким образом, чтобы минимизировать количество рассматриваемых сущностей в описании синтаксиса, семантики языка и при доказательствах корректности и завершаемости, оставаясь в то же время максимально приближенным к ядру языку Haskell.

Синтаксис выражений языка HLL приведен на Рис. 4 - в HLL-выраже-ниях присутствуют связанные переменные. В последние годы наблюдается интерес к суперкомпиляции языков высшего порядка (со связанными переменными), таким как Haskell, Timber. Однако, опубликованные работы обходят стороной алгоритм обобщения выражений со связанными переменными. Отчасти, это связано с тем, что авторы слишком неформально работают со связанными переменными. В данной работе использование связанных переменных строго формализовано - выбрано соглашение об именовании переменных (соглашение Барендрегта) и вводится понятие допустимой для выражения подстановки.

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

Также в главе 2 рассматривается операционная семантика языка с вызовом по имени (call-by-name)3.

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

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

Рис. 5 Отношение трансформации HOSC: алгоритм построения частичного дерева процессов t для конфигурации во

t = (eo)

while incomplete(t) do /3 — unprocessedLeaf (t)

t = choice{drive*(t,l3},generalize(t,f3),fold(t,P)} end

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

Определение 2 (Эквивалентность). Два НЬЬ-выражения е\ и ег являются эквивалентными, если для любого контекста С[ ], такого, что С[в1] и С[ег] - замкнутые выражения, вычисления выражений С[е{\ и С[ег] либо вместе завершаются, либо вместе не завершаются.

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

В главе 3 "Структура суперкомпилятора НОБС" описывается методологическая основа НОБС в виде отношения трансформации [2] (а не конкретного алгоритма). Недетерминированный алгоритм построения частичного дерева процессов приведен на Рис. 5, - таким образом описывается множество остаточных программ.

В главе 3 также дается алгоритм преобразования частичного дерева процессов в остаточную программу, являющуюся одним самодостаточным выражением с локальными определениями. Построение остаточных программ такого вида положительно сказывается на склонности суперкомпилятора НОЭС к нормализации программ.

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

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

В главе 4 "Корректность суперкомпилятора НОБС" приводится доказательство корректности суперкомпилятора НОБС. В отличие от большинства работ, где приводится доказательство корректности конкретного алгоритма, приводится доказательство корректности отношения трансформации, определенного в главе 3, т.е. показывается корректность любого алгоритма, удовлетворяющего этому отношению трансформации.

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

Сперва рассматривается отношение НОБСо, которое допускает свертку только некоторых узлов и не допускает свободных переменных в локальных определениях в остаточной программе. Доказывается теорема, что любая остаточная программа, удовлетворяющая отношению НОБСо, является строгим улучшением исходной программы, а, следовательно, остаточная програма эквивалентна исходной.

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

Наконец, показывается, что результат суперкомпиляции по отношению НОБСх/2 и соответствующий результат по отношению НОБС относятся через Л-дроппинг, а поэтому эквивалентны.

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

Также рассматривается вопрос о корректности отношения трансфор-

и

Рис. 6 Уточненное гомеоморфное вложение HLL-выражений Вложение с учетом таблицы связанных переменных е' <** е" I,, если е' е"|р, е' <у е"\р или е' <** е"

Вложение переменных

/ <г /

и' <r V" \р если (г;', v") € р

v' <** v" |р если v' £ domain(p) и v" range(p)

Сцепление (Coupling)

с7{<?сТ{ \p если \/г: е- <** е'( \р

Xv' -> е' <** Аг>" -» е" если е' <** е" |ри{(и>")}

ео Ц «Г если Уг : <*Х|/>'

case е' of {сг v'ik -> е^;} <** cose е" of {a v''k ->• ej';} |„

если е' <** е" |р и Vi : ej <** < Погружение (Diving) только если fv(e) П domain(p) = 1

если Зг: е <** ег е <2* Лг>0 ео если е <** ео |Pu{(.,v0)}

е <2* ео ё7 _если Зг: е ei \р

е case е' of {с{ Щ -4- е^} |р

Р ИЛИ : е ei lpU{(i^)}

мации НОвС с учетом типизации.

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

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

В главе 5 "Схема суперкомпилятора НОБС" излагается несколько конкретных алгоритмов суперкомпилятора НОЭС. В главе 6 доказывается их корректность.

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

Рис. 7 Результат сравнения суперкомпиляторов

Бс___ Зс_+_ вс__+ БС+__ вс++_

(1) - - - - - + - +

(2) - + + + - + + +

(3) - + - + - + - +

(4) - - - - - + - +

(5) - - + + - - + +

(6) - + + + - + + +

(7) + + + + + + + +

и допустимости подстановки по отношению к выражению.

Предыдущие работы при рассмотрении суперкомпилятора для языка высшего порядка лишь адаптировали классическое гомеоморфного вложение <3: аппликации, А-абстракции и саяе-выражения рассматривались как специальные конструкторы и связанные переменные не различались. Как показали эксперименты, в случае языка высшего порядка, использование "наивного" гомеоморфного вложения, подобного <, дает неудовлетворительные результаты в суперкомпиляторе, предназначенном для трансформационного анализа.

В главе 5 рассматривается вложение <* - уточнение отношения <, в котором различаются связанные переменные: не допускается вложение связанной переменой через погружение, связанная переменная может быть вложена только в соответствующую связанную переменную, аппликации рассматриваются как бинарные конструкторы. Затем вводится усиление вложения <* - вложение <**, в котором аппликации рассматриваются как конструкторы разной арности (Рис. 6). Предложенное вложение обладает следующим свойством: если два НЬЬ-выражения вложены через <", то их обобщение - нетривиальное НЬЬ-выражение.

Как было сказано ранее, для анализа программ может быть полезно иметь несколько результатов суперкомпиляции. В главе 5 описывается параметризованный алгоритм суперкомпилятора НОБС - БС^к. Алгоритм зависит от трех параметров:

1. г - Какое гомеоморфное вложение использовать: (*), <* (+) или <е (-)?

2. у - Разделять ли узлы на глобальные и локальные при поиске релевантных кандидатов [7] (+) или не разделять (—)?

3. к - Разделять ли выражения на классы в соответствие в типом ре-декса (+) или нет (-)?

Все возможные варианты суперкомпилятора корректны, так как соответствуют отношению трансформации НОБС, корректность которого была показана в главе 4.

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

Чтобы подчеркнуть важность учета связанных переменных, сравниваются восемь вариантов суперкомпилятора. Для сравнения используется модельная задача: доказательство эквивалентности выражений. Рассматриваемые тестовые примеры используют функции высших порядков и оперируют потенциально бесконечными данными. Результаты эксперимента, представленные на Рис. 7, показывают, что наилучшим сочетанием параметров является использование уточненного гомеоморфного вложения, разделение узлов на локальные и глобальные и разделение выражений на классы в соответствии с типом редекса, - именно такое сочетание параметров выбирается для использования в суперкомпиляторе НОБС (вместо вложения <* используется его усиление - <с*) 4-

Таким образом, в главе 5 завершено полное и формальное описание внутреннего устройства суперкомпилятора НОБС.

Осталось доказать, что суперкомпилятор НОБС завершается на любой входной программе. В главе 6 "Завершаемость суперкомпилятора НОБС" доказывается завершаемость всех алгоритмов, представленных в главе 5.

Для доказательства завершаемости используется инструментарий абстрактных преобразователей программ, разработанный Сёренсеном [б], поскольку суперкомпилятор НОБС можно рассматривать как абстрактный преобразователь программ (частичных деревьев процессов).

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

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

4То есть под суперкомпилятором НОБС понимается суперкомпилятор 5С»-(-+.

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

Как было показано в первой главе (теорема 1), отношение < является вполне-квазиупорядочением на множестве ЕсигиУ 8ЬЬ-выражений при конечных С и Р. То же самое относится и к отношению < для выражений языка НЬЬ. Однако, как было показано на модельной задаче, отношение < для НЬЬ-выражений дает неудовлетворительные результаты при использовании суперкомпилятора для трансформационного анаг лиза. Использование предложенного автором уточненного вложения <**, напротив, дает лучшие результаты.

Легко показать, что уточненное вложение <** не является вполне-квазиупорядочением на множестве Бситу НЬЬ-выражений при конечных С и Однако, для завершаемости суперкомпилятора достаточно, чтобы уточненное вложение <** было вполне-квазиупорядочением не на всем множестве -ЕсиРиУ НЬЬ-выражений, а на множестве выражений, которыми помечаются узлы частичного дерева процессов.

Теорема 3 (Ключников). Пусть Мр - множество НЬЬ-выражений, возникающих в узлах частичного дерева процессов для программы Р, строящегося по алгоритму на Рис. 5. В любой бесконечной последовательности НЬЬ-выражений е\, ег,... из множества Мр найдутся е* и

такие, что г < j и ег- <** е^.

Доказательство теоремы 3 происходит в три этапа:

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

2. Рассматривается отношение <2 , являющееся уточнением отношения <1 и гарантирующее нетривиальное обобщения для е\ и е2, если б1 ег- Показывается, что с помощью расширенных индексов де Брюина и факта того, что <1 - вполне-квазиупорядочение, доказательство того, что <2 - вполне-квазиупорядочение на множестве Мр, сводится к теореме 1.

3. Доказывается, что <** - вполне-квазиупорядочение на множестве Мр, - показываем, что в силу типизации исходной программы по Хиндли-Милнеру максимальная арность аппликации выражений в узлах дерева процессов ограничена.

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

Из теоремы 3 следует завершаемость суперкомпилятора HOSC.

Таким образом в диссертации полностью и формально описан суперкомпилятор HOSC (главы 3, 5), доказана его корректность и завершаемость. То есть, суперкомпилятор HOSC удовлетворяет требованиям, предъявляемым к суперкомпилятору, предназначенному для трансформационного анализа (таблица на Рис. 3).

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

Пусть А =>■¡с А' обозначает, что А' по смыслу эквивалентно А и может быть получено как результат суперкомпиляции А, или, другими словами, =>sc есть "отношение суперкомпиляции" (в терминологии Климова [2]).

Пусть = обозначает эквивалентность и = означает "равенство текстов". Верно следующее:

А А! В =»дс В' А! = В' А^В

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

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

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

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

Доказательство эквивалентности двух выражений tl и t2 можно свести к доказательству свойства одного выражения. А именно: если equals

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

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

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

2. Подход, основанный на нормализации, работает для бесконечных данных.

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

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

В качестве тестов для проверки способности суперкомпилятора HOSC распознавать эквивалентность выражений рассматриваются примеры из первой главы книги "Алгебра программирования" Ричарда Бёрда, где эквивалентность выражений доказывается ручными преобразованиями. Суперкомпилятор HOSC распознает эквивалентность всех 25 примеров в полностью автоматическом режиме. Стоит отметить, что если использовать в качестве свистка не уточненное вложение <**, а адаптацию классического вложения <, то суперкомпилятор HOSC распознает лишь 6 эквивалентностей из 25. Это показывает плодотворность использования уточненного вложения <**.

В языке Haskell существуют требования к согласованности некоторых операций, которые определяются программистом при реализации монады. Монада - это некоторый алгебраический тип данных и набор функций для операций над значениями типов. Монада определяется следующими операциями (некоторые из них не являются обязательными): return, join, bind, fmap, mzero. Монадические операции, определяемые программистом, должны удовлетворять, среди прочего, следующим соотношениям:

1. Va, к.join (return а) к = к а

2. Vm, к, h.join т (Ах join (к х) h) = join (join т к) h

3. Vf.join mzero f = mzero

4. Vv.bind v mzero = mzero

Компилятор языка Haskell не способен проверить выполнения этих соотношений для конкретной реализации монады.

Однако, эта задача сводится к распознаванию эквивалентности выражений. Во второй части главы 7 рассматриваются три монады из стандартной библиотеки языка Haskell - List, Maybe, State.

Суперкомпилятор HOSC распознал соотношения 1, 2 и 3 как эквивалентные для всех монад, распознал соотношение 4 как соотношение эквивалентности для монады State. Для монад Maybe и List из анализа остаточных программ, полученных при проверке 4-го соотношения, видно, что оно выполняется только для строгих v (вычисление v завершается и в случае списков представляет из себя конечную структуру).

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

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

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

Недостижимая в большинстве случаев цель суперкомпиляции - построить идеальное дерево процессов [1]. Частичное дерево процессов не является идеальным, если при его построении были произведены обобщения. Отсюда представляется логичным пытаться применять леммы, чтобы избежать обобщения.

На примерах показано, как возможности суперкомпиляции могут быть расширены за счет применения лемм (замены выражений на эквивалентные выражения). С другой стороны, суперкомпилятор сам может быть использован для распознавания эквивалентности двух выражений. Тогда, применяя к этому принцип метасистемного перехода [10], как следствие получаем идею многоуровневой суперкомпиляции: построим башню суперкомпиляторов, - суперкомпиляторы верхнего уровня управляют суперкомпиляторами, расположенными ниже, чтобы получить (и затем применить) леммы. Леммы запрашиваются, когда у суперкомпилятора верхнего уровня обнаруживается ситуация гомеоморфного вложения конфигураций - леммы применяются для избежания обобщения. В главе 8 описан алгоритм такого суперкомпилятора в общем виде.

Однако, в общем случае суперкомпилятор, применяющий леммы, может выдавать некорректную остаточную программу. Дэвидом Сэндсом

Рис. 8 Алгоритм распознавания улучшающих лемм

т>п Vi: ei t^ е •

gCgeil = SCje2Д 5С[е1Д >* «SC[e2l ei >3 e2

тф(ег,..., efc)>* пф{е e'k)

было показано [5], что замена выражения е\ на эквивалентное ему выражение е2 не нарушает корректность преобразования, если выражение е2 является строгим улучшением выражения е.\. Для удобства будем называть упорядоченную пару таких выражений улучшающей леммой.

Определение 4 (Улучшающая лемма). Упорядоченная пара (ei,e2) является улучшающей леммой, е\ >s е2, если выражение операционно эквивалентно выражению е2, ei = е2, и если в любом контексте С, таком, что C[ei] и С[е2] - замкнутые выражения, если вычисление выражения С[еi] завершается за п вызовов функций, то вычисление выражения С[е2] завершается не более чем за п вызовов функций.

Сэндсом было показано, что применение улучшающих лемм дает корректные результаты.

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

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

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

Доказывается следующая теорема:

Теорема 5 (Распознавание улучшений). Пусть е!х = <SC[ei]] и е2 = SC[e2J. Если е[ = е2 и е[ >Z е'2, то е\ >s е2

На базе суперкомпилятора HOSC и применении улучшающих лемм разработан двухуровневый модельный суперкомпилятор TLSC. На мо-

5аналогичное гомеоморфному вложению

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

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

Результаты

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

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

— Сформулировано уточненное отношение гомеоморфного вложения.

— Расширен алгоритм нахожения тесного обобщения.

— Доказаны корректность и завершаемость алгоритма.

• Разработанный алгоритм реализован в экспериментальном суперкомпиляторе HOSC для языка Haskell. Суперкомпилятор HOSC является первым суперкомпилятором языка Haskell, для которого формально доказаны теоремы корректности и завершаемости.

• Разработан алгоритм распознавания эквивалентности выражений на основе синтаксического сравнения остаточных программ. Этот алгоритм реализован в суперкомпиляторе HOSC и работает в полностью автоматическом режиме.

• Предложен и реализован алгоритм распознавания улучшающих лемм.

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

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

Список литературы

[1] Gliick R., Klimov A. V. Occam's razor in metacompuation: the notion of a perfect process tree // WS A '93: Proceedings of the Third International Workshop on Static Analysis. - Springer, 1993. - Pp. 112-123.

[2] Klimov A. V. к program specialization relation based on supercompilation and its properties // First International Workshop on Metacomputa-tion in Russia. — Ailamazyan University of Pereslavl, 2008. — Pp. 54-77.

[3] Lisitsa A., Nemytykh A. Verification as a parameterized testing (experiments with the SCP4 supercompiler) // Programming and Computer Software. - 2007. - Vol. 33, no. 1. - Pp. 14-23.

[4] Lisitsa A., Webster M. Supercompilation for equivalence testing in meta-morphic computer viruses detection // First International Workshop on Metacomputation in Russia. — Ailamazyan University of Pereslavl, 2008.-Pp. 113-118.

[5] Sands D. Total correctness by local improvement in the transformation of functional programs // ACM Trans. Program. Lang. Syst.— 1996. — Vol. 18, no. 2.-Pp. 175-234.

[6] S0rensen M. H. Convergence of program transformers in the metric space of trees // Mathematics of Program Construction.— Vol. 1422 of LNCS. - Springer, 1998. - Pp. 315-337.

[7] S0rensen M. H., Gliick R. Introduction to supercompilation // Partial Evaluation. Practice and Theory.— Vol. 1706 of LNCS.— Springer, 1998. - Pp. 246-270.

[8] The GHC Team. Haskell 2010 language report. - http: //haskell. org/ definition/haskell2010.pdf. — 2010.

[9] Turchin V. F. The concept of a supercompiler // ACM Transactions on Programming Languages and Systems (TOPLAS).— 1986.— Vol. 8, no. 3. — Pp. 292-325.

[10] Turchin V. F. Metacomputation: Metasystem transitions plus supercompilation // Partial Evaluation. - Vol. 1110 of LNCS. - Springer, 1996. -Pp. 481-509.

Отпечатано в ООО «Компания Спутник+» ПД № 1-00007 от 25.09.2000 г. Подписано в печать 01.10.2010 Тираж 100 экз. Усл. п.л. 1,5 Печать авторефератов (495)730-47-74,778-45-60

Введение

1 Позитивная суперкомпиляция и анализ программ

1.1 Исторический обзор.

1.1.1 Суперкомпиляция Рефала.

1.1.2 Суперкомпиляция функциональных языков первого порядка.

1.1.3 Суперкомпиляции императивных языков.

1.1.4 Суперкомпиляция функциональных языков высшего порядка.

1.1.5 Другие работы.

1.2 Суперкомпиляция функционального языка первого порядка

1.2.1 Примеры суперкомпиляции.

1.2.2 Синтаксис и семантика языка ЭЬЬ.

1.2.3 Обобщение и гомеоморфное вложение ЗЬЬ-выражений

1.2.4 Построение дерева процессов.

1.2.5 Построение частичного дерева процессов.

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

1.4 Выводы.

2 Язык НЬЬ: синтаксис и семантика

2.1 Формализация языка НЬЬ.

2.2 Синтаксис языка НЬЬ.

2.3 Подстановка.

2.4 Семантика языка НЬЬ.

2.5 Типизация.

2.6 Алгебра НЪЬ-выражений.

2.7 Выводы.

3 Структура суперкомпилятора НОЭС

3.1 Устранение локальных определений.

3.2 Представление множеств.

3.3 Построение частичного дерева процессов.

3.4 Генерация остаточной программы.

3.5 Отношение транформации НОЭС.

3.6 Выводы.

4 Корректность суперкомпилятора НОЯС

4.1 Операционная теория улучшений.

4.2 Корректность отношения трансформации НОвСо.

4.3 Корректность отношения трансформации НОЗС\/2.

4.3.1 Пример сведения отношения ИОБС^^ к отношению

НО Б Со.

4.4 Корректность отношения трансформации НОБС

4.5 Типизация и корректность.

4.6 Выводы.

5 Схема суперкомпилятора НОвС

5.1 Язык НЬЬ: вложеиие и обобщение.

5.2 Параметризованный НЬЬ суперкомпилятор.

5.2.1 Конкретные НЪЬ суперкомпиляторы.

5.3 Сравнение суперкомпиляторов

5.4 Усиление уточненного вложения с учетом типизации

5.5 Выводы.

6 Завершаемость суперкомпилятора НОБС

6.1 Абстрактные преобразователи программ.

6.2 Гомеоморфное вложение <Р*.

6.2.1 Связанные переменные.

6.2.2 Высший порядок и арность.

6.3 Вполне-квазиупорядочение <**.

6.3.1 Замена case-выражений на конструкторы.

6.3.2 Замена имен переменных на индексы де Брюина

6.3.3 Расширенные индексы де Брюина.

6.3.4 Проблема арности.

6.3.5 Кодировка

6.4 Завершаемость суперкомпилятора SC*.

6.5 Пересмотр обработки ситуации зацикливания

6.6 Завершаемость остальных суперкомпиляторов.

6.7 Выводы.

7 Распознавание эквивалентности выражений

7.1 Моделирование знаний в виде программ.

7.2 Доказательство свойств программ методами суперкомпиляции

7.3 Доказательство эквивалентности выражений.

7.3.1 Доказательство эквивалентности выражений, основанное на равенстве.

7.3.2 Доказательство эквивалентности выражений, основанное на нормализации

7.3.3 Генерация множеств эквивалентных выражений

7.4 Проверка корректности реализаций монад

7.5 Выводы.

8 Метод многоуровневой суперкомпиляции

8.1 Многоуровневая суперкомпиляция.

8.1.1 Накапливающий параметр: базовая суперкомпиляция

8.1.2 Накапливающий параметр: применение леммы

8.1.3 Соединение суперкомпиляторов, переход к многоуровневой суперкомпиляции.

8.1.4 Генерация множества остаточных программ.

8.1.5 Несколько открытых вопросов

8.2 Корректность = эквивалентность + улучшение.

8.2.1 Распознавание улучшающих лемм.

8.3 Модельный двухуровневый суперкомпилятор.

8.4 Примеры.

8.4.1 Суперкомпиляция нелинейного выражения.

8.4.2 Накапливающий параметр.

8.4.3 Улучшение асимптотики программ.

8.5 Выводы.

Объект исследования и актуальность работы

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

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

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

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

Наиболее очевидным и широко распространенным методом проверки правильности систем является тестирование - проверка построенной системы в различных ситуациях, при различных исходных данных. Наиболее распространено модульное тестирование (unit testing). Инструменты для модульного тестирования существуют практически для любого языка программирования [38]. При модульном тестировании рассматривается некоторый компонент, например некоторый модуль (функция) /, принимающий на вход некоторый параметр X. Результатом работы модуля являются некоторые данные Y:

Y = f(X)

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

Y = f(X) P(Y)

Или: v{f{X))

Если при тестировании проверяется работа модуля на входных параметрах Xi,X2, -. Хп, то, соответственно, рассматривается выполнение предикатов p{f{X1)),p{f{X2)),.M{Xn))

Зачастую предикат может сам зависеть от значений входного параметра:

P(XJ(X))

Тогда рассматриваются выполнения предикатов p(X1J(X1)),p(X2, f(X2)),. ,р(Хп, f(Xn))

Тестирование имеет множество преимуществ:

Рассматривается реальная система.

• Проверка может выполняться в реальной среде с реальными интерфейсами.

• Проверять можно наиболее опасные или часто используемые режимы работы системы.

• Программист сам пишет тесты на том же языке, на котором написана программа.

В то же время у тестирования есть и недостатки:

• Тестированием можно проверить лишь немногие траектории вычисления системы (их обычно бесконечное множество).

• Тестированием сложно проверить редко выявляющиеся ошибки, особенно ошибки в системах реального времени.

• Тестирование не может гарантировать правильность системы: "тестированием можно доказать только наличие ошибок". (Дейкстра).

Другим подходом к проверке корректности программ является формальная верификация продукта. Формальная верификация программ -приемы и методы формального доказательства (или опровержения) того, что программа удовлетворяет заданной формальной спецификации. Одним из распространенных методов формальной верификации программ является проверка на моделях программ (model checking) [18]. Доказать, что конкретная реализация продукта (программа) удовлетворяет некоторым формальным требованиям очень сложно, поэтому при проверке на моделях проверяется не сама программа, а ее формальная модель. Формальная модель строится вручную. Обычно такал модель значительно проще проверяемой системы, - это абстракция, которая отражает наиболее существенные характеристики системы. Как и в случае тестирования, при проверке на моделях при описании условий корректности записывается некоторый предикат (логическая формула) относительно модели, и проверяется, будет лн заданная формула выполняться всегда на данной модели. Соответственно, есть различные языки описаний моделей и логических формул (темпоральные логики, структуры Крипке, бинарные решающие диаграммы, и т.д.).

Проверка на моделях программ обладает следующими преимуществами.

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

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

• Можно проверять модель программы еще до написания самой программы.

Однако и у формальной верификации есть ряд недостатков:

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

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

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

Существуют методы, в которых модель программы (вычислений) строится автоматически, — несущественные с точки зрения системы детали отбрасываются, и затем происходит моделирование вычислений. Здесь уместно упомянуть такие методы как символьное выполнение [55] и абстрактную интерпретацию [20]. В некоторых случая утверждения о корректности программ записываются практически на том же самом языке, что и верифицируемая программа [131].

Как было отмечено, главным недостатком тестирования предиката р(Х, f(X)) при конкретных условиях

P(X1J(X1)))P(X2, /№)),. ,р(хп, f{xn)) является неполнота. Успешное выполнение тестов не гарантирует отсутствия ошибок.

Предикат р пишется обычно (и это правильно для тестирования) без учета внутренней структуры программы /. Если приглядеться к проверяемому выражению р(Х, f(X)), то легко увидеть, что оно является композицией двух функций - предиката и проверяемой функций /. Существуют методы преобразований программ, способные упрощать композицию двух функций. В случае выражения р(Х, f(X)) преобразование специализирует предикат р для конкретной функции /. Результатом преобразования будет некоторая функция р'

Р'(Х) = ., зависящая только от входного параметра X, но учитывающая особенности композиции конкретного предиката р и конкретной функции /. Если преобразованная программа обладает более простой и ясной структурой по сравнению с исходными программами р и /, то с помощью очень простого анализа текста программы удается показать, что преобразованная программа выдает только True, или найти такие входные параметры X, когда она выдает False.

Одним из методов преобразований программ, способных упрощать композицию функций, является суперкомпиляция. Одним из успешных применений суперкомпиляции для проверки корректности программ является верификация с помощью суперкомпиляции реализаций (на языке РЕФАЛ) ряда протоколов кэш-когерентности, выполненная Андреем Немытых [71] (при этом, в некоторых протоколах удалось найти ошибки). Реализация протокола принимала в качестве входа конечную цепочку команд, и проверялось состояние памяти после выполнения этих команд. Требования, которым должна удовлетворять реализация протокола, кодировались в виде предиката, проверяющего состояния ячеек.

Суть трансформационного анализа программ можно сформулировать следующим образом: вместо того, чтобы анализировать исходную программу, эта программа вначале преобразуется в эквивалентную ей программу," и затем анализируется уже преобразованная программа. Если используемый метод преобразования программ способен устранять многие избыточности исходной программы, то в некоторых случаях анализ остаточной программы становится тривиальным [127, 40].

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

Функциональный язык программирования Haskell можно рассматривать как язык исполняемых спецификаций [46]. Программы на языке Haskell имеют, как правило, простую и ясную структуру и в то же время достаточно хорошо поддаются упрощающим преобразованиям (с сохранением семантики). Семантика языка Haskell детально формализована [110]. Язык Haskell обладает мощными изобразительные средствами, которые облегчают написание на нем спецификаций:

• Функции высших порядков.

• Бесконечные структуры данных.

• Автоматический вывод и проверка типов.

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

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

Цели и задачи работы

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

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

Стоит отметить, что цели оптимизации программ и анализа программ в некоторой степени противоречат друг другу. Главная цель оптимизации программы - получить небольшую и быструю программу, которая может быть труднопонимаемой для человека, иметь запутанную и странную структуру. Более того, оптимизатор не обязательно выдает программу, эквивалентную исходной! Если исходная успешно программа завершается на некоторых входных данных и выдает осмысленный результат, то, несомненно, оптимизированная программа также должна завершаться и выдавать тот же результат. Однако, если исходная программа не завершается, или завершается аварийно, оптимизированной программе позволительно завершаться и выдавать некоторый произвольный результат (особенно, если это позволяет ускорить программу или уменьшить ее размер). Например, суперкомпилятор SCP4 [71, 72] часто осуществляет преобразования функций с расширением области определения.

Если же некоторый метод преобразования программ используется не для оптимизации программ, а для анализа программ, то не предполагается выполнения преобразованных программ. Таким образом, размер и скорость выполнения преобразованной программы больше не играют главной роли. В частности, при преобразованиях позволительно дублировать код. Например, следующее выражение let р = f х у in gpqpr определенно можно преобразовать в g (f х у) q (f х у) г

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

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

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

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

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

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

Поэтому автор поставил перед собой следующие задачи:

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

2. Разработать на базе метода алгоритм суперкомпиляции программ, написанных на ядре языка Haskell, сохраняющий семантику программ и гарантированно завершающийся* на любой входной программе.

3. Реализовать разработанный алгоритм в экспериментальном, суперкомпиляторе.

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

1 Вообще, а не только для языка Haskell.

Научная новизна работы

Структура1 суперкомпилятора, предложенная в работе, допускает более глубокие» преобразования программ, чем методы суперкомпиляции, ориентированные на оптимизацию, с помощью двух приемов:

1. Рассматривается операционная семантика вызова по имени (call-by-name), а не семантика вызова по необходимости (call-by-need)2. Непосредственно перед суперкомпиляцией все локальные определения (let-выражения) поднимаются на верхний уровень методом А-лифтинга, что позволяет существенно упростить дальнейший конфигурационный анализ и агрессивно распространять информацию о текущей конфигурации вниз по дереву процессов.

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

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

Доказательство корректности отношения трансформации HOSC опирается на операционную теорию улучшений Дэвида Сэндса. Стандартный способ доказать корректность трансформации - показать, что остаточная программа является улучшением исходной (в терминологии Сэндса).

2Конечные результаты работы программы при семантике вызова по имени и вызова по необходимости совпадают

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

Все определенные далее алгоритмы суперкомпиляции удовлетворяют отношению трансформации HOSC и, следовательно, корректны.

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

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

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

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

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

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

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

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

Практическая значимость работы

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

На основе разработанных алгоритмов и методов создан экспериментальный суперкомпилятор HOSC для ядра языка Haskell.

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

На базе суперкомпилятора HOSC создан многоуровневый суперкомпилятор TLSC, способный производить более глубокие преобразования программ, в частности, улучшать асимптотику программ.

Апробация работы и публикации

Результаты работы докладывались на следующих конференциях и семинарах:

• Международный семинар "First International Workshop on Metacom-putation in Russia, META'08", Россия, Переславль-Залесский, 2008.

• Научный семинар по языкам программирования "Copenhagen Programming Language Seminar (COPLAS)" на факультете информатики Копенгагенского университета, Дания, Копенгаген, 2008.

• Седьмая международная конференция памяти Андрея Ершова "Perspectives of System Informatics, PSI'09", Россия, Новосибирск, 2009.

• Международный семинар "International Workshop on Program Understanding, PU'09", Россия, Алтай, 2009.

• Объединенный научный семинар по робототехническим системам ИПМ им. М.В. Келдыша РАН, МГУ им. М.В. Ломоносова, МГТУ им. Н.Э. Баумана, ИНОТиИ РГГУ и отделения "Программирование" ИПМ им. М.В. Келдыша РАН, Россия, Москва, 2009.

• Семинар московской группы пользователей языка Haskell (MskHUG), Москва, 2009.

• Международный семинар "Second International Workshop on Meta-computation in Russia, META'10", Россия, Переславль-Залесский, 2010

• Научный семинар ИСП РАН, Россия, Москва, 2010.

По результатам работы имеются четыре публикации, включая одну статью в рецензируемом научном журнале из списка ВАК (1),-одну статью в международном периодическом издании (3), две статьи в сборниках трудов международных научных семинаров (2, 4):

1. Ключников И.Г., Романенко С. A. SPSC: Суперкомпилятор на языке Scala // Программные продукты и системы. - 2009. - №2 (86). -С. 74-80.

2. Klyuchnikov I., Romanenko S. SPSC: a Simple Supercompiler in Scala // International Workshop on Program Understanding, PU 2009, Altai Mountains, Russia, June 19-23, 2009. - Novosibirsk: A.P. Ershov Institute of Informatics Systems, 2009. - Pp. 5-17.

3. Klyuchnikov I., Romanenko S. Proving the Equivalence of Higher-Order Terms by Means of Supercompilation // Perspectives of Systems Informatics. 7th International Andrei Ershov Memorial Conference, PSI 2009, Novosibirsk, Russia, June 15-19, 2009. Revised Papers. - Vol. 5947 of LNCS. - Springer, 2010. - Pp. 193-205.

4. Klyuchnikov I., Romanenko S. Towards Higher-Level Supercompilation Proceedings of the second International Workshop on Metacomputation in Russia. Pereslavl-Zalessky, Russia, July 1-5, 2010. - Pereslavl-Zalessky: Ailamazyan University of Pereslavl, 2010. - Pp. 82-101.

8.5 Выводы,

Главная идея многоуровневой суперкомпиляции основана на принципе метасистемного перехода [116, 125].

Другой подход к расширению возможностей суперкомпиляции, основанный на*принципе метасистемного перехода - дистилляция [39, 43, 41].

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

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

Во-первых, нынешний алгоритм многоуровневой суперкомпиляции (см. Рис. 8.6) применяет лемму к нижней конфигурации в целом. Но леммы могут применяться более тонко:

• Улучшающая лемма (или ее частный случай) может быть применена к подвыражению.

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

Во-вторых, поиск лемм реализован примитивным способом: структура вкладывающихся конфигурации не учитывается. Однако, существуют методы, разработанные в области механического доказывания теорем по индукции (как сопоставление разностей [13], рипплинг [90] и критика расхождения [130]), которые могут быть использованы в более проработанном генераторе лемм.

Многоуровневый суперкомпилятор не зависит от незначительных деталей реализации суперкомпилятора "первого приближения", лежащего в его основе. Тем не менее, некоторые свойства суперкомлилятора имеют значение. Преждевсего, распознавание улучшающих лемм [96, 97] полагается на то, что суперкомпилятор сохраняет свойства завершаемости программ. Не все суперкомпиляторы обладают таким свойством. Например, суперкомпилятор SCP4 [71], работающий с программами на языке Еефал, может расширять область область определения программ, поэтому доказательство эквивалентности выражений, основанное на нормализации суперкомпиляцией, применимо только для завершающихся выражений, оперирующих конечными данными [73].

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

Поскольку любая остаточная программа, порожденная суперкомпилятором HOSC, является самодостаточным выражением, распознавание эквивалентности может сводится к тривиальному сравнению выражений. В случае суперкомпилятора наподобие Supero [78, 76], остаточная программа имеет менее тривиальную структуру, соответственно, сравнение остаточных программ становится более сложным, нежели в случае суперкомпилятора HOSC.

В принципе, многоуровневая суперкомпиляции может быть реализована на базе суперкомпилятора для императивного объектно-ориентированного языка, как например Jscp (суперкомпилятор для Java [58]), но остается ряд технических проблем для исследования.

Заключение

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

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

Сформулировано уточненное отношение гомеоморфного вложения.

Расширен алгоритм нахожения тесного обобщения.

Доказаны корректность и завершаемость алгоритма.

• Разработанный алгоритм реализован в экспериментальном суперкомпиляторе HOSC для языка Haskell. Суперкомпилятор HOSC является первым суперкомпилятором языка Haskell, для которого формально доказаны теоремы корректности и завершаемости.

• Разработан алгоритм распознавания эквивалентности выражений на основе синтаксического сравнения остаточных программ. Этот алгоритм реализован в суперкомпиляторе HOSC и работает в полностью автоматическом режиме.

• Предложен и реализован алгоритм распознавания улучшающих лемм.

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

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

1. Abadi M., Cardelli L., Curien P.L. Explicit substitutions // Journal of functional programming. — 1991. — Vol. 1, no. 4. — Pp. 375-416.

2. Abramov S.M. Metacomputation and program testing // Proceedings of 1st International Workshop on Automated and Algorithmic Debugging.- 1993.

3. Abramov S.M., Glück R. Semantics modifiers: an approach to nonstandard semantics of programming languages // Third Fuji International Symposium on Functional and Logic Programming / Citeseer. — 1998.

4. Abramov S.M., Glück R. From standard to non-standard semantics by semantics modifiers // International Journal of Foundations of Computer Science. — 2001. — Vol. 12, no. 2. — Pp. 171-211.

5. Abramov S.M., Glück R. Inverse Computation and the Universal Resolving Algorithm // Wuhan University Journal of Natural Sciences. — 2001. — Vol. 6, no. 1. Pp. 31-45.

6. Abramov S.M., Glück R. Principles of inverse computation and the universal resolving algorithm // The essence of computation. — Vol. 2566 of LNCS. Springer, 2002. - Pp. 269-295.

7. Abramov S.M., Glück R., Klimov Y. Faster Answers and-Improved Termination in Inverse Computation of Non-Flat Languages. — 2003.

8. Albert E., Vidal G. The narrowing-driven approach to functional logic program specialization // New Generation Computing. — 2002. — Vol. 20, no. 1. Pp. 3-26.

9. Alpuente M., Falaschi M., Vidal G. Partial evaluation of functional logic programs // ACM Transactions on Programming Languages and Systems (TOPLAS). — 1998. Vol. 20, no. 4. — Pp. 768-844.

10. Barendregt H.P. The lambda calculus: its syntax and semantics. — North-Holland, 1984.

11. Basin D. A., Walsh T. Difference Matching // CADE-11; Proceedings of the 11th International Conference on Automated Deduction.

12. Springer-Verlag, 1992. — Pp. 295-309.

13. Bird R., de Moor O. Algebra of programming. — Prentice-Hall, Inc., 1997.

14. Bolingbroke M., Peyton Jones S.L. Supercompilation by Evaluation // Haskell 2010 Symposium. 2010.

15. Boyer R.S., Moore J.S. Proving Theorems about LISP Functions // Journal of the ACM (JACM). — 1975. — Vol. 22, no. 1. Pp. 129144.

16. Burstall R.M., Darlington J. A Transformation System for Developing Recursive Programs // Journal of the ACM (JACM). 1977. - Vol. 24, no. 1. — Pp. 44-67.

17. Clarke E., Grumberg O., D. Peled. Model Checking. — MIT Press, 1999.

18. Cockett R. Deforestation, program transformation, and cutelimination // Electronic Notes in Theoretical Computer Science.2001. Vol. 44, no. 1. - Pp. 88-127.

19. Curry H.B., Fey s R., Craig W. Combinatory logic. — North-Holland, 1958. — Vol. 1.

20. Damas L., Milner R. Principal type-schemes for functional programs // Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages / ACM New York, NY, USA. — 1982.- Pp. 207-212.

21. Danvy O. An Extensional Characterization of Lambda-Lifting and Lambda-Dropping // FLOPS '99: Proceedings of the 4th Fuji International Symposium on Functional and Logic Programming. — Vol. 1722 of LNCS. Springer-Verlag, 1999. - Pp. 241-250.

22. Danvy O., Schultz U.P. Lambda-dropping: transforming recursive equations into programs with block structure // Theor. Comput. Sci. — 2000.- Vol. 248, no. 1-2. Pp. 243-287.

23. De Bruijn N.G. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser Theorem // Indagationes Mathematicae. — 1972. — Vol. 34. Pp. 381-392.

24. Dershowitz N. Termination of rewriting //J. Symb. Comput. — 1987.- Vol. 3, no. 1-2. Pp. 69-116.

25. Dybjer P., Filinski A. Normalization and Partial Evaluation // Applied Semantics. — Vol. 2395 of Lecture Notes in Computer Science. — Springer, 2002. Pp. 137-192.

26. Ershov A.P. On the essence of compilation // Formal Description of Programming Concepts / Ed. by E. Neuhold. — North-Holland, 1978.- Pp. 391-420.

27. Futamura Y. Partial Evaluation of Computation Process An Approach to a Compiler-Compiler // Systems; Computers, Controls. — 1971. — Vol. 2; no. 5. — Pp. 45-50.

28. Gluck R. Is there a fourth Futamura projection? // PEPM '09: Proceedings of the 2009 ACM SIGPLAN workshop, on Partial evaluation and program manipulation. — ACM, 2009. — Pp. 51-60.

29. Glück R., J0rgensen J. Generating Transformers for Deforestation'and Supercompilation // Static Analysis. — Vol. 864 of LNGS. — 1994.

30. Glück R., J0rgensen J. Generating optimizing specializers // IEEE International Conference on Computer Languages. — IEEE Computer Society Press, 1994.

31. Glück R., Klimov A. V. Occam's Razor in Metacompuation: the Notion of a Perfect Process Tree // WSA '93: Proceedings of the Third International Workshop on Static Analysis. — London, UK: Springer-Verlag, 1993. — Pp. 112-123.

32. Glück R., S0rensen M.H. Partial Deduction and Driving are Equivalent // PLIPL'94. Vol. 844 of LNCS. - Springer-Verlag London, UK, 1994. - Pp. 165-181.

33. Glück R., S0rensen M.H. A Roadmap to Metacomputation by Supercompilation // Selected Papers From the International Seminar on Partial Evaluation. — Vol. 1110 of LNGS. 1996. - Pp. 137-160.

34. Glück R., Turchin V.F. Experiments with a self-applicable supercompiler: Tech. Rep. 4: City University of New York, 1989.

35. Glück R., Turchin V.F. Application of metasystem transition to function inversion and transformation // ISSAC '90: Proceedings of the international symposium on Symbolic and algebraic computation. — ACM, 1990. Pp. 286-287.

36. Hamill Paul. Unit test frameworks. — O'Reilly, 2004.

37. Hamilton G. W. Distillation: extracting the essence of programs // Proceedings of the 2007 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation / ACM Press New York, NY, USA. 2007. - Pp. 61-70.

38. Hamilton G. W. Distilling Programs for Verification // Electron. Notes Theor. Comput. Sei. — 2007. — Vol. 190, no. 4. Pp. 17-32.

39. Hindley J.R. The principal type-scheme of an object in combinatory logic // Transactions of the American Mathematical Society. — 1969.- Vol. 146. Pp. 29-60.

40. Holst C.K., Hughes J. Towards binding-time improvement for free // Functional Programming / Springer Verlag. — 1990. — P. 83. Hudak P., Jones M.P. Tech. Rep.: : Yale University, Department of Computer Science, 1994.

41. Johnsson T. Lambda lifting: Transforming programs to recursive equations // Functional programming languages and computer architecture.- Vol. 201 of LNCS. 1985. - Pp. 190-203.

42. Jones N.D. The Essence of Program Transformation by Partial Evaluation and Driving // Logic, language and computation. — Vol. 792 of LNCS. Springer-Verlag, 1994. — Pp. 62-79.

43. Jonsson P.A., Nordlander J. Positive Supercompilation for a higher order call-by-value language // ACM SIGPLAN Notices. — 2009. — Vol. 44, no. 1. — Pp. 277-288.

44. Jonsson P.A., Nordlander J. Supercompiling Overloaded Functions. — submitted to ICFP 2009:

45. Jonsson P.A., Nordlander J. Strengthening Supercompilation For Call-By-Value Languages // Second International Workshop on Metacomputation in Russia. — 2010.

46. King J.C. Symbolic execution and program testing // Commun. ACM.- 1976. Vol. 19, no. 7. - Pp. 385-394.

47. Klimov A". V. A Program Specialization Relation Based on Supercompilation and its Properties // First International Workshop on Metacom-putation in Russia. — 2008. — Pp. 54-77.

48. Klimov A.V. An approach to Supercompilation for Object-Oriented Languages: the Java Supercompiler Case Study // First International Workshop on Metacomputation in Russia. — 2008.

49. Klimov A.V. A Java Supercompiler and its Application to Verification of Cache-Coherence Protocols // Perspectives of Systems Informatics.- Vol. 5947 of LNCS. 2010. - Pp. 185-192.

50. Klyuchnikov I. Supercompiler HOSC 1.0: under the hood: Preprint 63.- Moscow: Keldysh Institute of Applied Mathematics, 2009.

51. Klyuchnikov I. Supercompiler HOSC 1.1: proof of termination: Preprint 21. — Moscow: Keldysh Institute of Applied Mathematics, 2010.

52. Klyuchnikov I. Supercompiler HOSC: proof of correctness: Preprint 31.- Moscow: Keldysh Institute of Applied Mathematics, 2010.

53. Klyuchnikov I., Romanenko S. SPSC: a Simple Supercompiler in Scala // PU'09 (International Workshop on Program Understanding).- 2009.

54. Klyuchnikov I., Romanenko S. Proving the Equivalence of Higher-Order Terms by Means of Supercompilation // Perspectives of Systems Informatics. — Vol. 5947 of LNCS. 2010. — Pp. 193-205.

55. Klyuchnikov I., Romanenko S. Towards Higher-Level Supercompilation // Second International Workshop on Metacomputation in Russia.- 2010.

56. Krustev D. A Simple Supercompiler Formally Verified in Coq // Second International Workshop on Metacomputation in Russia. — 2010.

57. Lassez J.-L., Maher M.J., Marriott K. Unification Revisited // Proceedings of the Workshop on Foundations of Logic and Functional Programming. — Vol. 306 of LNCS. — Springer-Verlag, 1988. — Pp. 67-113.

58. Leuschel M. On' the power of homeomorphic embedding for online termination // Static Analysis. — Vol. 1503 of Lecture Notes in Computer Science: — Springer, 1998. — Pp. 230-245.

59. Leuschel 'M. Homeomorphic Embedding for Online'Termination,of Symbolic Methods // The essence of computation. — Vol. 2566 of Lecture Notes in Computer Science. — Springer, 2002. — Pp. 379-403.

60. Lisitsa A., Nemytykh A. Towards Verification via Supercompilation // COMPSAC '05: Proceedings of the 29th Annual International Computer Software and Applications Conference. — IEEE Computer Society, 2005.- Pp. 9-10.

61. Lisitsa A., Nemytykh A. A Note on Specialization of Interpreters // CSR '07: Proceedings of the 2nd international symposium on Computer Science in Russia. — Vol. 4649 of LNCS. — 2007. — Pp. 237-248.

62. Lisitsa A.P., Nemytykh A.P. Verification as a parameterized testing (experiments with the SCP4 supercompiler) // Programming and Computer Software. — 2007. — Vol. 33, no. 1. — Pp. 14-23.

63. Lisitsa A., Nemytykh A. Reachability Analysis in Verification via Su» percompilation // International Journal of Foundations of Computer

64. Science. — 2008. — Vol. 19, no. 4. — Pp. 953-969.

65. Lisitsa A., Webster M. Supercompilation for Equivalence Testing in Metamorphic Computer Viruses Detection // Proceedings of the First International Workshop on Metacomputation in Russia. — Ailamazyan University of Pereslavl, 2008. — Pp. 113-118.

66. Marlow S., Wadler P. Deforestation for Higher-Order Functions // Proceedings of the 1992 Glasgow Workshop on Functional Programming.

67. Springer, 1992. Pp. 154-165.

68. Mendel-Gleason G.E., Hamilton G. W. Equivalence in Supercompilation and'Normalisation By Evaluation // Second International Workshop on Metacomputation in Russia. — 2010.

69. Mitchell N. Transformation and Analysis of Functional Programs: Ph.D. thesis / University of York. — 2008.

70. Mitchell N. Rethinking Supercompilation // ICFP 2010. — 2010.

71. Mitchell N., Runciman C. A Supercompiler for Core Haskell // Implementation and Application of Functional Languages. — Vol. 5083 of

72. CS. Springer-Verlag, 2008. - Pp. 147-164.i

73. Monsuez B. Polymorphic Typing for Call-by-Name Semantics // Proceedings of the International Conference on Formal Methods in Programming and Their Applications. — Springer-Verlag, 1993. — Pp. 156169.

74. Nemytykh A. P. Supercompiler SCP4: Use of quasi-distributive laws in program transformation // Wuhan University journal of natural sciences. — 2001. — Vol. 6, no. 1. — Pp. 375-382.

75. Nemytykh A.P. A note on elimination of simplest recursions // ASIA-PEPM '02: Proceedings of the ASIAN symposium on Partial evaluation and semantics-based program manipulation. — ACM, 2002. — Pp. 138146.

76. Nemytykh A.P. The Supercompiler SCP4: General Structure // PSI 2003. Vol. 2890 of LNCS. — Springer, 2003. - Pp. 162-170.

77. Nemytykh A., Pinchuk V. Program Transformation with Metasystem Transitions: Experiments with a Supercompiler // LNCS. — 1996. — Pp. 249-260.

78. Nemytykh A.P., Pinchuk V.A., Turchin V.F. A Self-Applicable Supercompiler // Selected Papers from the International Seminar on Partial Evaluation. — Vol. 1110 of LNCS. 1996. — Pp. 322-337.

79. Peyton Jones S.L. An introduction to fully-lazy supercombinators // Combinators and Functional Programming Languages. — Vol. 242 of LNCS. Springer, 1986. - Pp. 175-206.

80. Peyton Jones S.L. The Implementation of Functional Programming Languages. — Prentice-Hall, Inc., 1987.

81. Pitts A.M. Operationally-based theories of program equivalence // Semantics and Logics of Computation. — 1997. — Pp. 241-298.

82. Plotkin G.D. Call-by-name, call-by-value and the A-calculus // Theoretical computer science. — 1975. — Vol. 1, no. 2. — Pp. 125-159.

83. Reich J.S., Naylor M., Runciman C. Supercompilation and the Reduc-eron // Proceedings of the Second International Workshop on Meta-computation in Russia. — 2010.

84. Rippling: a heuristic for guiding inductive proofs / A. Bundy, A. Stevens, F. van Harmelen et al. // Artif. Intell. — 1993. — Vol. 62, no. 2. — Pp. 185-253.

85. Romanenko A.Y. Inversion and metacomputation // PEPM '91: Proceedings of the 1991 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation. — ACM, 1991. — Pp. 1222.

86. Romanenko S.A. Higher-Order Functions as a Substitute for Partial Evaluation // Proceedings of the First International Workshop on Metacomputation in Russia. — Ailamazyan University of Pereslavl, 2008.

87. Rose K.H. Explicit Substitution Tutorial & Survey: Tech. Rep. LS-96-3: BRICS, 1996.

88. Sands D. Operational theories of improvement in functional languages // Proceedings of the Fourth Glasgow Workshop on Functional Programming. — 1991.

89. Sands D. Proving the correctness of recursion-based automatic program transformations // Theoretical Computer Science. — 1996. — Vol. 167, no. 1-2. Pp. 193-233.

90. Sands D. Total correctness by local improvement in the transformation of functional programs // A CM Trans. Program. Lang. Syst. — 1996. — Vol. 18, no. 2. — Pp. 175-234.

91. Santos A. Compilation by Transformation in Non-Strict Functional Languages: Ph.D. thesis / Glasgow University, Department of Computing Science. — 1995.

92. Schultz U.P. — Implicit and explicit aspects of scope and block structure. — Master's thesis, DAIMI, Department of Computer Science,

93. University of Aarhus, 1997.

94. Secher J.P. — Perfect Supercompilation. — Master's thesis, Department of Computer Science, University of Copenhagen, 1999.

95. Secher J.P. Driving-Based program transformation in theory and practice: Ph.D. thesis / Department of Computer Science, Copenhagen University. — 2002.

96. Secher J.P., S0rensen M.H. On Perfect Supercompilation // PSI '99. — Vol. 1755 of LNCS. — Springer-Verlag, 2000. — Pp. 113-127.

97. S0rensen M.H. —■ Turchin's Supercompiler Revisited: an Operational Theory of Positive Information Propagation. — Master's thesis, K0benhavns Universitet, Datalogisk Institut, 1994.

98. S0rensen M.H., Gliick R. An algorithm of generalization in positive supercompilation // Logic Programming: The 1995 International Symposium / Ed. by J. W. Lloyd. — 1995. — Pp. 465-479.

99. S0rensen M.H., Gliick R. Introduction to Supercompilation // Partial Evaluation. Practice and Theory. — Vol. 1706 of LNCS. — 1998. — Pp. 246-270.

100. S0rensen M.H., Gliick R., Jones N.D. Towards Unifying Partial Evaluation, Deforestation, Supercompilation, and GPC // Programming Languages and Systems. — Vol. 788 of LNCS. — 1994.

101. S0rensen M.H., Gliick R., Jones N.D. A Positive Supercompiler. // Journal of Functional Programming. — 1996. — Vol. 6, no. 6. — Pp. 811838.

102. S0rensen M. H. Convergence of Program Transformers in the Metric Space of Trees // Mathematics of Program Construction. — Vol. 1422 of LNCS. 1998. - Pp. 315-337.

103. Stoughton A. Substitution revisited // Theor. Comput. Sci. — 1988. — Vol. 59, no. 3. Pp. 317-325.

104. The GHC Team. Haskell 2010 Language Report. — http://haskell. org/definition/haskell2010.pdf. — 2010.

105. Tolmach A., Chevalier T., The GHC Team. An External Representation for the GHC Core Language. — http://www.haskell.org/ghc/docs/ 6.12.2/core.pdf. — 2010.

106. Turchin V.F. A supercompiler system based on the language REFAL // SIGPLAN Not. 1979. - Vol. 14, no. 2. - Pp. 46-54.

107. Turchin V.F. The Language Refal: The Theory of Compilation and Metasystem Analysis. — Department of Computer Science, Courant Institute of Mathematical Sciences, New York University, 1980.

108. Turchin V.F. Semantic definitions in REFAL and the automatic production of compilers // Semantics-Directed Compiler Generation, Proceedings of a Workshop. — Vol. 94 of LNCS. — Springer-Verlag, 1980. Pp. 441-474.

109. Turchin V.F. Program transformation by supercompilation // Programs as Data Objects. Vol. 217 of LNCS. — Springer, 1986. — Pp. 257-281.

110. Turchin V.F. The concept of a supercompiler // ACM Transactions on Programming Languages and Systems (TOPLAS). — 1986. — Vol. 8, no. 3. Pp. 292-325.

111. Turchin V.F. A constructive interpretation of the full set theory // Journal of Symbolic Logic. — 1987. — Vol. 52, no. 1. — Pp. 172-201.

112. Turchin V.F. The algorithm of generalization in the supercompiler // Partial Evaluation and Mixed Computation. Proceedings of the IFIP TC2 Workshop. 1988.

113. Turchin V.F. Program transformation with metasystem transitions // Journal of Functional Programming. — 1993. — Vol. 3, no. 03. — Pp. 283-313.

114. Turchin V.F. On Generalization of Lists and Strings in Supercompilation: Tech. Rep. TR 95-002: City University of New York, 1996.

115. Turchin V.F. Supercompilation: Techniques and Results // Perspectives of System Informatics / Springer. — Vol. 1181 of LNCS. — 1996.

116. Turchin V.F., Nemytykh A.P. Metavariables: Their implementation and use in Program Transformation: Tech. Rep. TR 95-012: City College of the City University of New York, 1995.

117. Turchin V.F., Nirenberg R.M., Turchin D. V. Experiments with a supercompiler // LFP '82: Proceedings of the 1982 ACM symposium on LISP and functional programming. — ACM, 1982. — Pp. 47-55.

118. Turchin V. F. The phenomen of science. A cybernetic approach to human evolution. — Columbia University Press, 1977.

119. Turchin V. F. Metacomputation: Metasystem Transitions plus Supercompilation' // Partial Evaluation. —• Vol. 1*110 of Lecture Notes in Computer Science. — Springer, 1996. — Pp. 481-509.

120. Turner D.A. Total Functional Programming // Journal of Universal Computer Science. — 2004. — Vol. 10, no. 7. — Pp. 751-768.

121. Wadler P. Theorems for free! // FPCA '89: Proceedings of the fourth international conference on Functional programming languages and computer architecture. — ACM New York, NY, USA, 1989. — Pp. 347-359.

122. Wadler P., Blott S. How to make ad-hoc polymorphism less ad hoc // POPL '89: Proceedings of the 16th ACM SIGPLAN-SIGACT symposium on Principles of programming languages. — 1989. — Pp. 60-76.

123. Walsh T. A divergence critic for inductive proof // J. Artif Int. Res. — 1996. Vol. 4, no. 1. — Pp. 209-235.

124. Xu D.N.,,Peyton Jones S.L., Claessen K. Static contract checking for Haskell // SIGPLAN Not. 2009. - Vol. 44, no. 1. - Pp. 41-52.

125. Абрамов С.M. Метавычисления и логическое программирование // Программирование. — 1991. — № 3.

126. Абрамов С.М. Метавычисления и их применение. — Наука-Физматлит, 1995.

127. Абрамов С.М., Пармёнова Л.В. Метавычисления и их применение. Суперкомпиляция. — Институт программных систем РАН, 2006.

128. Ключников И.Г., Романеико С. A. SPSC: Суперкомпилятор на языке Scala // Программные продукты и системы. — 2009. — № 2.

129. Турчин В.Ф. Метаязык для формального описания алгоритмических языков // Цифровая вычислительная техника и программирование. — 1966.

130. Турчин В.Ф. Алгоритмический язык рекурсивных функций (РЕ-ФАЛ): Препринт 4: ИПМ, 1968.

131. Турчин В.Ф. Метаалгоритмический язык // Кибернетика. — 1968. №4.

132. Турчин В.Ф. Эквивалентные преобразования рекурсивных функций, описанных на языке РЕФАЛ // Теория языков и методы построения систем программирования. — Киев-Алушта: 1972.

133. Турчин В.Ф. Эквивалентные преобразования программ на РЕФА-Ле: Труды ЦНИПИАСС 6: ЦНИПИАСС, 1974.

134. Флоренцев С.Н., Олюнин В.Ю., Турчин В.Ф. РЕФАЛ-интерпретатор / / Тезисы 1-й Всесоюзной конференции по программированию. — Киев: 1968.