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

>V Б ОД

иГ\Й '^ФрССИЙСКАЯ АКАДЕМИЯ НАУК "" Ордена Ленина Сибирское отделение Вычислительный центр

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

САБЕЛЬФЕЛЬД Виктор Карлович

Анализ свойств и эквивалентные преобразования на моделях программ

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

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

Новосибирск 1994

Работа выполнена в Институте систем информатики Сибирского отделения РАН

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

профессор С.С. Гончаров доктор физико-математических наук профессор В.П. Ильин доктор физико-математических наук профессор Р.И. Подловченко

Ведущая организация — Институт кибернетики АН Украины

Защита состоится ,укЛ2Г ^ 1994 года в

IV

_ часов на заседании специализированного совета Л.002.10.02 по защитам диссертаций на соискание ученой степени доктора наук при Вычислительном центре СО РАН (630090, Новосибирск, 90, пр. Акад. Лаврентьева , 6).

С диссертацией можно ознакомиться в читальном зале ВЦ СО РАН, г. Новосибирск, 90, пр. Акад. Лаврентьева , 6.

Автореферат разослан

-11- 191УГ.

Ученый секретарь специализированного совета кандидат технических наук

Г.И.Забиняко

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

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

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

Основы теории схем программ, центральной задачей которой является проблема эквивалентных преобразований, были заложены в работах A.A. Ляпунова, Ю.И. Янова, А.П. Ершова, В.М. Глушкова, A.A. Летичевского, Д. Лахэма, Д. Парка и М. Патерсона. Значительный вклад в развитие теории внесли Ф.Е. Аллен, М. Берд, Дж. Маккарти, С. Игараши, H.A. Криницкий, С. Гарлэнд, Дж. Бэкус, 3. Манна, Д. Скотт, В.В. Мартынюк, С.С. Лавров, В.А. Тузов, Г.А. Килдел, Р.И. Под-ловченко, Дж. деБаккер, Б.К. Розен, Э. Ашкрофт, А. Пнуели, Дж. Кок, В.А. Непомнящий, В.Э. Иткин, А.О. Буда, Дж. Кэм, Дж.Д. Ульман, Б. Курсель, П. Кузо и Р. Кузо, A.B. Анисимов, Л.П. Лисовик, В.Н. Касьянов, В.Е. Котов, А.Б. Годлевский, Г.Н. Петросян, С.Л. Кривой, и другие.

Несмотря на достигнутые успехи, полного завершения теория эквивалентных-преобразований не получила. Общезначимые полные системы преобразований были построены фактически только для функциональной эквивалентности схем Янова (Ю.И.Янов 1958,1968, А.П.Ершов 1967) и для введенной В.Э.Иткиным логико-термальной эквивалентности стандартных схем (В.К.Сабельфельд 1979). Для моделей рекурсивных программ систематического исследования эквивалентных преобразований не проводилось вовсе.

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

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

систем.

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

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

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

• выявление таких содержательных свойств программ и схем программ, знание которых позволяет производить эквивалентные преобразования;

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

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

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

Публикации и апробация. Основные результаты работы докладывались на Всесоюзной конференции по методам трансляции (Новосибирск, 1981), на Всесоюзном семинаре "Оптимизация и преобразование программ" (Новосибирск, 1982), на национальной школе болгарских Математиков по программирова-

нию (Приморско, 1983), на Всесоюзном семинаре "Алгоритмические проблемы в программировании" (Цесис, 1984), на конференции ИФИП по спецификации и преобразованиям программ (Бад-Тельц, 1986), на Всесоюзной конференции "Проблемы совершенствования синтеза, тестирования и отладки программ" (Рига, 1986), на советско-французском семинаре "Информатика 88" (Ницца,1988), на советско-французском симпозиуме "Информатика 91" (Гренобль,1991), на Всесоюзной конференции по прикладной логике (Новосибирск, 1988), на международной конференции по формальным методам в программировании и приложениях (Новосибирск, 1993), а также на научных семинарах Института систем информатики и Вычислительного центра СО РАН (Новосибирск), Института кибернетики им. В.М. Глушко-ва АН Украины (Киев), Дрезденского технического университета, Института информатики Мюнхенского технического университета, Института математики Аугсбургского университета, лаборатории теоретической информатики и программирования университета Париж-7. Основные результаты работы отражены в 40 публикациях.

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

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

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

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

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

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

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

