'

Синтез функциональных программ при помощи метода дедуктивных таблиц.

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





Слайд 0

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


Слайд 1

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


Слайд 2

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


Слайд 3

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


Слайд 4

Дедуктивные таблицы (2) Структура дедуктивной таблицы If(A1 ? … ? An) then (G1 ? … ? Gm) 15.02.2009 5 Синтез функциональных программ при помощи метода дедуктивных таблиц


Слайд 5

Дедуктивные таблицы (3) Терм t, не содержащий свободных (на связанных с квантором) переменных, удовлетворяет строке таблицы или если для некоторой подстановки ?: Утверждение A? не содержит свободных переменных и является ложным (G? – истинным) Если строка имеет выходной терм s, то s? не содержит свободных переменных и равен t?. 15.02.2009 6 Синтез функциональных программ при помощи метода дедуктивных таблиц


Слайд 6

Дедуктивные таблицы (4) Доказательство в дедуктивной таблице проводиться до получения финальной строки или 15.02.2009 7 Синтез функциональных программ при помощи метода дедуктивных таблиц


Слайд 7

Свойства дедуктивных таблиц (1) Двойственность строка эквивалентна строке 15.02.2009 8 Синтез функциональных программ при помощи метода дедуктивных таблиц


Слайд 8

Свойства дедуктивных таблиц (2) Переименование свободных переменных ? – перестановка строка эквивалентна строке 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 9


Слайд 9

Свойства дедуктивных таблиц (3) Добавление примера ? – подстановка Таблица эквивалентна 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 10


Слайд 10

Свойства дедуктивных таблиц (4) Тождественные преобразования Эквивалентность таблиц не нарушается при применении в строках тождественных преобразований на основе тождеств алгебры логики: A ? A = A; A ? false = false; A ? true = true; ¬ ¬ A = A; 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 11


Слайд 11

Свойства дедуктивных таблиц (5) Добавление и удаление тождественно истинного утверждения и тождественно ложной цели Добавление и удаление свободной переменной 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 12


Слайд 12

Дедуктивные правила (1) Вычислимые термы – термы, не содержащие свободных переменных, которые можно получить на основе уже определенных констант, функций и предикатов. Таблицы, для которых совпадают множества удовлетворяющих им вычислимых термов термов совпадают, называются подобными. 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 13


Слайд 13

Дедуктивные правила (2) Правило OR- и AND-разделения G1,G2,A1,A2 – логические выражения, t – выходной терм. 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 14


Слайд 14

Дедуктивные правила (3) Правило резолюции G1,G2 – логические выражения, P, P’ – некоторые подвыражения G1 и G2, ? – подстановка, для которой P? = P’?, s и t – выходные термы. 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 15


Слайд 15

Дедуктивные правила (4) Правило индукции. wf-отношение – отношение, исключающее бесконечно убывающие цепочки. Спецификация: где a – входной параметр, z – выходная переменная, Q – логическая формула. Гипотеза индукции: где <wf – wf-отношение в рассматриваемой теории 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 16


Слайд 16

Дедуктивные правила (5) Правило замены эквивалентных термов где G1, G2 – логические выражения, [L=R] – подвыражение G1, T – некоторый терм, входящий в G2, такой что для некоторой подстановки ?:T? = L?, s и t – выходные термы. 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 17


Слайд 17

Пример синтеза функциональной программы (1) Спецификация: z = fact(n) is if n = 0 then z = 1 else z = n*fact(n-1) В таблице согласно тождеству if A then B else C ? A ? B ? ¬A ? C 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 18


Слайд 18

Пример синтеза функциональной программы (2) OR-разделение Резолюция. Общее подвыражение . (n=0). Добавление примера{z1<1,z2 < n*fact(n-1) } 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 19


Слайд 19

Вспомогательные таблицы (1) Пусть в таблице присутствуют строки где G, F – логические выражения, a – входной параметр, t[a], t’[a] – термы над входным параметром, x, x’ – выходные переменная, r[a,x], r’[a,x’] – выходные термы. F содержит реплику G. 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 20


Слайд 20

Вспомогательные таблицы (2) Если t’[a] <wf t[a], можно в выражении G заменить все вхождения t[a] на произвольную константу и построить обобщенную цель G’[c,x], которая станет исходной целью для вспомогательной таблицы (соответственно – спецификацией для вспомогательных функций). 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 21


Слайд 21

Вспомогательные таблицы (3) Исходная цель Гипотеза индукции Воспроизведение шагов доказательства Резолюция с гипотезой индукции 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 22


Слайд 22

Вспомогательные таблицы (4) 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 23 Лемма имеющаяся строка (i) их резолюция завершает доказательство


Слайд 23

Пример вывода вспомогательной таблицы (1) Для функции сортировки списка чисел задается спецификация вида z = sort(a) is perm(a,z) ? ord(z) perm(x,y) – предикат, равный true, если его аргументы-списки есть перемтановки друг-друга. ord(x) – предикат, равный true, если его аргумент-список упорядочен. 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 24


Слайд 24

Пример вывода вспомогательной таблицы (2) В ходе доказательства получается строка Далее, строка 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 25


Слайд 25

Исходная цель вспомогательной таблицы Лемма 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 26


Слайд 26

Конец 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 27


Слайд 27

Источники Источники Kreitz, C. Program Synthesis Chapter III.2.5 of Automated Deduction – A Basis for Applications, pp. 105–134, Kluwer, 1998. Ayari, A., Basin D.: A High-Order Interpretation Of Deductive Tableau J. Symbolic Computation (2001) 11, 1-32 Manna Z., Waldinger R.: Fundamentals of Deductive Program Synthesis IEEE Transactions on Software Engineering, vol. 12, No. 8, August 1992 Traugott J. Deductive Synthesis of Sorting Programs Journal of Symbolic Computation, vol.7, 1989. 15.02.2009 Синтез функциональных программ при помощи метода дедуктивных таблиц 28


×

HTML:





Ссылка: