Программный синтез - Program synthesis

В Информатика, программный синтез это задача построить программа что доказуемо удовлетворяет заданный высокий уровень формальная спецификация. В отличие от проверка программы, программа должна быть построена, а не дана; однако в обеих областях используются формальные методы доказательства, и обе включают подходы разной степени автоматизации. В отличие от автоматическое программирование методы, спецификации в программном синтезе обычно не являютсяалгоритмический заявления в соответствующем логическое исчисление.^[1]

Источник

Во время Летнего института символической логики Корнельского университета в 1957 г. Церковь Алонсо поставил задачу синтезировать схему из математических требований.^[2] Несмотря на то, что работа относится только к схемам, а не к программам, эта работа считается одним из самых ранних описаний синтеза программ, и некоторые исследователи называют синтез программ «проблемой Чёрча». В 1960-х годах аналогичная идея для «автоматического программиста» была изучена исследователями искусственного интеллекта.^{[нужна цитата ]}

С тех пор проблемой синтеза программ стали заниматься различные исследовательские сообщества. Известные работы включают теоретико-автоматный подход 1969 г. Бючи и Ландвебер,^[3] и работы Манна и Waldinger (ок. 1980 г.). Развитие современных языки программирования высокого уровня также можно понимать как форму программного синтеза.

События 21 века

В начале 21 века наблюдается всплеск практического интереса к идее программного синтеза в формальная проверка сообщество и связанные области. Армандо Солар-Лезама показал, что задачи синтеза программ можно кодировать в Логическая логика и использовать алгоритмы для Проблема логической выполнимости для автоматического поиска программ.^[4] В 2013 г. исследователи из г. UPenn, Калифорнийский университет в Беркли, и Массачусетский технологический институт.^[5] С 2014 года проводится ежегодное соревнование по синтаксису программ, в котором сравниваются различные алгоритмы синтеза программ на соревнованиях, соревнование по синтаксическому синтезу или SyGuS-Comp.^[6] Тем не менее, доступные алгоритмы способны синтезировать только небольшие программы.

В документе 2015 года продемонстрирован синтез PHP программы, которые аксиоматически доказаны как соответствующие заданной спецификации, для таких целей, как проверка числа на простое или перечисление множителей числа.^[7]

Каркас Манна и Вальдингера

Правила разрешения без клауза (объединяющие замены не показаны)

№	Утверждения	Цели	Программа	Источник
51	${\displaystyle E[p]}$
52	${\displaystyle F[p]}$
53		${\displaystyle G[p]}$	s
54		${\displaystyle H[p]}$	т
55	${\displaystyle E[{\text{true}}]\lor F[{\text{false}}]}$			Решимость (51,52)
56		${\displaystyle \lnot F[{\text{true}}]\land G[{\text{false}}]}$	s	Решимость (52,53)
57		${\displaystyle \lnot F[{\text{false}}]\land G[{\text{true}}]}$	s	Решимость (53,52)
58		${\displaystyle G[{\text{true}}]\land H[{\text{false}}]}$	п ? s : т	Решимость (53,54)

В рамках Манна и Waldinger, опубликовано в 1980 г.,^[8][9] начинается с заданного пользователем формула спецификации первого порядка. Для этой формулы построено доказательство, тем самым синтезируя функциональная программа из объединение замены.

Фреймворк представлен в виде таблицы, столбцы которой содержат:

• Номер строки («Nr») для справки.
• Формулы которые уже были установлены, включая аксиомы и предварительные условия, («Утверждения»)
• Формулы еще предстоит доказать, включая постусловия, («Цели»),^{[примечание 1]}
• Условия обозначение допустимого выходного значения («Программа»)^{[заметка 2]}
• Обоснование текущей строки («Источник»)

Первоначально в таблицу вводятся базовые знания, предварительные и пост-условия. После этого соответствующие правила проверки применяются вручную. Фреймворк был разработан для повышения удобочитаемости промежуточных формул: в отличие от классическое разрешение, это не требует клаузальная нормальная форма, но позволяет рассуждать формулами произвольной структуры и содержащими любые стыки ("безусловное разрешение "). Доказательство завершено, когда ${\displaystyle {\it {true}}}$ был получен в Цели столбец, или, что то же самое, ${\displaystyle {\it {false}}}$ в Утверждения столбец. Программы, полученные с помощью этого подхода, гарантированно удовлетворяют формуле спецификации, начиная с; в этом смысле они правильный по конструкции.^[10] Только минималист, но Полный по Тьюрингу, функциональный язык программирования, состоящий из условных, рекурсивных, арифметических и других операторов^{[заметка 3]} В рамках этой структуры были синтезированы алгоритмы для вычисления, например, разделение, остаток,^[11] квадратный корень,^[12] объединение терминов,^[13] ответы на реляционная база данных запросы^[14] и несколько алгоритмы сортировки.^[15][16]

