程序合成

在计算机科学中，程序合成是构建一个可以满足给定高级正式规范的程序的任务。与程序验证相反，该程序应构建而不是给出；但是，这两个领域都利用了形式的证明技术，并且两者都构成了不同程度的自动化的方法。与自动编程技术相反，程序合成中的规格通常是适当的逻辑演算中的非算法语句。

程序综合的主要应用是减轻程序员编写正确，有效的代码的负担，以满足规范。但是，程序合成还具有循环不变性的超级优化和推断的应用。

起源

在1957年康奈尔大学符号逻辑研究所期间，阿隆佐教堂（Alonzo Church）将问题定义为从数学要求中综合了电路。即使作品仅是指电路而不是程序，但该工作仍被认为是对程序综合的最早描述之一，一些研究人员将程序综合称为“教会的问题”。在1960年代，人工智能研究人员探索了“自动程序员”的类似想法。

从那时起，各个研究社区都考虑了程序综合问题。著名的作品包括Büchi和Landweber的1969年自动机理论方法，以及Manna和Waldinger的作品（c。1980）。现代高级编程语言的发展也可以理解为程序合成的一种形式。

21世纪的发展

21世纪初期，人们对正式验证社区和相关领域的程序综合观念的实际兴趣激增。 Armando Solar-Lezama表明，可以在布尔逻辑中编码程序综合问题，并使用算法来自动找到程序。

语法引导的合成

2013年， UPENN ， UC BERKELEY和MIT的研究人员提出了一个统一的计划合成问题统一的程序合成问题（Syntax引导的合成）。 Sygus算法的输入由逻辑规范以及一个无上下文的表达式语法组成，该语法限制了有效解决方案的语法。例如，要合成返回两个整数的函数f ，逻辑规范可能看起来像这样：

（ f （ x ， y ）= x f （ x ， y ） = y ） ∧f （ x ，y） ≥x∧f （ x ， y ）≥y

语法可能是： 

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

“ ite”代表“如果是else”。表达方式 

ite(x <= y, y, x)

将是一个有效的解决方案，因为它符合语法和规范。

从2014年到2019年，年度语法指导的合成竞赛（或Sygus-Comp）比较了竞争性活动中计划合成的不同算法。该竞赛基于SMT-LIB 2使用了标准化的输入格式Sygus-if。例如，以下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)))

Manna和Waldinger的框架

非顾问分辨率规则（未显示统一替换）
nr 断言 目标 程式 起源
51
52
53 s
54 t
55 解决（51,52）
56 s 解决（52,53）
57 s 解决（53,52）
58 p ？英石 决心（53,54）

Manna和Waldinger的框架于1980年出版，从用户赋予的一阶规范公式开始。对于该公式，构建了一个证明，从而从统一替换中综合了功能程序。

该框架显示在表布局中，包含：

  • 用于参考目的的行号（“ nr”）
  • 已经建立的公式，包括公理和先决条件，（“断言”）
  • 公式仍然有待证明，包括后条件，（“目标”），
  • 表示有效输出值的术语（“程序”）
  • 当前行的理由（“原始”）

最初，将背景知识，条件和后条件输入到表中。之后，手动应用适当的证明规则。该框架旨在增强中间公式的人类可读性：与经典的分辨率相反，它不需要可神经正常形式，而是允许人们使用任意结构和包含任何连接器的公式进行推理（“非可扣除分辨率”）。当证明是完整的已在目标列中或等效地得出在“断言”列中。通过这种方法获得的程序可以保证满足规范公式的启动；从这个意义上讲，它们是正确的。仅支持一种极简主义但纯净的，纯粹的功能编程语言，该语言由条件，递归和算术和其他操作员组成。在此框架中进行的案例研究合成算法，以计算EG除法，其余，平方根，项统一，关系数据库查询的答案和几种排序算法。

证明规则

证明规则包括：

例如，第55行是通过解决断言公式获得的从51和从52个共享一些常见的子形成 。分解形成为 ， 和取而代之 ， 和 ， 和取而代之 。从逻辑上讲，这种解析是从和 。更普遍， 和只需要两个纯净的子形成和 ， 分别;然后，它们的解析是由和和以前一样是最通用的统一者和 。该规则概括了条款的解决。
如第58行所示，将父式的程序术语组合在一起，以形成分解的输出。在一般情况下， 也应用于后者。自从subformula 出现在输出中，必须注意仅在与可计算属性相对应的子形成上解析。
  • 逻辑转换。
例如， 可以转变为 ）在主张和目标中，由于两者都是等效的。
  • 结合性主张和析取目标的分裂。
下面的玩具示例的第11至13行中显示了一个示例。
该规则允许综合递归功能。对于给定的前后条件这样 ， 寻找这样 ”，以及适当的用户良好订单 dom ，添加断言总是听起来很听起来” “。解决这个主张可以引入递归电话在程序术语中。
在Manna，Waldinger（1980），第108-111页中给出了一个示例被定义为 （第110页）。

默里（Murray）已显示这些规则已完成，以实现一阶逻辑。 1986年，Manna和Waldinger添加了广义的电子分辨率和偏见规则，以处理平等。后来，这些规则原来是不完整的（但声音）。

例子

示例最大功能的合成
nr 断言 目标 程式 起源
1 公理
2 公理
3 公理
10 M 规格
11 M 干扰（10）
12 M 拆分（11）
13 M 拆分（11）
14 x 解决（12,1）
15 x 解决（14,2）
16 x 解决（15,3）
17 y 解决（13,1）
18 y 解决（17,2）
19 x <y ？ Y ： X 决心（18,16）

作为玩具示例，一个功能程序来计算最大值两个数字和可以得出如下。

从需求描述开始：“最大值大于或等于任何给定的数字，并且是给定数字之一”，即一阶公式作为正式翻译获得。该公式将被证明。通过反向SkoLemization ，获得第10行中的规范，分别表示变量和skolem常数的上层和下案字母。

在第11行中应用转换规则为分布法中的变换规则后，证明目标是一个脱节，因此可以分为两种情况，即。第12和13行。

转向第一种情况，以第1行中的公理解决第12行导致程序变量的实例化在第14行中。直观地，第12行的最后一个结合规定了该价值在这种情况下必须采取。正式地，上面第57行中显示的非顾问分辨率规则应用于第12和1行，并使用

  • p是a = a和x = m的常见实例x = x ，通过句法统一后一个公式获得
  • f [ p ]为true∧x = x ，从实例化第1行获得（适当填充以使上下文f [ p a可见），并且
  • g [ p ]为x≤x∧y≤xx x = x ，从实例化的第12行获得，

屈服 true∧false ） ∧ （ x≤x∧y≤x ，简化 。

以类似的方式，第14行产生第15行，然后通过分辨率16行。另外，第二种情况在第13行中的处理方式类似，最终产生了第18行。

在最后一步中，使用第58行的分辨率规则加入了两个情况（IE第16和18行）；为了使该规则适用，需要步骤15→16。直觉上，第18行可以被读为“以防万一 ， 输出有效（相对于原始规范），而第15行说：“以防​​万一 ， 输出已验证;步骤15→16确定两个案例16和18都是互补的。由于第16行和第18行都带有程序术语，因此有条件的表达式在程序列中导致。由于目标公式已得出，进行了证明，并将“程序”列 “线包含该程序。

也可以看看