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

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

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

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

Дедуктивные таблицы (2) Структура дедуктивной таблицы If(A 1 … A n ) then (G 1 … G m ) Утверждения ЦелиВыходной терм f1(x)…fn(x) A1A1 t1t1 tntn ……… AkAk t 1 t n G1G1 s1s1 snsn ……… GmGm s 1 s n Синтез функциональных программ при помощи метода дедуктивных таблиц

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

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

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

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

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

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

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

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

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

Дедуктивные правила (3) Правило резолюции G1,G2 – логические выражения, P, P – некоторые подвыражения G1 и G2, λ – подстановка, для которой P λ = Pλ, s и t – выходные термы Синтез функциональных программ при помощи метода дедуктивных таблиц 15 i G1[P]t k G2[P]s r G1 λ [true] G2λ [false] If P λ then s λ else t λ

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

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

Пример синтеза функциональной программы (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 Синтез функциональных программ при помощи метода дедуктивных таблиц 18 1 (n=0) (z=1) ¬ (n=0) (z=n*fact(n-1)) z

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

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

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

Вспомогательные таблицы (3) Исходная цель Гипотеза индукции Воспроизведение шагов доказательства Резолюция с гипотезой индукции Синтез функциональных программ при помощи метода дедуктивных таблиц 22 1aG'[c,x]x 2aif y

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

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

Пример вывода вспомогательной таблицы (2) В ходе доказательства получается строка Далее, строка Синтез функциональных программ при помощи метода дедуктивных таблиц perm(tail(b), w^x) perm(tail(b), x2^w) perm(tail(b), x3^x) [if iselem(f, x) then head(b) f] [if iselem(h, w) then h head(b)] if b=null then null else sort(w)^ head(b)*sort(x) 30 perm(tail(tail(b)), w^y) perm(tail(tail(b)), v2^w) perm(tail(tail(b)), x3^y) [if f = head(tail(b)) then head(b) f] [if iselem(f, y) then head(b) f] [if iselem(h, w) then h head(b)] ¬tail(b)=null t (30)

Исходная цель вспомогательной таблицы Лемма Синтез функциональных программ при помощи метода дедуктивных таблиц 26 #AssertionGoalf1f2 1a1a perm(с, w^x) perm(с, x2^w) perm(с, x3^x) [if iselem(f, x) then head(b) f] [if iselem(h, w) then h head(b)] wx 3131 perm(y, les(y)^gre(y)) perm(y, x2^les(y)) perm(y, x3^gre(y)) [if iselem(f, gre(y)) then head(b) f] [if iselem(h, les(y)) then h head(b)]

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

Источники Kreitz, C. Program Synthesis Chapter III.2.5 of Automated Deduction – A Basis for Applications, pp. 105–134, Kluwer, 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, Синтез функциональных программ при помощи метода дедуктивных таблиц 28