VI,у,г € £ 1Пх = 1 идемпотентность

хГ[у — уГ\х коммутативность

х П (у П г)) = (х П у) П г ассоциативность

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

х < у <=> хПу = х,

X < у <=> (х П у — х)к.(х Ф у).

Поскольку нас интересуют обычно не синтаксические свойства анализируемого объекта, не его структура, а свойства тех вычислений, которые он описывает, мы говорим о семантических, или содержательных свойствах анализируемого объекта. Метод разметки был впервые использован А.П.Ершовым как средство сбора нелокальной информации в схемах Янова. А. А.Лети-чевский предложил использовать метод разметки для поиска инвариантных соотношений в программах. Позднее Г.Килдел сформулировал единый алгебраический подход к описанию объектов-свойств, в рамках которого построил алгоритм нахождения точного решения задачи глобального анализа графовой модели программы в случае дистрибутивности всех преобразователей свойств. Дж.Кэм и Дж.Ульман ввели понятие окружения для анализа и доказали алгоритмическую неразрешимость задачи потокового анализа (flow analysis problem) графовой модели в общей постановке.

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

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

В диссертационной работе задача анализа семантических свойств

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

• ставится и решается для модели рекурсивных программ;

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

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

1. Достижимость: достижима ли программная точка от начала?

2. Заданиость переменной: верно ли, что переменная задана (имеет какое-нибудь значение) при любом попадании в данную точку?

3. "Мертвость" переменной: верно ли, что значение переменной не понадобится при любом продолжении вычислений после данной точки?

4. Доступность, или избыточность выражения: верно ли, что любому попаданию в данную точку предшествует вычисление и запоминание значения рассматриваемого выражения?

5. Верно ли, что при любом попадании в данную точку значение целочисленной переменной находится в фиксированном диапазоне? 6. Инвариант программной точки: верно ли, что при любом попадании в данную точку инвариант (логическое выражение) принимает значение «истина»?

7. Константность переменной: верно ли, что при любом попадании в данную точку переменная имеет одно и то же значение?

8. Обобщенный тип выражения: верно ли, что при любом попадании в данную точку выражение имеет указанный обобщенный тип?

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

х:=у;

while р(х) do М : x:=x+z; y:=y+z od; F(x,y)

в точке М можно указать, например, {р(ж) Л (® = ?/)}. До цикла значения переменных х и у здесь совпадают, а в цикле

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

while р(у) do М : y:=y+z od; F(y,y)

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

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

лан в работах С.С.Лаврова и А.П.Ершова для другой модели императивных программ — схем Лаврова. Н.Криницкий и С.Игараши независимо построили полные системы преобразований для функциональной эквивалентности ациклических схем. Важное отношение логико-термальной эквивалентности, которое основано на отслеживании логико-термальных историй вычислений в стандартных схемах — еще одной модели императивных программ, описанной Л.Лахэмом, Д.Парком и М.Патерсоном, было введено В.Э.Иткиным, который доказал его разрешимость. Частичное решение проблемы построения полной системы преобразований, сохраняющих логико-термальную эквивалентность, было получено для довольно узких подклассов стандартных схем в работах Син Мен Де и В.Е.Хачатряна. Полное решение эта проблема получила в работах В.К.Сабельфельда.

