'

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

Понравилась презентация – покажи это...





Слайд 0

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


Слайд 1

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


Слайд 2

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


Слайд 3

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


Слайд 4

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


Слайд 5

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


Слайд 6

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


Слайд 7

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


Слайд 8

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


Слайд 9

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


Слайд 10

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


Слайд 11

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


Слайд 12

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


Слайд 13

Литература 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 с. 9.05.2009 14


×

HTML:





Ссылка: