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

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

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

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

Метод дедуктивных таблиц - 2 УтвержденияЦелиВыходной терм f1(x)…fn(x) A1A1 t1t1 tntn ……… AkAk t 1 t n G1G1 s1s1 snsn ……… GmGm s 1 s n

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

Вспомогательные таблицы - 2 Исходная цель получаемая лемма имеющаяся в основной таблице строка (i) их резолюция завершает доказательство k+1G 1 (y, fnew(y)) iG[t[a],x]r[a,x] k+2truer''[a,fnew(t[a])] 1aG'[c,x]x

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

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

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

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

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

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

Литература Manna Z., Waldinger R. Fundamentals of Deductive Synthesis // Transactions on software engineering P Ayari A., Basin D. A High-Order Interpretation of Deductive Tableau // Journal of Symbolic Computation P 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 P Averin A., Vagin V. The Development of Parallel Resolution Algorithms Using the Graph Representation // International Journal Information Theories & Applications P Traugott J. Deductive Synthesis of Sorting Programs // Journal of Symbolic Computation P Большакова Е.И., Мальковский М.Г. Автоматический Синтез Программ. М.: Издательство Московского универсистета с. Flener P. Achievements and Prospects of Program Synthesis // Computational Logic: Logic Programming and Beyond. Heidelberg: Spriger Berlin, P Стюарт Рассел (Stuart J. Russel), Питер Норвиг (Peter Norvig) Искуственный интеллект: современный подход, 2-е издание. Перевод с английского М.: Издательский дом «Вильямс» с