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

• Автор: Харф, Майт Якобович
• Шифр специальности: 01.01.10
• Научная степень: Кандидатская
• Год защиты: 1984
• Место защиты: Таллин
• Количество страниц: 122 c. : ил

ГЛАВА I. ОБЗОР МЕТОДОВ СИНТЕЗА ПРОГРАММ

1.1. Дедуктивный подход к синтезу

1.2. Индуктивный подход к синтезу

1.3. Трансформационный подход к синтезу

1.'4. Автоматический синтез в пакетах прикладных

программ

ГЛАВА II. МЕТОД СТРУКТУРНОГО СИНТЕЗА ПРОГРАММ

2.1. Язык условий задач

2.2. Вычислимость объектов

2.3. Форма аксиом

2.4. Правила вывода

2.5. Язык программ
2.6. Синтез программ линейной структуры
2.6.1. Построение доказательства теоремы
2.6.2. Алгоритм построения доказательства
2.6.3. Оценка сложности
2.7. Синтез ветвящихся программ
2.7.1. Алгоритм построения доказательства
2.7.2. Оценка сложности
2.8. Синтез црограмм с подпрограммами (первый способ)
2.8.1. Алгоритм построения доказательства
2.8.2. Оценка сложности
2.9. Синтез программ с подпрограммами (второй способ)

2.9.1. Оценка сложности
2.10. Заключение
ГЛАВА III. ОПТИМИЗАЦИЯ АВТОМАТИЧЕСКИ СИНТЕЗИРУЕМЫХ
ПРОГРАММ
3.1. Минимизация синтезируемых линейных участков программ
3.2. Минимизация ветвящихся программ
3.3. Минимизация программ с подпрограммами
3.4. Оптимальное распределение памяти, занимаемой данными синтезируемой црограммы
3.5. Заключение
ГЛАВА ІУ. РЕАЛИЗАЦИЯ СИНТЕЗАТОРА ПРОГРАММ
4.1. Место синтезатора программ в системе программирования ПРИЗ
4.1.1. Общая структура системы ПРИЗ
4.1.2. Общая структура генератора программ
4.2. Общая структура синтезатора
4.3. Представление условий задачи
4.3.1. Общие принципы представления условий задачи
4.3.2. Представление модели задачи
4.3.3. Представление оператора задачи
4.4. Представление синтезируемой программы
4.5. Реализация основных алгоритмов синтезатора
4.5.1. Реализация алгоритма синтеза линейных участков программ
4.5.2. Синтез црограмм, содержащих ветвления
и подпрограммы
4.5.3. Реализация алгоритма минимизации синтезируемых линейных участков программ

4.5,4. Реализация алгоритма минимизации
синтезируемых црограмм, содержащих ветвления и подцрограммы
4.6. Внутренний язык синтезатора
4.6.1. Внутримашинное представление структур данных
4.6.2. Средства работы со структурами данных
4.6.3. Машинная реализация внутреннего языка
4.7. Заключение
ЗАКЛЮЧЕНИЕ
ЛИТЕРАТУРА
ПРИЛОЖЕНИЯ

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