Правила доказательства

Правила доказательства включают:

• Неклаузальный разрешающая способность (см. таблицу).

Например, строка 55 получается путем разрешения формул утверждения ${\displaystyle E}$ от 51 и ${\displaystyle F}$ из 52, которые имеют общую подформулу ${\displaystyle p}$. Резольвента образуется как дизъюнкция ${\displaystyle E}$, с ${\displaystyle p}$ заменен на ${\displaystyle {\it {true}}}$, и ${\displaystyle F}$, с ${\displaystyle p}$ заменен на ${\displaystyle {\it {false}}}$. Эта резольвента логически следует из конъюнкции ${\displaystyle E}$ и ${\displaystyle F}$. В более общем смысле, ${\displaystyle E}$ и ${\displaystyle F}$ нужно иметь только две объединяемые подформулы ${\displaystyle p_{1}}$ и ${\displaystyle p_{2}}$, соответственно; их резольвента затем формируется из ${\displaystyle E\theta }$ и ${\displaystyle F\theta }$ как и раньше, где ${\displaystyle \theta }$ это самый общий объединитель из ${\displaystyle p_{1}}$ и ${\displaystyle p_{2}}$. Это правило обобщает разрешение статей.^[17]

Термины программы родительских формул объединяются, как показано в строке 58, для формирования выходных данных резольвенты. В общем случае ${\displaystyle \theta }$ применяется и к последнему. Поскольку подформула ${\displaystyle p}$ появляется в выходных данных, необходимо проявлять осторожность, чтобы разрешить только подформулы, соответствующие вычислимый характеристики.

• Логические преобразования.

Например, ${\displaystyle E\land (F\lor G)}$ можно преобразовать в ${\displaystyle (E\land F)\lor (E\land G)}$) как в утверждениях, так и в целях, поскольку они эквивалентны.

• Разделение конъюнктивных утверждений и дизъюнктивных целей.

Пример показан в строках с 11 по 13 приведенного ниже примера игрушки.

• Структурная индукция.

Это правило позволяет синтезировать рекурсивные функции. Для данного предусловия и постусловия "Данное ${\displaystyle x}$ такой, что ${\displaystyle {\textit {pre}}(x)}$, найти ${\displaystyle f(x)=y}$ такой, что ${\displaystyle {\textit {post}}(x,y)}$", и соответствующий пользовательский хороший порядок ${\displaystyle \prec }$ области ${\displaystyle x}$, всегда разумно добавить утверждение "${\displaystyle x'\prec x\land {\textit {pre}}(x')\implies {\textit {post}}(x',f(x'))}$".^[18] Разрешение этого утверждения может ввести рекурсивный вызов ${\displaystyle f}$ в срок действия Программы.