Назовем оператор присваивания стандартной схемы невырожденным, если его переменная-результат встречается среди аргументов, например х :— f(x,y,z). Схема называется консервативной, если все встречающиеся в ней операторы присваивания являются невырожденными. A.A. Летичевский показал разрешимость эквивалентности для подкласса консервативных схем, в которых?все операторы невырожденные, а условные операторы содержат один и тот же набор переменных, составленный из всех переменных памяти схемы. Г.Н.Петросяну удалось обобщить этот результат на случай, когда каждый условный оператор содержит один и тот же набор переменных, составленный из переменных некоторой выделенной подпамя-ти схемы.

А.В.Годлевский доказал разрешимость эквивалентности в следующем классе схем: все предикатные символы одноместны, и аргументом всех условных операторов является выделенная переменная х, а все присваивания переменной х имеют вид х := f(x,...), т.е. первым аргументом служит переменная х.

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

терялся ни один из термов, на которых проверяются условия распознавателей. Всякий такой терм должен встречаться в качестве подтерма каждого последующего теста этого вычисления. Если, например, р(<Т1,..., ап) и q(т^,..., гт) — два следующих друг за другом теста вычисления сквозной схемы при некоторой свободной интерпретации, то для всякого г, 1 < г < п, найдется такое ), 1 < ] < тп, , что терм <7; является подтермом терма Ту Второе условие требует, чтобы во всех вычислениях сквозных схем при свободных интерпретациях предикаты проверялись только на наборах попарно различных термов. Лля сквозных схем в третьей главе диссертационной работы построен алгоритм распознавания функциональной эквивалентности и полная система преобразований. На этом довольно широком классе сквозных схем продемонстрирован общий подход, разработанный автором для построения полных систем эквивалентных преобразований и алгоритмов распознавания эквивалентности. Главная идея этого подхода состоит в последовательном «сближении» сравниваемых схем за счет направленного применения разработанных автором эквивалентных преобразований. Такой процесс «сближения» проходит через определенные промежуточные контрольные точки, в которых проверяются ключевые условия дальнейшего продвижения по пути «сближения». Ложность ключевых условий влечет неэквивалентность сравниваемых схем. Основные этапы процесса сближения следующие. Первый этап — это этап приведения, или «чистки мусора», на котором удаляются недостижимые конструкции и стандартизуются фрагменты, из которых нет выхода на конец вычислений. На втором этапе происходит выравнивание логической структуры схем, которое реализуется с помощью эквивалентного преобразования «копирование». Применением эквивалентного преобразования вставки неиспользуемых преобразователей мы строим схему, которая содержит в себе не мешающие друг другу вычисления обеих сравниваемых схем. На заключительном этапе применением преобразования замены термов по свойству их равенства мы добиваемся совпадения сравниваемых схем. Условие применимости этого преобразования проверяется с помощью алгоритма разметки для построения инвариантов.

Описанный трансформационный подход сближения сравни-

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

Рост интереса к функциональным, или аппликативным языкам, — в которых в отличие от императивных языков главным примитивом служит не оператор, изменяющий состояние вычислений, а вызов функции, доставляющий результат без каких бы то ни было побочных эффектов, — во многом объясняется тем, что они содержат средства более высокого уровня, нежели императивные языки. В первую очередь это средства рекурсивного определения, которые сегодня широко используются для абстрактной спецификации сложных алгоритмов. Эквивалентные преобразования на уровне таких спецификаций необходимы для получения эффективных программ из обычно весьма неэффективных рекурсивных описаний алгоритмов, а также в системах автоматизации проектирования, анализа, оптимизации и верификации программ. Исследованию отноше^й эквивалентности на моделях рекурсивных программ посвящены работы Д. Маккарти, Э. Ашкроф-та, 3. Манны, А.Пнуели, 3. Галила, С. Гарлэнда и Д. Лахэма, Б.Розена. Проблема эквивалентных преобразований для функциональных программ рассматривалась только для конкретных функциональных языков, таких, как Lisp, Норе, FP, Miranda и др. Языково-независимое преобразование свертки-развертки и связанную с этим преобразованием методологию разработки программ исследовали Р. БерстаЛл и Дж. Дарлингтон. Первой работой, которая положила начало систематическому исследованию проблемы эквивалентных преобразований на схемном уровне, была, по-видимому, работа А.П. Ершова и В.К. Сабель-фельда [1].

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

