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

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

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

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

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

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

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

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

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

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

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

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

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