🗊Использование возможностей параллельных вычислений в синтезе функциональных программ. Подготовил: Фастовец Н.Н. Научный руково

Использование возможностей параллельных вычислений в синтезе функциональных программ. Подготовил: Фастовец Н.Н. Научный руководитель: Ассистент, к.ф-м.н. Корухова Ю.С.

Содержание Автоматический синтез программ Метод дедуктивных таблиц Вспомогательные таблицы Параллельный вывод вспомогательных функций Параллельный управляемый и автоматический синтез Заключение

Автоматический синтез программ Предпосылки: Возрастание сложности ПО Возрастание требований к надежности ПО Три подхода: Индуктивный Дедуктивный Трансформационный

Метод дедуктивных таблиц - 1 Спецификация программы в виде логической формулы: ∀x ∃y Q[x,y] где x – входная переменная, y – выходная переменная, Q – логическая формула, устанавливающая связь между входными и выходными переменными.

Метод дедуктивных таблиц - 2

Вспомогательные таблицы - 1 Условие вывода вспомогательной таблицы где G, F – логические выражения, a – входной параметр, t[a], t’[a] – термы над входным параметром, x, x’ – выходные переменная, r[a,x], r’[a,x’] – выходные термы. F содержит реплику G.

Вспомогательные таблицы - 2 Исходная цель получаемая лемма имеющаяся в основной таблице строка (i) их резолюция завершает доказательство

Параллельный вывод вспомогательных функций - 1 Основан на независимости доказательства во вспомогательной таблице Позволяет одновременное проведение двух веток доказательства Устраняет потерю времени, связанную с неверным выбором стратегии доказательства

Параллельный вывод вспомогательных функций - 2

Параллельный управляемый и автоматический синтез - 1 Может ускорить решение конкретной задачи Позволяет совместить преимущества управляемого и автоматического синтеза

Параллельный управляемый и автоматический синтез - 2

Заключение Использование возможностей параллельных вычислений позволяет: Одновременное проведение двух веток доказательства Совмещение управляемого и автоматического синтеза

Спасибо за внимание! Вопросы?

Литература Manna Z., Waldinger R. Fundamentals of Deductive Synthesis // Transactions on software engineering. 1992. 18. № 8. P. 674-704 Ayari A., Basin D. A High-Order Interpretation of Deductive Tableau // Journal of Symbolic Computation. 2001. 11. P. 1-32 Kreitz C. Program Synthesis // Automated Deduction - A Basis for Applications Volume I Foundations - Calculi and Methods Volume II Systems and Implementation Techniques Volume III Applications. Secaucus: Springer. 1998. P. 105-134. Averin A., Vagin V. The Development of Parallel Resolution Algorithms Using the Graph Representation // International Journal “Information Theories & Applications”. 2006. 13. № 2. P 263-271. Traugott J. Deductive Synthesis of Sorting Programs // Journal of Symbolic Computation. 1986. 7. P. 533-571 Большакова Е.И., Мальковский М.Г. Автоматический Синтез Программ. М.: Издательство Московского универсистета. 1987. 114 с. Flener P. Achievements and Prospects of Program Synthesis // Computational Logic: Logic Programming and Beyond. Heidelberg: Spriger Berlin, 2002. P. 1-43 Стюарт Рассел (Stuart J. Russel), Питер Норвиг (Peter Norvig) Искуственный интеллект: современный подход, 2-е издание. Перевод с английского — М.: Издательский дом «Вильямс». 2007. 1408 с.