сание новых преобразований и доказательство их корректности. Мы рассматриваем два класса эквивалентных преобразований рекурсивных схем. Первый содержит преобразования, которые сохраняют введенную Б.Розеном древесную эквивалентность. Это отношение сильнее функциональной эквивалентности. Неформально, две рекурсивные схемы древесно эквивалентны, если они имеют «почти идентичные» деревья развертки.

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

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

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

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

Функция / : L —► L называется монотонной, если Vx,j/ei (*< у =*/(*)< Яг/)); дистрибутивной, если

v*,yei f(xny) = f(x)nf{y).

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

1. конечный граф Г = (V, Е, Ф),

2. окружение для анализа (L, П,Г),

3. разметка Ца : Е —* L (начальная разметка),

4. частичное отображение / : ЕхЕ —► F — семантическая функция разметки, — которая определена для всякой пары (е', е) смежных дуг из Е и сопоставляет этой паре некоторую монотонную функцию из F. Эту функцию называют преобразователем свойств, соответствующим переходу от е' к е и обозначают .

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

конец) графа Г. Для маршрута «> € марш(е',е) с началом е' и концом е положим

Здесь «¿ь — тождественная функция на Ь, Ух £ Ь «^¿(г) — х, а. через о обозначена операция суперпозиции функций на Ь. Содержательно, функция дш описывает, как преобразуются свойства в результате «прохождения» маршрута т, когда известны преобразователи свойств, соответствующие переходу к смежным дугам.

Наконец, для дуг е £ Е определим

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

Задача потокового анализа графа Г в заданном окружении (L,n,F), при заданных начальной разметке fio и семантической функции / состоит в нахождении свойств #(е) для всех дуг е графа Г.

Доказана алгоритмическая неразрешимость этой задачи в общей постановке (теорема 1.3). Описан алгоритм разметки, строящий безопасное приближенное решение задачи анализа (теорема 1.1), которое оказывается точным решением для случая, когда все преобразователи свойств дистрибутивны (теорема 1.4).

В разделе 1.2 описаны постановка и решение задач прямого и обратного анализа семантических свойств рекурсивных фрагментов. Вводится модель рекурсивных программ, называемая рекурсивными схемами и рекурсивными фрагментами. Описанный и исследуемый здесь (и в четвертой главе диссертации) класс рекурсивных схем 7Z шире класса тех рекурсивных схем, что известны и использовались в литературе, начиная с классических работ деБаккера, С.Гарлэнда и Д.Лахэма. Например,

если маршрут и> состоит из одной дуги е, если Зш' 6 марш(е', е") го = т'е, где е", е — смежные дуги

#ео = П П

«'€£ и/£марш(е',е)

рассмотренные Б.Розеном рекурсивные схемы (мы называем их здесь схемами Розена) содержат только такие базисные символы /, на интерпретации которых накладывается единственное ограничение /(/)(!., ..., Л) = X (т.е. результат вычисления не определен, если не определены все аргументы). Ограничения на интерпретации базисных символов для класса рекурсивных схем, исследованного в работах [3, 4, 5, 25], можно описать как ЭМсЦН) = {{1,2}, {1,3}} (т.е. результат вычисления условного терма не определен, если не определено условие или обе альтернативы), и 5<п'с<(/) = {{1,2,..., г(/)}} (т.е. результат вычисления не определен, если не определено значение хотя бы одного аргумента) для всех остальных базисных символов /, отличных от Н^. В схемах введенного и исследованного в диссертационной работе класса 71 рекурсивных схем более тонкие ограничения на возможные интерпретации базисного символа задаются самой схемой за счет фиксации (произвольного) множества «строгих наборов параметров» этого символа. Это множество фиксирует все комбинации неопределенных значений аргументов, при которых интерпретация базисного символа должна быть не определена. Однако, как доказано в последней главе диссертационной работы, статус проблем древесной и функциональной эквивалентности для схем из 72. остается таким же, что и для'схем Розёна.

