|
ИСТИНА |
Войти в систему Регистрация |
ФНКЦ РР |
||
Дедуктивный синтез программ с использованием волновых правилстатья
- Автор: Корухова Ю.С.
- Сборник: Программные системы и инструменты. Тематический сборник
- Серия: Программные системы и инструменты
- Том: 6
- Год издания: 2005
- Место издания: Издательский отдел ВМК МГУ М
- Первая страница: 6
- Последняя страница: 16
- Аннотация: В работе рассматривается синтез функциональных программ с помощью метода дедуктивных таблиц. При таком подходе формальная спецификация программы рассматривается как теорема существования, из конструктивного доказательства которой извлекается требуемая программа. Применение метода дедуктивных таблиц в "чистом" виде ведет к большому перебору, что делает его практическое использование невозможным. Для сокращения перебора предлагается использовать т. н. волновые правила, применяющиеся при доказательстве по индукции, которое возникает при построении рекурсивных программ. С помощью волновых правил строится план доказательства, которое затем проводится в дедуктивной таблице одновременно с синтезом рекурсивной ветви функции. Данный подход был реализован автором в системе автоматического синтеза программ АЛИСА.
- Добавил в систему: Корухова Юлия Станиславовна