Синтез программы

Задача построить программу, соответствующую формальной спецификации

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

Основное применение синтеза программ — освободить программиста от бремени написания правильного, эффективного кода, который удовлетворяет спецификации. Однако синтез программ также имеет приложения к супероптимизации и выводу инвариантов циклов . ^[2]

Источник

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

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

Развитие 21 века

В начале 21 века в сообществе формальной верификации и смежных областях произошел всплеск практического интереса к идее синтеза программ . Армандо Солар-Лезама показал, что можно кодировать проблемы синтеза программ в булевой логике и использовать алгоритмы для проблемы выполнимости булевых уравнений для автоматического поиска программ. ^[5]

Синтез, управляемый синтаксисом

В 2013 году исследователи из UPenn , UC Berkeley и MIT предложили унифицированную структуру для задач синтеза программ под названием Syntax-guided Synthesis (стилизованный SyGuS) . ^[6] Входные данные для алгоритма SyGuS состоят из логической спецификации вместе с контекстно-свободной грамматикой выражений, которая ограничивает синтаксис допустимых решений. ^[7] Например, чтобы синтезировать функцию f , которая возвращает максимальное из двух целых чисел, логическая спецификация может выглядеть следующим образом:

( f ( x , y ) = x ∨ f ( x , y ) = y ) ∧ f ( x , y ) ≥ x ∧ f ( x , y ) ≥ y

и грамматика может быть такой:

< Эксп >  ::= x | y | 0 | 1 | < Эксп > + < Эксп > | ite( < Условие > , < Эксп > , < Эксп > ) < Условие >  ::=  < Эксп > <= < Эксп >

где "ite" означает "if-then-else". Выражение

ite(x <= y, y, x)

было бы правильным решением, поскольку оно соответствует грамматике и спецификации.

С 2014 по 2019 год ежегодный конкурс Syntax-Guided Synthesis Competition (или SyGuS-Comp) сравнивал различные алгоритмы синтеза программ в соревновательном мероприятии. ^[8] В соревновании использовался стандартизированный формат ввода SyGuS-IF, основанный на SMT-Lib 2. Например, следующий SyGuS-IF кодирует задачу синтеза максимального из двух целых чисел (как представлено выше):

(набор-логический LIA)(synth-fun f ((x Int) (y Int)) Int ((i Целое) (c Целое) (b Логическое)) ((i Int (cxy (+ ii) (ite bii))) (c Целое (0 1)) (b Бул ((<= ii)))))(объявить-var x Int)(объявить-var y Int)(ограничение (>= (fxy) x))(ограничение (>= (fxy) y))(ограничение (или (= (fxy) x) (= (fxy) y)))(чек-синтезатор)

Соответствующий решатель может вернуть следующий вывод:

((define-fun f ((x Int) (y Int)) Int (ite (<= xy) yx)))

Индуктивный синтез, управляемый контрпримером

Контрпримерный управляемый индуктивный синтез (CEGIS) — это эффективный подход к созданию синтезаторов звуковых программ. ^{[9] [10]} CEGIS включает взаимодействие двух компонентов: генератора , который генерирует программы-кандидаты, и верификатора , который проверяет, соответствуют ли кандидаты спецификации.

При заданном наборе входов I , наборе возможных программ P и спецификации S целью синтеза программы является нахождение программы p в P такой, что для всех входов i в I выполняется S ( p , i ). CEGIS параметризуется с помощью генератора и верификатора:

• Генератор принимает набор входных данных T и выводит программу-кандидат c , которая верна для всех входных данных в T , то есть кандидата, такого, что для всех входных данных t в T выполняется S ( c , t ) .
• Верификатор берет программу-кандидат c и возвращает true, если программа удовлетворяет S на всех входных данных , в противном случае возвращает контрпример , то есть входные данные e в I, такие, что S ( c , e ) не выполняется.

CEGIS запускает генератор и верификатор в цикле, накапливая контрпримеры:

Алгоритм cegis является  входным параметром : Генератор программ сгенерирует , верификатор проверить , спецификация спецификация , вывод : Программа, которая удовлетворяет спецификации , или неудача входные данные  := пустой набор цикл  кандидат  := сгенерировать ( спецификация , входные данные ) если  проверить ( спецификация , кандидат ) тогда  вернуть  кандидата  иначе  проверить выдает контрпример e добавить e к входным данным  конец if

Реализации CEGIS обычно используют решатели SMT в качестве верификаторов.

