Синтез программы
-
Обзор методов синтеза программ
- Синтез программ — это процесс создания компьютерных программ из спецификаций.
- Методы синтеза программ включают индуктивное программирование, метапрограммирование и другие.
-
Индуктивное программирование
- Индуктивное программирование основано на доказательстве теорем и создании программ из них.
- Примеры включают доказательство теорем о числах и создание программ для вычисления математических функций.
-
Метапрограммирование
- Метапрограммирование позволяет создавать программы, которые генерируют другие программы.
- Примеры включают создание программ для генерации кода на различных языках программирования.
-
Синтез, основанный на синтаксисе
- SyGuS — унифицированная структура для задач синтеза программ, основанная на синтаксисе.
- Алгоритмы SyGuS сравнивались на ежегодном конкурсе с 2014 по 2019 год.
-
Концепция Манны и Вальдингера
- Основана на формуле спецификации первого порядка, которая преобразуется в программу.
- Гарантирует, что программы удовлетворяют исходной спецификации.
- Поддерживает функциональный язык программирования с условными и рекурсивными операторами.
-
Тематические исследования
- Примеры включают алгоритмы для различных математических операций и запросов к базам данных.
-
Правила доказательства
- Включают неклаузальное разрешение, логические преобразования и другие.
- Мюррей показал, что правила являются полными для логики первого порядка.
-
Пример синтеза программы
- Демонстрирует процесс синтеза программы для вычисления максимального значения из двух чисел.
Полный текст статьи: