Главная страница « Научно-исследовательский семинар «

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

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

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

Приглашаются аспиранты и стажеры программистских кафедр.