Те результаты, которые были получены для потокового анализа моделей императивных программ, к рекурсивным программам оказываются во многих случаях неприложимыми по той причине, что вычисления рекурсивных программ соответствуют не всевозможным путям в каком-то графе, а скорее всевозможным деревьям, получающимся последовательным раскрытием встречающихся в программе вызовов. Кроме того, поскольку (рекурсивная) процедура представляет собой правило получения значения по произвольному набору параметров, нас обычно интересуют здесь свойства «второго порядка»: свойством терма оказывается функция, которая по свойствам переменных-параметров дает свойство результата вычисления этого терма. В 1.2 описаны понятия интерпретации и детерминанта рекурсивной схемы 5 как предела последовательности термов приближений детерминанта /(5г"е):

¿е<(5) = 1иЬ{У(ппе) : п > 0}),

где е — главный терм схемы — универсальная интерпретация, а отображение х : Т —» Т соответствует правилу «параллельного вычисления самых внешних вызовов» :

если терм I — переменная; если < = /(<!,...,<„),где / — базисный символ если * = .. .,*„), и Р(жь...,а;„) •<= г — определение символа .Р в 5,

7г°< = тг" = для п > 0. Всякое вхождение подтерма в

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

/ Гх{х, у) <= И(рх, Р2(/х, /у), х) \

