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

В информатике синтез программ — это задача построения программы , которая доказуемо удовлетворяет заданной формальной спецификации высокого уровня . В отличие от проверки программ , программа должна быть построена , а не дана; однако обе области используют методы формального доказательства, и обе включают подходы с различной степенью автоматизации. В отличие от методов автоматического программирования , спецификации в синтезе программ обычно являются неалгоритмическими утверждениями в соответствующем логическом исчислении . [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]

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

Правила неклаузуального разрешения (унифицирующие замены не показаны)
№УтвержденияЦелиПрограммаИсточник
51 Э [ п ] {\displaystyle E[п]}
52 Ф [ п ] {\displaystyle F[п]}
53 Г [ п ] {\displaystyle G[п]} с
54 ЧАС [ п ] {\displaystyle H[п]} т
55 Э [ истинный ] ∨ Ф [ ЛОЖЬ ] {\displaystyle E[{\text{true}}]\or F[{\text{false}}]} Решимость(51,52)
56 ¬ Ф [ истинный ] ∧ Г [ ЛОЖЬ ] {\displaystyle \lnot F[{\text{истина}}]\land G[{\text{ложь}}]} сРешимость(52,53)
57 ¬ Ф [ ЛОЖЬ ] ∧ Г [ истинный ] {\displaystyle \lnot F[{\text{false}}]\land G[{\text{true}}]} сРешимость(53,52)
58 Г [ истинный ] ∧ ЧАС [ ЛОЖЬ ] {\displaystyle G[{\text{истина}}]\land H[{\text{ложь}}]} Тихоокеанское стандартное время​​Решимость(53,54)

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

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

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

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

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

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

Например, строка 55 получается путем разрешения формул утверждения из 51 и из 52, которые обе имеют некоторую общую подформулу . Резольвента формируется как дизъюнкция , с заменой на , и , с заменой на . Эта резольвента логически следует из конъюнкции и . В более общем смысле, и необходимо иметь только две унифицируемые подформулы и , соответственно; их резольвента затем формируется из и как и прежде, где — наиболее общий унификатор и . Это правило обобщает разрешение предложений . [22] Э {\displaystyle E} Ф {\displaystyle F} п {\displaystyle p} Э {\displaystyle E} п {\displaystyle p} т г ты е {\displaystyle {\it {истина}}} Ф {\displaystyle F} п {\displaystyle p} ф а л с е {\displaystyle {\it {ложь}}} Э {\displaystyle E} Ф {\displaystyle F} Э {\displaystyle E} Ф {\displaystyle F} п 1 {\displaystyle p_{1}} п 2 {\displaystyle p_{2}} Э θ {\displaystyle E\тета } Ф θ {\displaystyle F\тета } θ {\displaystyle \тета} п 1 {\displaystyle p_{1}} п 2 {\displaystyle p_{2}}
Программные термины родительских формул объединяются, как показано в строке 58, для формирования выходных данных резольвенты. В общем случае применяется к последней также. Поскольку подформула появляется в выходных данных, необходимо соблюдать осторожность, чтобы разрешать только подформулы, соответствующие вычислимым свойствам. θ {\displaystyle \тета} п {\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)} 0 ≤ н ′ < н {\displaystyle 0\leq n'<n}

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

Пример

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

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

Начиная с описания требования " Максимум больше или равен любому заданному числу и является одним из заданных чисел " , формула первого порядка получается как ее формальный перевод. Эта формула должна быть доказана. С помощью обратной сколемизации [примечание 4] получается спецификация в строке 10, заглавная и строчная буквы обозначают переменную и константу Сколема соответственно. ∀ X ∀ Y ∃ M : X ≤ M ∧ Y ≤ M ∧ ( X = M ∨ Y = M ) {\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, с M {\displaystyle M} 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 )} x ≤ x ∧ y ≤ x {\displaystyle x\leq x\land y\leq x}

Аналогичным образом строка 14 дает строку 15, а затем строку 16 по разрешению. Кроме того, второй случай в строке 13 обрабатывается аналогично, в конечном итоге давая строку 18. x ≤ M ∧ y ≤ M ∧ y = M {\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 содержат программный термин, в столбце программы получается условное выражение . Поскольку формула цели была выведена, доказательство выполнено, и столбец программы строки « » содержит программу. x ≤ y {\displaystyle x\leq y} y {\displaystyle y} y ≤ x {\displaystyle y\leq x} x {\displaystyle x} true {\displaystyle {\textit {true}}} true {\displaystyle {\textit {true}}}

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

Примечания

  1. ^ Различие «Утверждения» / «Цели» введено только для удобства; следуя парадигме доказательства от противного , Цель эквивалентна утверждению . F {\displaystyle F} ¬ F {\displaystyle \lnot F}
  2. ^ Когда и — формула Goal и термин Program в строке, соответственно, то во всех случаях, когда выполняется, — допустимый вывод синтезируемой программы. Этот инвариант поддерживается всеми правилами доказательства. Формула Assertion обычно не связана с термином Program. F {\displaystyle F} s {\displaystyle s} F {\displaystyle F} s {\displaystyle s}
  3. ^ С самого начала поддерживается только условный оператор ( ?: ). Однако можно добавлять произвольные новые операторы и отношения, предоставляя их свойства в качестве аксиом. В игрушечном примере ниже были аксиоматизированы только те свойства и , которые действительно нужны в доказательстве, в строках с 1 по 3. = {\displaystyle =} ≤ {\displaystyle \leq }
  4. ^ В то время как обычная скулемизация сохраняет выполнимость, обратная скулемизация, т. е. замена универсально квантифицированных переменных функциями, сохраняет валидность.
  5. ^ Для этого нужна была аксиома 3; на самом деле, если бы не было общего порядка , то для несопоставимых входных данных не мог бы быть вычислен максимум . ≤ {\displaystyle \leq } x , y {\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 error: no target: CITEREFAlurSinghFisman (help)
  3. ^ Алонзо Чёрч (1957). «Применение рекурсивной арифметики к проблеме синтеза схем». Резюме Летнего института символической логики . 1 : 3–50 .
  4. ^ Ричард Бюхи, Лоуренс Ландвебер (апрель 1969 г.). «Решение последовательных условий с помощью стратегий конечных состояний». Труды Американского математического общества . 138 : 295– 311. doi : 10.2307/1994916. JSTOR  1994916.
  5. ^ (Солар-Лезама) harv error: no target: CITEREFSolar-Lezama (help)
  6. ^ Alur, Rajeev; al., et (2013). «Синтаксически-управляемый синтез». Труды по формальным методам в автоматизированном проектировании . IEEE. стр. 8.
  7. ^ (Дэвид и Крёнинг) harv error: no target: CITEREFDavidKroening (help)
  8. ^ SyGuS-Comp (Конкурс по синтаксическому синтезу)
  9. ^ (Солар-Лезама) harv error: no target: CITEREFSolar-Lezama (help)
  10. ^ (Дэвид и Крёнинг) harv error: no target: CITEREFDavidKroening (help)
  11. ^ (Солар-Лезама) harv error: no target: CITEREFSolar-Lezama (help)
  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. Vol. 607. Springer. pp.  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.). Калифорнийский университет в Беркли.
Retrieved from "https://en.wikipedia.org/w/index.php?title=Program_synthesis&oldid=1241784157#Syntax-guided_synthesis"