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

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

Происхождение [ править ]

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

С тех пор проблемой синтеза программ стали заниматься различные исследовательские сообщества. Известные работы включают в себя 1969 автоматах теоретико-подход Büchi и Ландвебером , ^[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 : t	Решимость (53,54)

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

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

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

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

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

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

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

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

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

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

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

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

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

Мюррей показал, что эти правила полны для логики первого порядка . ^[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}$

Исходя из описания требования « Максимум больше или равен любому заданному числу и является одним из заданных чисел », формула первого порядка получается как ее формальный перевод. Эта формула требует доказательства. При обратной сколемизации , ^{[примечание 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 , полученным синтаксическим объединением последних формул,
• Р [ р ] является истинным ∧ х = х , получается из конкретизированной линии 1 (соответственно дополняетсячтобы сделать контекст F [⋅] вокруг р видно), и
• G [ p ] является x ≤ x ∧ y ≤ x ∧ x = x , полученным из созданной строки 12,

дает истину ∧ ложь ) ∧ ( 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}}}$

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

См. Также [ править ]

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

Примечания [ править ]

Ссылки [ править ]

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