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

Работа с статьей


[1] Корухова Ю. С. Дедуктивный синтез программ с использованием волновых правил // Программные системы и инструменты. Тематический сборник. — Т. 6 из Программные системы и инструменты. — Издательский отдел ВМК МГУ М, 2005. — С. 6–16. В работе рассматривается синтез функциональных программ с помощью метода дедуктивных таблиц. При таком подходе формальная спецификация программы рассматривается как теорема существования, из конструктивного доказательства которой извлекается требуемая программа. Применение метода дедуктивных таблиц в "чистом" виде ведет к большому перебору, что делает его практическое использование невозможным. Для сокращения перебора предлагается использовать т. н. волновые правила, применяющиеся при доказательстве по индукции, которое возникает при построении рекурсивных программ. С помощью волновых правил строится план доказательства, которое затем проводится в дедуктивной таблице одновременно с синтезом рекурсивной ветви функции. Данный подход был реализован автором в системе автоматического синтеза программ АЛИСА.

Публикация в формате сохранить в файл сохранить в файл сохранить в файл сохранить в файл сохранить в файл сохранить в файл скрыть