CEGIS был вдохновлен уточнением абстракции, направляемым контрпримерами (CEGAR). ^[11]

Структура Манны и Вальдингера

Структура Манны и Вальдингера , опубликованная в 1980 году, ^{[12] [13] начинается с} формулы спецификации первого порядка, заданной пользователем . Для этой формулы строится доказательство, тем самым также синтезируя функциональную программу из унифицирующих подстановок.

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

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

Первоначально в таблицу вводятся фоновые знания, предварительные условия и постусловия. После этого вручную применяются соответствующие правила доказательства. Фреймворк был разработан для улучшения читаемости промежуточных формул человеком: в отличие от классической резолюции , он не требует клаузальной нормальной формы , но позволяет рассуждать с формулами произвольной структуры и содержащими любые юнкторы (« неклаузальная резолюция »). Доказательство считается полным, когда выведено в столбце Цели или, что эквивалентно, в столбце Утверждения . Программы, полученные с помощью этого подхода, гарантированно удовлетворяют формуле спецификации, с которой началась; в этом смысле они являются правильными по построению . ^[14] Поддерживается только минималистский, но полный по Тьюрингу ^[15] чисто функциональный язык программирования , состоящий из условных, рекурсивных, арифметических и других операторов ^{[примечание 3]} . Исследования конкретных случаев, выполненные в рамках этой структуры, синтезировали алгоритмы для вычисления, например, деления , остатка , ^[16] квадратного корня , ^[17] объединения терминов , ^[18] ответов на запросы реляционной базы данных ^[19] и нескольких алгоритмов сортировки . ^{[20] [21]} ${\displaystyle {\it {true}}}$ ${\displaystyle {\it {false}}}$

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

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

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

Например, строка 55 получается путем разрешения формул утверждения из 51 и из 52, которые обе имеют некоторую общую подформулу . Резольвента формируется как дизъюнкция , с заменой на , и , с заменой на . Эта резольвента логически следует из конъюнкции и . В более общем смысле, и необходимо иметь только две унифицируемые подформулы и , соответственно; их резольвента затем формируется из и как и прежде, где — наиболее общий унификатор и . Это правило обобщает разрешение предложений . ^[22] ${\displaystyle E}$ ${\displaystyle F}$ ${\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}}$

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

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

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

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

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

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