50 = { ^(А, Л) ; _Г2(г, у) <= 1£(ру, ^(/у, /*), у) } \ Я»(ж) «^(раг.Ж/*),*) /

первЪе вхождение терма /аг имеет адрес а последнее

вхождение переменной х — адрес (Т^.З.

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

» Адрес терма-детерминанта является образом адреса главного терма схемы.

• Образом адреса вхождения подтерма является адрес вхождения подтерма в терм по адресу-образу.

• Всякий образ адреса вызова является также образом адреса тела.

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

тг«

, 1п/хп]т,

Множество образов адреса может быть и пустым. Например, для схемы

{Fi(u,v);Fi(x,y) <= f(x,Fi(gx,gy)),F2(x) «= f(x))

имеем /ma(?e([F2)) = 0, поскольку ни один из термов ir"F(u,v) не содержит вызовов символа fy, кроме того, Image([F{\.2.2) — 0, поскольку второй параметр символа F\ является «несущественным».

Аналогично определяется множество образов 1таде(а) адреса а и для рекурсивных фрагментов. Пусть задана верхняя полурешетка L с дном X и бинарной операцией U, называемой обгединением, для которой порядок С на элементах определяется соотношениями

djn

ztZy = xU у = у, х С у 1= (х С у) к (х ф у).

Предположим, что фиксированы фрагмент б, полурешетка свойств Ь и семантическая функция наследования свойств со-

поставляющая каждому базисному символу / и натуральному г (1 < г < г(/)) некоторый монотонный преобразователь свойств 5етЦ/, ¿) : Ь —* £, который определяет свойство подтерма терма /(<1,...,<п) с заданным свойством « € Ь как 5ет^(/,|)(«). Пусть, кроме того, фиксирован элемент Л0 полурешетки Ь, называемый начальным свойством. Тогда свойство адреса а в детерминанте ¿е<(С?) для фрагмента в определяется как

{/»о, если а — адрес входа в О,

$етЦ/,г)(^(Ь)), если 3» а = Ь.г и 1/Ь = /(Ь.....гп)

для базисного символа /.

Будем говорить, что сформулирована задача прямого семантического анализа рекурсивного фрагмента С, если фиксированы

• Полурешетка свойств Ь, удовлетворяющая условию обрыва цепей.

• Начальное свойство Ло-

• Семантическая функция Sem*, которая каждому базисному символу / и всякому натуральному i(l < i < г(/)) сопоставляет некоторый монотонный преобразователь свойств Sem*(/,i) -.L—*L.

Задача прямого семантического анализа рекурсивного фрагмента G состоит в определении свойства

Я*(а) = У

для каждого из адресов а фрагмента G.

Сформулируем задачу обратного семантического анализа рекурсивного фрагмента G. Пусть фиксирована полурешетка свойств L и семантическая функция синтеза свойств Sem*, сопоставляющая каждому базисному символу / некоторый монотонный преобразователь свойств Sem* : L" —* L,n = r(f), который определяет свойство терма /(¿ъ-■•>*«) по свойствам s„ его подтермов ti, ...,tn€ L как 5em^(/)(«i,...,s„). Пусть Var(a) для адреса а фрагмента G означает множество переменных тела символа F, если а — адрес подтерма в этом теле, или множество переменных всех входов фрагмента G, если а — адрес подтерма одного из входов. Через Prt обозначим функцию-проекцию Рг,- 6 (£" —* L), для которой Pr,(si,... ,s„) — Si-

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

' Рп, если t — Xi,

5emr(/)(sj.....sn), если t = /(¿i,.. -, tn), n = r(/),

для базисного символа /, и V« Si = Sem'(ti).

Тогда для каждого адреса а фрагмента G можно определить свойство Л*(а,п) п-го приближения детерминанта как элемент полурешетки llVar(a)i —► L следующим образом:

tf{a,n) = Sem*{J{irnGfa)).

Sem*(t) = <

Задача обратного семантического анализа рекурсивного фрагмента <? для заданных полурешетки свойств Ь и семантической функции 5ет^ состоит в нахождении свойства

оо

п=0

для каждого из адресов а фрагмента в.

В 1.2 доказана алгоритмическая неразрешимость задачи обратного семантического анализа рекурсивных фрагментов в общей постановке (теорема 1.7). Построены алгоритмы разметки для приближенного решения задач прямого и обратного семантического анализа свойств рекурсивного фрагмента (теоремы 1.5 и 1.8), получены достаточные условия для того, чтобы можно было эффективно строить точное решение этих задач (теоремы 1.6 и 1.9). Материал главы излагается по публикациям [7, 18].

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

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

• Кроме соотношений равенства термов вида

переменная = функциональный терм

в инвариантах появляются предикатные утверждения вида

значение истинности = предикатный терм.

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

• Множество инвариантных утверждений пополняется за счет учета некоторых свойств возможных интерпретаций встречающихся в схеме операций. Учитываются свойства, которые задаются в форме системы правил переписывания термов, например, х + у-*у + х, х&х-*х.

Система переписывания термов, описывающая свойства интерпретаций символов, порождает отношение редукции сетей, которое оказывается конфлюентным, (теорема 2.5), т.е.

V«, в!, в2 £ $ (в —» «1 & В г» «2 Звз Е 5 => 51 —» «з & «2 —♦ ^з)-

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

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

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

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

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

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

на правдоподобие, доставляющий предупреждающие сообщения о подозрительности конкретных использований языковых средств, призван привлечь внимание разработчика к таким подозрительным участкам программы и помочь в ее отладке. Материал главы излагается по публикациям [б, 9, 10, 12, 11, 18, 22].

В третьей главе после определения класса сквозных схем описывается система Ескв правил преобразования стандартных схем, которые порождаются следующими схемами правил: ЛТ1: удаление недостижимых, ЛТ2: стягивание тупиков, ЛТЗ: копирование, или склеивание копий, ЛТ4: замена переменных, ЛТ5: удаление неиспользуемых преобразователен, ЛТб: удаление неиспользуемого результата входа, ЛТ7: удаление вырожденной пересылки, ЛТ8: замена термов, Ф1: удаление избыточного теста, Ф2:удаление несущественного распознавателя,

Каждая из этих схем правил порождает некоторое рекурсивное множество правил. Условие применимости схемы правил содержит обычно некоторое нелокальное, но вычислимое свойство, которое выявляется с помощью алгоритма разметки. Первые восемь схем правил порождают правила преобразований, сохраняющих логико-термальную эквивалентность, а последние две — более слабую функциональную эквивалентность. В теореме 3.3 показано, как произвольную сквозную схему преобразовать в эквивалентную свободную схему. Построен алгоритм распознавания функциональной эквивалентности сквозных схем и доказана его корректность (теоремы 3.4, 3.5 и 3.6). Доказана теорема 3.7 о полноте системы эквивалентных преобразований £еКа для отношения функциональной эквивалентности сквозных схем. Материал главы излагается по публикациям [14, 17, 18].

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

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

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

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

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

Для программ языка АЬ мы описываем также метод обнаружения несущественных программных конструкций. Удаление таких конструкций из текста программы не меняет ее смысла. Поэтому наличие несущественных конструкций в программе может рассматриваться как аномалия, свидетельствующая о возможной программной ошибке. Материал главы излагается по публикациям [1, 2, 3, 4, 5, 15, 19, 20, 23, 24, 25, 26].

ЗАКЛЮЧЕНИЕ

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

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

2. Разработан новый подход к проблеме приближенного вычисления инвариантов частично интерпретированных стандартных схем. В рамках этого подхода построены алгоритмы вычисления аппроксимаций инвариантов, учитывающие свойства возможных интерпретаций встречающихся в схеме операций. Такие свойства задаются в форме систем правил переписывания термов, например, х + 0—*-х, х + ж—>2х. Кроме того, при приближенном вычислении инвариантов выявляются инвариантные предикатные утверждения вида зна-чение.истинности^тперм, и исключаются из рассмотрения некоторые заведомо недопустимые (т.е. нереализуемые) пути.

3. Спроектирован и (совместно с аспирантом Новосибирского университета П.Г.Емельяновым) реализован анализатор семантических свойств Модула-программ, основанный на разработанных в диссертационной работе алгоритмах разметки для семантического анализа свойств программ. Анализатор помогает программисту при отладке его программ за счет выявления явных семантических ошибок и подозрительных мест программы, а также за счет выявления инвариантных соотношений и других свойств вычислений в интересующих программиста точках программы.

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

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

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

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

7. Описан подход к проблеме обнаружения семантических ошибок в аппликативных спецификациях на языке АЬ, основанный на идеях семантического анализа свойств аппликативных программ с частично определенными операциями и средствами задания недетерминизма. Сформулирована аппроксимаци-онная семантика аппликативных программ, которая эффективно вычислима и надежна в том смысле, что она не противоречит исходной денотационной семантике программ, хотя и

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

Основные публикации по теме диссертации

[1] Ершов А.П., Сабельфельд В.К. Очерк схемной теории рекурсивных программ// Трансляция и модели программ. — Новосибирск, 1980. — С. 23-53.

[2] Sabelfeld V.K. Tree equivalence of linear recursive schemata is polynomial-time decidable// Information Processing Letters. — 1981. — Vol. 13. — №4. — P. 147153.

[3] Сабельфельд В.К, Эквивалентные преобразования рекурсивных схем программ// Оптимизация и преобразования программ. Ч. 1. — Новосибирск, 1983. — С. 48-55.

[4] Сабельфельд В.К. О древесной эквивалентности рекурсивных схем программ// Трансляция и оптимизация программ. — Новосибирск, 1983. — С. 122-136.

[5] Сабельфельд В.К. О проблеме древесной пустоты для рекурсивных схем программ// Проблемы системного и теоретического программирования. — Новосибирск, 1984. — С. 157-166.

[6] Сабельфельд В.К. Учет свойств операций при глобальном анализе свойств программ//Математическая Теория программирования. — Новосибирск, 1985. — С. 132-149.

[7] Сабельфельд В.К. Метод разметки для глобального анализа свойств. — Новосибирск, 1986. — 20 С. — (Препр./АН СССР. Сиб. отд-ние. ВЦ; №699).

[8] Sabelfeld V.K. Program Flow Analysis: Accounting Operation Properties. — LITP Preprint №86-30. — Universite Paris 7, 1986. — 26 P.

[9] Сабельфельд В.К. Как учитывать свойства операций при глобальном анализе программ?// Прикладная логика (Вычислительные системы). — Новосибирск, 1986. — Вып. 116. — С. 33-46.

[10] Sabelfeld V.K. How to take into account the properties of operations in program flow analysis. — Proc. of the IFIP Conference on Program Specification and Transformations, North-Holland, 1987. — P. 151-163.

[11] Касьянов B.H. Сабельфельд B.K. Инструментальные средства преобразования программ. — Новосибирск, 1987. — 22 С. — (Препр./АН СССР. Сиб. отд-ние. ВЦ; №765).

[12] Сабельфельд В.К., Черноброд J1.B. Об одном подходе к анализу свойств программ// Программирование. — 1987. — №4. — С. 21-34.

[13] Сабельфельд В.К. Разработка программ с помощью преобразования// Информатика: Технологические аспекты. — Новосибирск, 1987. — С. 115125.

[14] Сабельфельд В.К. Новый класс схем с разрешимой функциональной екви-валентностью// Информатика: инструментальные средства. — Новосибирск, 1988. — С. 109-126.

[15] Kasyanov V.N., Sabelfeld V.K. Took for Program Transformation// Methods of Compilation and Program Construction. — INRIA 1988. — P. 89-99.

[16] Сабельфельд В.К. Потоковый анализ и эквивалентные преобразования программ// Теоретические проблемы систем обработки информации. — Новосибирск, 1990. — С. 5-23.

[17] Sabelfeld V.K. An algorithm deciding functional equivalence in a new class of program schemes// Theoretical Comput. Sci. — 1990. — Vol. 71. — P. 265-279.

[18] Котов В.E., Сабельфельд В.К. Теория схем программ. — М.:, Наука, 1991. — 246 С.

[19] Сабельфельд В.К. Трансформации для рекурсивных схем программ// Смешанные вычисления и преобразование программ. — Новосибирск, 1991. — С. 99-111.

[20] Sabelfeld V.K. Equivalent Transformations for Recursion Schemes// Current Topics in Informatics Systems Research. — Novosibirsk, 1991. — P. 61-72.

[21] Sabelfeld V.K. On Equivalent Transformations for Recursion Schemes// Theoretical Computer Science and Methods of Compilation and Program Construction. — INRIA 1991. — P. 295-312.

[22] Брюхаиова Ю.В., Емельянов П.Г., Касьянов В.Н., Сабельфельд В.К. Методы и средства семантического анализа Модула-программ// Конструирование и оптимизация программ. — Новосибирск, 1993. — С. 7—23.

[23] Сабельфельд В.К. Анализ некоторых семантических свойств программ аппликативного языка AL// Программирование, 1993. —№6. — С. 6-15.

[24] Kasyanov V.N., Kuzminov T.V., Pokrovsky S.B., Pottosin I.V., Sabelfeld V.K., Shelekhov V.I., Stepanov G.G., Zakharov L.I. SOKRAT: An environment for safe and efficient programming. — International Congress on Сотр. Syst. and Applied Math. (CSAM'93), Abstracts, St.Peterburg, 1993, p. 177-178.

[25] Sabelfeld V.K. Equivalent Transformations of Recursion Schemes and Admissible Rewriting Rules//Novosibirsk, 1993. — 20 P. — (Prepr./ISI SD RAS; №20).

[26] Sabelfeld V.K. Analysis of some semantic properties for programs of the applicative language AL// Lect. Notes in Comput. Sci. — 1993. — Vol. 735. — P. 181-189.