Пример приведен в Manna, Waldinger (1980), p.108-111, где синтезирован алгоритм вычисления частного и остатка от двух заданных целых чисел с использованием хорошего порядка ${\displaystyle (n',d')\prec (n,d)}$ определяется ${\displaystyle 0\leq n'<n}$ (стр.110).

Мюррей показал, что эти правила полный за логика первого порядка.^[19]В 1986 году Манна и Вальдингер добавили обобщенное E-разрешение и парамодуляция правила для обработки также равенства;^[20] позже эти правила оказались неполными (но тем не менее звук ).^[21]

Пример

Пример синтеза максимальной функции

№	Утверждения	Цели	Программа	Источник
1	${\displaystyle A=A}$			Аксиома
2	${\displaystyle A\leq A}$			Аксиома
3	${\displaystyle A\leq B\lor B\leq A}$			Аксиома
10		${\displaystyle x\leq M\land y\leq M\land (x=M\lor y=M)}$	M	Технические характеристики
11		${\displaystyle (x\leq M\land y\leq M\land x=M)\lor (x\leq M\land y\leq M\land y=M)}$	M	Distr (10)
12		${\displaystyle x\leq M\land y\leq M\land x=M}$	M	С разрезом (11)
13		${\displaystyle x\leq M\land y\leq M\land y=M}$	M	С разрезом (11)
14		${\displaystyle x\leq x\land y\leq x}$	Икс	Решимость (12,1)
15		${\displaystyle y\leq x}$	Икс	Решимость (14,2)
16		${\displaystyle \lnot (x\leq y)}$	Икс	Решимость (15,3)
17		${\displaystyle x\leq y\land y\leq y}$	у	Решимость (13,1)
18		${\displaystyle x\leq y}$	у	Решимость (17,2)
19		${\displaystyle {\textit {true}}}$	х <у ? у : Икс	Решимость (18,16)

В качестве игрушечного примера приведем функциональную программу для вычисления максимальной ${\displaystyle M}$ двух чисел ${\displaystyle x}$ и ${\displaystyle y}$ можно получить следующим образом.^{[нужна цитата ]}

Начиная с описания требования "Максимум больше или равен любому заданному числу и является одним из заданных чисел", формула первого порядка ${\displaystyle \forall X\forall Y\exists M:X\leq M\land Y\leq M\land (X=M\lor Y=M)}$ получается как его формальный перевод. Эта формула требует доказательства. Обратным Сколемизация,^{[примечание 4]} получается спецификация в строке 10, прописные и строчные буквы обозначают переменную и Постоянная Сколема, соответственно.

После применения правила преобразования для распределительный закон в строке 11 цель доказательства - дизъюнкция, и поэтому ее можно разделить на два случая, а именно. строки 12 и 13.

Возвращаясь к первому случаю, разрешив строку 12 с аксиомой в строке 1, мы получим реализация программной переменной ${\displaystyle M}$ в строке 14. Интуитивно последний конъюнкт строки 12 задает значение, которое ${\displaystyle M}$ надо брать в этом случае. Формально правило разрешения отсутствия клауза, показанное в строке 57 выше, применяется к строкам 12 и 1, при этом

• п являясь обычным случаем х = х из А = А и х = М, полученный синтаксически объединение последние формулы,
• F [п] существование истинный ∧ х = х, получен из созданный строка 1 (с соответствующими дополнениями, чтобы контекст F [⋅] вокруг п видимый), и
• ГРАММ[п] существование х ≤ х ∧ у ≤ х ∧ х = х, полученный из созданной строки 12,

уступающий${\displaystyle \lnot (}$истинный ∧ ложный) ∧ (х ≤ х ∧ у ≤ х ∧ истинный${\displaystyle )}$, что упрощает ${\displaystyle x\leq x\land y\leq x}$.

Аналогичным образом строка 14 дает строку 15, а затем строку 16 по разрешению. Также второй случай, ${\displaystyle x\leq M\land y\leq M\land y=M}$ в строке 13 обрабатывается аналогичным образом, в результате получается строка 18.

На последнем этапе оба случая (то есть строки 16 и 18) объединяются с использованием правила разрешения из строки 58; Чтобы применить это правило, был необходим подготовительный шаг 15 → 16. Интуитивно строка 18 может быть прочитана как «на случай, если ${\displaystyle x\leq y}$, выход ${\displaystyle y}$ действительна (относительно исходной спецификации), а в строке 15 написано «в случае ${\displaystyle y\leq x}$, выход ${\displaystyle x}$ действует; на шаге 15 → 16 установлено, что оба случая 16 и 18 дополняют друг друга.^{[примечание 5]} Поскольку в строках 16 и 18 есть срок программы, условное выражение результаты в столбце программы. Поскольку формула цели ${\displaystyle {\textit {true}}}$ выведено, доказательство выполнено, и столбец программы "${\displaystyle {\textit {true}}}$"строка содержит программу.

Эта процедура производит только один оператор вида p? S: t, взятый из строки 58. Это не язык программирования, потому что он не является полным по Тьюрингу. Нет команд, например ASSIGNMENT, IF / ELSE, FOR / WHILE или рекурсивные программы, которые необходимы для создания полного по Тьюрингу языка. Его следует обозначить как таковой: способ создания единого логического оператора, а не способ создания программ в целом. Возможно, можно было бы использовать «Синтез операторов». Метод постройки колеса - это не метод постройки автомобиля.^{[нужна цитата ]}

Смотрите также

• Индуктивное программирование
• Метапрограммирование
• Автоматическое программирование
• Вывод программы
• Программирование на естественном языке
• Реактивный синтез
• Формальная проверка

Примечания

1. Различие «Утверждения» / «Цели» сделано только для удобства; следуя парадигме доказательство от противного, цель ${\displaystyle F}$ эквивалентно утверждению ${\displaystyle \lnot F}$.
2. Когда ${\displaystyle F}$ и ${\displaystyle s}$ - формула цели и термин программы в строке, соответственно, то во всех случаях, когда ${\displaystyle F}$ держит, ${\displaystyle s}$ - допустимый результат синтезируемой программы. Этот инвариантный соблюдается всеми правилами доказательства. Формула утверждения обычно не связана с термином программы.
3. Только условный оператор (?: ) поддерживается с самого начала. Однако можно добавить произвольные новые операторы и отношения, указав их свойства как аксиомы. В приведенном ниже примере игрушки только свойства ${\displaystyle =}$ и ${\displaystyle \leq }$ которые действительно необходимы в доказательстве, были аксиоматизированы в строках с 1 по 3.
4. В то время как обычная сколемизация сохраняет выполнимость, обратная сколемизация, т. Е. Замена универсально количественно определяемых переменных функциями, сохраняет валидность.
5. Для этого нужна была Аксиома 3; на самом деле, если ${\displaystyle \leq }$ не был общий заказ, для несравнимых входов невозможно вычислить максимум ${\displaystyle x,y}$.

Рекомендации

1. Таз, Д .; Deville, Y .; Flener, P .; Hamfelt, A .; Фишер Нильссон, Дж. (2004). «Синтез программ в вычислительной логике». В M. Bruynooghe и K.-K. Лау (ред.). Разработка программ в области вычислительной логики. LNCS. 3049. Springer. С. 30–65. CiteSeerX  10.1.1.62.4976.
2. Алонсо Черч (1957). «Приложения рекурсивной арифметики к проблеме синтеза схем». Итоги Летнего института символической логики. 1: 3–50.
3. Ричард Бючи, Лоуренс Ландвебер (апрель 1969 г.). «Решение последовательных условий с помощью стратегий с конечным числом состояний». Труды Американского математического общества. 138: 295–311. Дои:10.2307/1994916. JSTOR  1994916.
4. Солар-Лезама, Армандо (2008). Синтез программ с помощью зарисовок (Кандидат наук.). Калифорнийский университет в Беркли.
5. Алур, Раджив; др. и др. (2013). «Синтаксически управляемый синтез». Труды формальных методов в автоматизированном проектировании. IEEE. п. 8.
6. SyGuS-Comp (Конкурс синтаксически-управляемого синтеза)
7. Чарльз Фольксторф (7 января 2015 г.). «Программный синтез из аксиоматического доказательства правильности». arXiv:1501.01363 [cs.LO ].
8. Зохар Манна, Ричард Уолдингер (январь 1980 г.). «Дедуктивный подход к синтезу программ». Транзакции ACM по языкам и системам программирования. 2: 90–121. Дои:10.1145/357084.357090.
9. Зохар Манна и Ричард Уолдингер (декабрь 1978 г.). Дедуктивный подход к синтезу программ (PDF) (Техническое примечание). SRI International.
10. См. Manna, Waldinger (1980), p.100, чтобы узнать о правильности правил разрешения.
11. Манна, Вальдингер (1980), стр.108-111
12. Зохар Манна и Ричард Уолдингер (август 1987 г.). "Происхождение парадигмы двоичного поиска". Наука компьютерного программирования. 9 (1): 37–83. Дои:10.1016/0167-6423(87)90025-6.
13. Даниэле Нарди (1989). «Формальный синтез алгоритма объединения методом дедуктивной таблицы». Журнал логического программирования. 7: 1–43. Дои:10.1016/0743-1066(89)90008-3.
14. Даниэле Нарди и Риккардо Розати (1992). «Дедуктивный синтез программ для ответа на запросы». В Кунг-Киу Лау и Тим Клемент (ред.). Международный семинар по синтезу и преобразованию логических программ (LOPSTR). Мастерские по вычислительной технике. Springer. С. 15–29. Дои:10.1007/978-1-4471-3560-9_2.
15. Джонатан Трауготт (1986). «Дедуктивный синтез сортировочных программ». Материалы Международной конференции по автоматизированному вычету. LNCS. 230. Springer. С. 641–660.
16. Джонатан Трауготт (июнь 1989 г.). «Дедуктивный синтез сортировочных программ». Журнал символических вычислений. 7 (6): 533–572. Дои:10.1016 / S0747-7171 (89) 80040-9.
17. Манна, Вальдингер (1980), стр.99
18. Манна, Вальдингер (1980), стр.104
19. Manna, Waldinger (1980), стр.103, со ссылкой на: Нил В. Мюррей (февраль 1979 г.). Процедура доказательства бескванторной неклаузальной логики первого порядка (Технический отчет). Syracuse Univ. 2-79.
20. Зохар Манна, Ричард Уолдингер (январь 1986 г.). «Особые отношения в автоматическом удержании». Журнал ACM. 33: 1–59. Дои:10.1145/4904.4905.
21. Зохар Манна, Ричард Уолдингер (1992). «Правила особых отношений неполны». Proc. CADE 11. LNCS. 607. Springer. С. 492–506.

• Зохар Манна, Ричард Уолдингер (1975). «Знание и рассуждение в синтезе программ». Искусственный интеллект. 6 (2): 175–208. Дои:10.1016/0004-3702(75)90008-9.
• Джонатан Трауготт (1986). «Дедуктивный синтез сортировочных программ». Материалы Международной конференции по автоматизированному вычету. LNCS. 230. Springer. С. 641–660.