Это правило допускает синтез рекурсивных функций . Для заданного пред- и постусловия "Дано такое, что , найти такое, что ", и соответствующего заданного пользователем полного упорядочения области , всегда разумно добавить Утверждение " ". ^[23] Разрешение с помощью этого утверждения может ввести рекурсивный вызов в термине Программы. ${\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'))}$ ${\displaystyle f}$

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

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

Пример

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

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

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

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

• p является общим примером x=x для A=A и x=M , полученным путем синтаксического объединения последних формул,
• F[ p ] является истинным ∧ x=x , полученным из инстанцированной строки 1 (соответствующим образом дополненной, чтобы сделать контекст F[⋅] вокруг p видимым), и
• G[ p ] где x ≤ x ∧ y ≤ x ∧ x = x , получено из инстанцированной строки 12,

что дает true ∧ false ) ∧ ( x ≤ x ∧ y ≤ x ∧ true , что упрощается до . ${\displaystyle \lnot (}$ ${\displaystyle )}$ ${\displaystyle x\leq x\land y\leq x}$

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

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

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

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

Примечания

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

Ссылки

1. Basin, D.; Deville, Y.; Flener, P.; Hamfelt, A.; Fischer Nilsson, J. (2004). «Синтез программ в вычислительной логике». В M. Bruynooghe и K.-K. Lau (ред.). Разработка программ в вычислительной логике . LNCS. Том 3049. Springer. стр. 30–65. CiteSeerX  10.1.1.62.4976 .
2. (Алур, Сингх и Фисман)ошибка harv: нет цели: CITEREFAlurSinghFisman ( помощь )
3. Алонзо Чёрч (1957). «Применение рекурсивной арифметики к проблеме синтеза схем». Резюме Летнего института символической логики . 1 : 3–50.
4. Ричард Бюхи, Лоуренс Ландвебер (апрель 1969 г.). «Решение последовательных условий с помощью стратегий конечных состояний». Труды Американского математического общества . 138 : 295–311. doi :10.2307/1994916. JSTOR  1994916.
5. (Солар-Лезама)ошибка harv: нет цели: CITEREFSolar-Lezama ( помощь )
6. Alur, Rajeev; al., et (2013). «Синтаксически-управляемый синтез». Труды по формальным методам в автоматизированном проектировании . IEEE. стр. 8.
7. (Дэвид и Крёнинг)ошибка harv: нет цели: CITEREFDavidKroening ( справка )
8. SyGuS-Comp (Конкурс по синтаксическому синтезу)
9. (Солар-Лезама)ошибка harv: нет цели: CITEREFSolar-Lezama ( помощь )
10. (Дэвид и Крёнинг)ошибка harv: нет цели: CITEREFDavidKroening ( справка )
11. (Солар-Лезама)ошибка harv: нет цели: CITEREFSolar-Lezama ( помощь )
12. Зохар Манна, Ричард Уолдингер (январь 1980 г.). «Дедуктивный подход к синтезу программ». Труды ACM по языкам и системам программирования . 2 : 90–121. doi :10.1145/357084.357090. S2CID  14770735.
13. Зохар Манна и Ричард Уолдингер (декабрь 1978 г.). Дедуктивный подход к синтезу программ (PDF) (Техническая записка). SRI International. Архивировано (PDF) из оригинала 27 января 2021 г.
14. См. Manna, Waldinger (1980), стр. 100 о корректности правил разрешения.
15. Boyer, Robert S.; Moore, J. Strother (май 1983 г.). Механическое доказательство полноты Тьюринга чистого Lisp (PDF) (технический отчет). Институт вычислительной науки, Техасский университет в Остине. 37. Архивировано (PDF) из оригинала 22 сентября 2017 г.
16. Манна, Вальдингер (1980), стр.108-111
17. Зохар Манна и Ричард Уолдингер (август 1987 г.). «Происхождение парадигмы бинарного поиска». Наука компьютерного программирования . 9 (1): 37–83. doi :10.1016/0167-6423(87)90025-6.
18. Даниэле Нарди (1989). «Формальный синтез алгоритма унификации методом дедуктивной таблицы». Журнал логического программирования . 7 : 1–43. doi :10.1016/0743-1066(89)90008-3.
19. Даниэле Нарди и Риккардо Розати (1992). «Дедуктивный синтез программ для ответов на запросы». В Кунг-Киу Лау и Тим Клемент (ред.). Международный семинар по синтезу и преобразованию логических программ (LOPSTR) . Семинары по вычислениям. Springer. стр. 15–29. doi :10.1007/978-1-4471-3560-9_2.
20. Джонатан Трауготт (1986). «Дедуктивный синтез программ сортировки». Труды Международной конференции по автоматизированной дедукции . LNCS . Т. 230. Springer. С. 641–660.
21. Джонатан Трауготт (июнь 1989 г.). «Дедуктивный синтез программ сортировки». Журнал символических вычислений . 7 (6): 533–572. doi :10.1016/S0747-7171(89)80040-9.
22. Манна, Вальдингер (1980), стр.99
23. Манна, Вальдингер (1980), стр.104
24. Manna, Waldinger (1980), стр. 103, ссылаясь на: Neil V. Murray (февраль 1979). Процедура доказательства для безквантовой неклаузальной логики первого порядка (технический отчет). Syracuse Univ. 2-79.
25. Зохар Манна, Ричард Уолдингер (январь 1986 г.). «Специальные отношения в автоматизированной дедукции». Журнал ACM . 33 : 1–59. doi : 10.1145/4904.4905 . S2CID  15140138.
26. Зохар Манна, Ричард Уолдингер (1992). «Правила специальных отношений неполны». Proc. CADE 11. LNCS. Том 607. Springer. С. 492–506.

• Дэвид, Кристина; Кренинг, Дэниел (2017-10-13). «Программный синтез: проблемы и возможности». Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences . 375 (2104): 20150403. doi :10.1098/rsta.2015.0403. ISSN  1364-503X. PMC 5597726.  PMID 28871052  .
• Алур, Раджив; Сингх, Ришабх; Фисман, Дана; Солар-Лезама, Армандо (2018-11-20). «Синтез программ на основе поиска». Сообщения ACM . 61 (12): 84–93. doi :10.1145/3208071. ISSN  0001-0782.
• Зохар Манна, Ричард Вальдингер (1975). «Знание и рассуждение в синтезе программ». Искусственный интеллект . 6 (2): 175–208. doi :10.1016/0004-3702(75)90008-9.
• Solar-Lezama, Armando (2008). Синтез программ путем создания эскизов (PDF) (Ph.D.). Калифорнийский университет в Беркли.