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

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

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

Источник

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

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

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

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

Синтаксис-ориентированный синтез

В 2013 году исследователями из Университета Пенсильвании , Калифорнийского университета в Беркли и Массачусетского технологического института была предложена единая структура для решения задач синтеза программ под названием Синтаксис-ориентированный синтез (стилизованный SyGuS) . Входные данные алгоритма SyGuS состоят из логической спецификации и бесконтекстной грамматики выражений, ограничивающей синтаксис допустимых решений. Например, для синтеза функции f , возвращающей максимум два целых числа, логическая спецификация может выглядеть следующим образом:

( ж ( Икс , y ) знак равно Икс ∨ ж ( Икс , y ) знак равно y ) ∧ ж ( Икс , y ) ≥ Икс ∧ ж ( Икс , y ) ≥ y

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

<Exp> ::= x | y | 0 | 1 | <Exp> + <Exp> | ite(<Cond>, <Exp>, <Exp>)
<Cond> ::= <Exp> <= <Exp>

где «ite» означает «если-то-иначе». Выражение

ite(x <= y, y, x)

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

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

(set-logic LIA)
(synth-fun f ((x Int) (y Int)) Int
  ((i Int) (c Int) (b Bool))
  ((i Int (c x y (+ i i) (ite b i i)))
   (c Int (0 1))
   (b Bool ((<= i i)))))
(declare-var x Int)
(declare-var y Int)
(constraint (>= (f x y) x))
(constraint (>= (f x y) y))
(constraint (or (= (f x y) x) (= (f x y) y)))
(check-synth)

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

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

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

Индуктивный синтез с использованием контрпримеров (CEGIS) — эффективный подход к созданию звуковых программных синтезаторов. CEGIS предполагает взаимодействие двух компонентов: генератора , который генерирует программы-кандидаты, и верификатора , который проверяет, соответствуют ли кандидаты спецификации.

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

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

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

algorithm cegis is
    input: Program generator generate,
           verifier verify,
           specification spec,
    output: Program that satisfies spec, or failure

    inputs := empty set
    loop
        candidate := generate(spec, inputs)
        if verify(spec, candidate) then
            return candidate
        else verify yields a counterexample e
            add e to inputs
        end if

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

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

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

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

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

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

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

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

Первоначально в таблицу вводятся базовые знания, предварительные и постусловия. После этого вручную применяются соответствующие правила доказательства. Фреймворк был разработан для повышения удобочитаемости промежуточных формул человеком: в отличие от классического разрешения , он не требует клаузальной нормальной формы , но позволяет рассуждать с формулами произвольной структуры и содержащими любые соединения (« неклаузальное разрешение »). Доказательство завершено, когда ${\it {true}}$ было получено в столбце «Цели» или, что то же самое, ${\it {false}}$ в столбце Утверждения . Программы, полученные с помощью этого подхода, гарантированно удовлетворяют формуле спецификации, начиная с которой; в этом смысле они верны по своей конструкции . Только минималистский, но полный по Тьюрингу , чисто функциональный язык программирования , состоящий из условных, рекурсивных, арифметических и других операторов. поддерживается. Тематические исследования, выполненные в рамках этой структуры, синтезировали алгоритмы для вычисления, например, деления , остатка , квадратный корень , объединение терминов , ответы на к реляционной базе данных запросы и несколько алгоритмов сортировки .

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

К правилам доказательства относятся:

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

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

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

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

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

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

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

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

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

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

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

Пример

Пример синтеза функции максимума

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

В качестве игрушечного примера — функциональная программа для вычисления максимального $M$ из двух чисел $x$ и $y$ можно вывести следующим образом.

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

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

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

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

уступчивость $\lnot ($правда ∧ ложь ) ∧ ( х ≤ х ∧ у ≤ х ∧ истинный $)$, что упрощается до $x\leq x\land y\leq x$.

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

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

См. также

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

Ссылки

• Дэвид, Кристина; Кренинг, Дэниел (13 октября 2017 г.). «Программный синтез: проблемы и возможности» . Философские труды Королевского общества A: Математические, физические и технические науки . 375 (2104): 20150403. doi : 10.1098/rsta.2015.0403 . ISSN   1364-503X . ПМЦ   5597726 . ПМИД   28871052 .
• Алур, Раджив; Сингх, Ришаб; Фисман, Дана; Солар-Лезама, Армандо (20 ноября 2018 г.). «Поисковой программный синтез» . Коммуникации АКМ . 61 (12): 84–93. дои : 10.1145/3208071 . ISSN   0001-0782 .
• Зоар Манна, Ричард Уолдингер (1975). «Знание и рассуждение в синтезе программ». Искусственный интеллект . 6 (2): 175–208. дои : 10.1016/0004-3702(75)90008-9 .
• Солар-Лезама, Армандо (2008). Синтез программы путем эскизирования (PDF) (доктор философии). Калифорнийский университет, Беркли.