ACM通信

研究突出了

软件合成过程

作者:Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, Philippe Suter
ACM通讯，2012年2月，第55卷第2期，103-111页
10.1145/2076450.2076472
评论

根据规范自动合成程序片段可以使程序更容易编写和推理。为了将综合集成到编程语言中，软件综合算法应该以可预测的方式运行:它们应该成功地实现定义良好的规范类。我们建议系统地将决策程序推广为合成过程，并使用它们来编译嵌入在函数式和命令式程序中的隐式指定计算。综合过程是可预测的，因为无论何时存在满足规范的代码，它们都能保证找到满足规范的代码。为了说明我们的方法，我们通过扩展整数算法和集合数据结构的量词消除算法推导出综合过程。然后，我们展示了这种综合过程的实现可以扩展编译器，以支持隐式值定义和高级模式匹配。

回到顶部

1.简介

从说明书合成软件^8，15承诺使程序员更有效率。尽管最近在生成短指令序列的技术上取得了实质性的进展¹¹和程序片段,^21，22合成仅限于小段代码。我们预计这种情况在未来的一段时间内还会继续存在，原因有二:(1)合成在算法上是一个困难的问题，(2)合成可能需要详细的规范，这对于大型程序来说很难编写。

我们期望综合的重要实际应用在于它与通用编程语言的编译器的集成。为了使这种集成可行，我们的目标是确定定义良好的表达式和合成算法类成功的保证对于这些表达式类，就像任何格式良好的程序都会成功编译一样。我们这种合成算法的起点是决策程序．

一类公式的可满足性的决策过程在其类中接受一个公式(约束)，并检查其变量的某些值的公式是否为真。在这个基本功能的基础上，许多决策过程实现提供了额外的特性，即只要给定的公式是可满足的，就生成一个满意的赋值(一个模型)。这样的模型生成功能有很多用途，包括在验证和测试用例生成中更好的错误报告。一个重要的见解是，决策过程的模型生成工具也可以用作一种高级计算机制。给定一些变量的一组值，模型生成决策过程可以在运行时找到剩余变量的值，从而使给定的公式为真。这种机制有可能使决策过程的算法改进到声明式范式，如约束逻辑编程，¹⁰它将搜索引入到程序执行的内在方面。我们没有改变整个程序执行平台来支持搜索，而是引入了一种方法来编译表达性的声明性约束，同时对程序的其余部分保留现有的执行和编译技术。

我们的方法是将决策过程转化为合成过程，它在编译时以参数化约束作为输入执行。合成过程生成一个专门的代码片段，在运行时接受参数的值并计算变量的值。保证计算值满足指定的约束条件。因此，生成的代码特定于所需的约束，并且可以更高效。它不要求决策过程在运行时出现。这种方法还可以通过检查生成的解决方案存在和唯一的条件，给开发人员静态反馈。我们使用这个术语合成对于我们的方法，因为它从隐式规范开始，并涉及编译时的预计算。因为它计算的函数满足给定的输入/输出关系，我们称之为合成功能相对于反应合成法。¹⁹最后，我们调用我们的方法完整的因为它保证对来自定义良好的类的所有规范表达式都有效。

合成过程的输入只是所需的约束，而不一定是草图中合成代码的值或结构上的任何边界²¹和resource-bounded合成。²²这使得一个综合过程高度自动化，但意味着它的实现不能只依赖于搜索一个明显有限的状态空间;相反，它必须使用来自潜在决策程序的见解。对特定理论的决策程序的使用也将我们的工作与早期基于一阶逻辑的工作区分开来。^8，11

我们通过概述两个无界领域的合成算法来演示我们的方法:线性算法和以集合表示的对象集合。我们已经将这些算法作为Scala编程语言的编译器扩展来实现和部署。¹⁶读者可以在Kuncak等人中找到更多的细节。¹²我们发现我们的扩展使开发人员能够更自然地表达许多程序片段。例如，可以声明程序应该满足的不变量，而不是建立这些不变量的计算细节。在我们的经验中，合成时间是可以接受的，运行时间类似于等效的手写代码。

回到顶部

2.例子

我们首先举例说明整数线性算法的合成过程的使用。考虑下面的示例，将给定的秒数(存储在变量tosec中)分解为小时、分钟和剩余秒。(val关键字引入了一个具有给定值的不可变“变量”。)

我们的合成器成功了，因为约束是一个属于整数线性算法的公式。然而，合成器发出以下警告:

这个警告的原因是m和s的界限不严格。修正规范中的错误后，将m 60替换为m < 60，将s 60替换为s < 60，合成器不发出警告。生成的代码对应如下:

没有警告就保证了解决方案总是存在并且是唯一的。通过这种风格的代码编写，开发人员直接保证满足h * 3600 + m * 60 + s == tosec键的正确性条件，使程序的理解和验证更加容易。如果开发人员显式地编写计算，静态分析器或验证器可能很难恢复关键正确性条件。

进一步使用这个示例，假设开发人员强加了这个约束

然后，我们的系统发出以下警告:

指出当tosec参数太大时，约束没有解的事实。

除了choose函数之外，程序员还可以使用综合法对整数进行更灵活的模式匹配。在现有的确定性编程语言中，整数匹配要么在常量类型上进行测试，要么在Haskell (n+k)图案，在一些非常特殊的图案形式。我们的方法支持更丰富的模式集，如下面的快速求幂代码所示，它对参数是零、偶数还是奇数进行案例分析:

在这个例子中，系统使用合成，例如，计算j从约束我= 2 *j+ 1。函数的正确性源于fp(米,b,我) =mb^我，我们可以用归纳法证明。的情况下我= 2 *j+ 1我们观察到:

请注意，整数算术表达式上的模式匹配暴露了使归纳证明更清晰的方程。为了支持这个构造，我们的编译器扩展生成了选择适当的大小写并将i分解为适当的新指数j的代码。此外，它检查模式匹配是否详尽。该构造支持线性整数算术的任意表达式(它可以证明，例如，模式2 * k, 3 * k, 6 * k 1,6 * k + 1的集合是穷尽的)。系统还接受隐式定义，例如

系统确保上述定义匹配每个整数z(因为42和5是互质数)，并发出代码进行计算x而且y从z．

我们的方法和实现也适用于参数化整数算术公式，只有当参数已知时，它才会变成线性的。例如，我们的合成器接受以下规范，将静态未知维数的三维数组的线性表示的偏移量分解为每个坐标的索引:

在这里，dimX、dimY、dimZ是变量，其值在运行时之前是未知的。请注意，包含变量相乘的约束的可满足性通常是不可判定的。在这种参数化的情况下，我们的合成器在某种意义上是完整的，它生成的代码(1)总是终止，(2)在运行时检测当前参数值是否存在解，以及(3)每当有解存在时计算一个解。

除了整数算法，其他理论也适用于综合，并提供类似的好处。考虑以平衡的方式分割集合的问题。下面的代码尝试这样做:

对于上面的代码，我们的合成器发出了一个警告，表明在某些情况下约束没有解决方案。事实上，当集合s的大小为奇数时，没有解。如果我们弱化规范

那么我们的合成器就可以证明代码对于所有可能的输入集都有一个解。合成器发出代码，对于每个输入，计算一个这样的解。集合约束的本质是，如果有一个解，那么就有许多解。我们的合成器在编译时解决这些选择。因此，产生的代码是确定性的。

回到顶部

3.隐式计算

接下来，我们将介绍将隐式计算嵌入到通用编程语言中的编程语言构造。我们的构造和算法是由一个语法定义的集合Formulas参数化的。公式表示真值，我们将它们表示为定义良好的布尔类型编程语言表达式的子集。公式是由术语(表示的术语)构建的，它是编程语言表达式，表示某些类型的值，如整数或集合。

3.1.“选择”结构

作为支持隐式计算的基本形式，我们将这种形式的构造集成到编程语言中

在这里F公式(不包含选择)和吗F的匿名函数的布尔值F(例如,．F)．当我们使用诸如为了表示一个变量，我们假设它可以代表一个由0、1或多个实际变量组成的元组。其中可以出现两种变量F:输出变量和参数．的参数是在选择发生时作用域内的程序变量;它们的值将在语句执行时知道。输出变量表示需要计算的值，以便F成为现实，他们将被分配作为选择的结果。

隐式计算的好处之一是它们显式地确定了允许开发人员假设的属性。特别地，我们可以将上面的choose构造转换为以下命令序列，并使用保护命令语言⁴：

在这里,F［: =表示替换变量的结果与条款在公式F浩劫表示给定变量的非确定性变化。上述翻译的简单性表明，在现有的验证系统中表示选择是很自然的^6，24．

3.2.广义条件

我们的下一个构造使开发人员能够指定如何对缺少约束的解决方案作出反应。作为一个具体的例子，考虑一下

如果一个那么它的值是7x是3，结果是13。如果一个是10，结果是11。一般形式如下:

x是一个绑定变量，这可能出现在两个F而且T．布尔表达式F属于公式，而T而且E是任何编程语言表达式。该构造检查是否存在值x令人满意的F，如果是，计算T与x绑定到一个这样的值。如果不存在这样的值，则进行计算E(这并不是指x)．转换为受保护的命令也很简单。

3.3.表达模式匹配

我们可以使用广义条件来定义高级形式的模式匹配。考虑一个在结构上与我们前面看到的示例相似的模式匹配表达式。

我们显式地将绑定模式变量命名为j，而不是依赖于语法约定来推断它。此外，我们还添加了保护，使表达式更有趣。我们可以将上述模式匹配转化为:

像2*j这样的表达式属于Terms，而像j > 0这样的条件属于Formulas。上述翻译推广到模式中使用的可决定逻辑的任意Terms和逻辑中的任意formula作为条件的情况。

在后续部分中，我们将重点放在choose构造上，记住条件匹配和模式匹配构造可以类似地合成。

回到顶部

4.派生的合成过程

接下来，我们精确地定义了综合过程的概念，并描述了从决策过程中导出综合过程的方法。

我们用变量表示集合。阵线(问)表示公式或项中的自由变量集合问．如果= (x₁、……x_n)，我们也用要表示变量集{x₁、……x_n}。如果问是一个项或公式，= (x₁、……x_n)一个变量向量和= (t₁、……x_n)一个向量的项，那么问［: =表示同时代入的结果问自由变量x₁、……x_n与条款t₁、……t_n,分别。给定一个替换:FV(F)我们写术语F代入的结果x阵线(F)和(x)．

4.1.Model-generating决策过程

作为选择调用综合算法的起点，我们考虑一个模型生成决策过程。鉴于F我们期望这个决策过程产生的公式

1. 替换:阵线(F）C这样F是一个真正的
2. 或者unsat值，如果不存在这样的替换

我们假设决策过程是确定性的，并表现为一个函数。我们写Z (F)=或Z (F)=unsat，表示将决策过程应用于的结果F．

4.2.解释方法

就像解释器可以被认为是编译器的基线实现一样，作为我们方法的基线，我们考虑在运行时部署一个模型生成决策过程。考虑选择语句(1)F_树表示公式的语法树F，在编程语言中表示为一个值，并被接受为决策过程的输入Z．同样,让一个_的名字表示自由参数变量名的语法表示一个在F．

上面的代码用它们的实际值替换已知参数(将值转换为公式语法树的常量)，然后调用决策过程Z获取剩余变量的值。类似地，我们可以替换(鉴于xF有T其他的E)与

在这里T表示在返回的替换丰富的环境中评估术语T。这种动态调用方法是灵活的(因为F可以在运行时计算)，并且可以立即受益于投入到实现现有决策过程中的大量工程工作。但是，另一种编译方法可能具有重要的性能和可预测性优势，我们将在本文的其余部分探讨这些优势。

4.3.编译:合成过程

我们考虑一种编译方法，在编译时调用修改的决策过程，将公式转换为求解形式。

定义1(合成过程)。综合过程以公式F和变量向量作为输入．它输出一对

1. 先决条件公式,精准医疗与阵线(前)阵线(F) \
2. 术语的元组,阵线()阵线(F) \

使下列两项影响有效:

我们指出这样一个事实，即在和F收益率精准医疗而且通过编写．

请注意,Always成立，因此上面的定义意味着这三个公式都是等价的:．因此，如果我们知道如何计算，我们可以定义．在实践中，对…应用化简是有用的，因此我们显式地返回pre。

请注意,F前,是否可以在当前程序点(我们表示的是哪个点)引用范围内的变量在3.1节中，但为了可读性经常省略)。合成器发出这些术语在编译器的中间表示;然后，标准编译器将它们与其他代码一起处理。的语法树用它的意义作为函数的参数输出变量．choose语句(1)的整个编译时处理涉及以下几个方面:

1. 如果公式pre是可满足的，则发出非可行性警告，报告合成问题无解的反例
2. 如果公式不惟一，则发出非惟一警告
   
   
   
   是可以满足的,是新鲜的变量);在这种情况下，作为反例报告所有自由变量的值，以表明至少有两个解
3. 作为编译后的代码，发出行为为断言(前);＝

一个模型生成决策过程的存在意味着一个“微不足道”的综合过程的存在，它满足定义1，但只是在运行时调用决策过程。(在传统编程语言领域，这类似于通过将源代码与解释器捆绑在一起“编译”代码，而不需要任何专门化。)因此，综合过程概念的有用性来自于这样一个事实:我们经常可以创建避免这种琐碎解决方案的编译代码。编译方法的潜在优势包括:

• 改进了运行时效率，因为部分推理是在编译时完成的。
• 改进的错误报告:可以在编译时检查解决方案的存在性和唯一性。
• 更简单的部署:发出的代码可以编译到编译器的任何目标，并且不需要额外的运行时支持。

本文采用的是编译方法。我们相信这种方法在实现隐式计算中具有重要的作用。也就是说，我们希望也有探索“即时合成”和“分析引导合成”的混合解释-编译解决方案的空间，类似于更传统语言的这种解决方案。

4.4.量词消除与合成

通过合成过程计算出的前提条件(在定义1中已经提到)可以看作是应用量词消去的结果(参见Bradley和Manna的第7章)¹)删除从F，有以下区别。

• 综合程序通过识别预先和发出代码来加强量词消除程序计算一个见证为．
• 量词消除算法的最坏情况界限衡量生成公式的大小和生成它所需的时间，但不衡量的大小或者是评估的时间．对于某些领域，计算(甚至“打印”)解决方案比简单地检查解决方案的存在性要困难得多。此外，一个算法，生成一个小的或简单的外观精准医疗不一定是执行速度最快的精准医疗而且．

尽管存在这些差异，我们发现我们可以很自然地扩展现有的量词消除程序，用构成程序的证人的显式计算．

4.5.Elimination-based合成工具箱

接下来，我们将描述一个与领域无关的基本技术工具箱，我们发现它在将量词消除过程转换为综合过程方面很有用。核心思想是确定证人期限函数。

定义2。一个见证项功能是一个函数

这样是一个有效的公式．注意,见证(y, F)可能包含变量FV(F) \ {y}。

4.5.1.多变量综合

我们可以举证(y, F)来合成任意数量的变量，使用以下翻译方案:

上面的翻译有基本情况，当没有变量要消除，所以F成为前提，并应用见证函数的递归情形。

在实现中，我们可以避免替换，只在生成的代码中使用局部变量定义_我相反的_我．我们生成一个代码块

阵线(_我)阵线(F) \ {x_我、……x_n}。这种递归转换模式的一个结果是，与量词消除过程的步骤相比，合成代码按保留顺序计算值。

4.5.2.一点规则合成

最基本和最广泛适用的量词消去形式，一点规则，立即导致一个综合程序步骤。如果x阵线(t)我们可以定义

如果公式还没有形式x＝tF，我们经常可以用保持等价的变换把它改写成这种形式，或者在某些情况下，加强公式。

4.5.3.从析句到条件句

考虑某个一阶理论中的一个无量词公式，其中的任务是检查公式的可满足性或应用消去变量。对于这两个任务，我们可以先将公式改写为析取范式，然后对每个析取进行独立处理。这使得我们可以专注于处理字面量的连词，而不是任意的命题组合。

接下来，我们展示我们可以同样地在合成中使用析取范式。考虑一个公式D₁.．.D_n用析取范式。我们可以对每一个应用合成D_我产生的先决条件精准医疗_我解出的形式_我．然后，我们可以用选择第一个的条件来合成代码_我适用于:

虽然析取范式可以比原公式大指数级，但在实际应用中采用了析取范式的转换。^20.其他量词消除方法具有更好的最坏情况复杂性⁵；这些同样可以转化为合成过程。决策树技术在这种情况下很有用。另外可能有用的是部分评估有效约束求解算法的技术，如DPLL(T)．⁷

请注意，量词消去过程中产生的许多析取，具有有限集合上的量化形式。在这种情况下，通常可以生成一个循环来搜索候选解，而不是生成一个大的条件表达式。这种方法可以大大减少合成代码的大小。我们发现这种技术适用于生成处理整数线性算法中的可除性约束的代码。

4.5.4.变量变换

当面对综合问题时，变量变换技术解决了一个相关但更简单的综合问题在哪里是一个新的变量向量。然后，合成代码恢复原始值通过让＝（),是一个可执行文件重建函数．

请注意,可能具有不同的维度，甚至不同类型的值的范围．在我们的综合过程中，我们已经在许多案例中使用了变量转换技术，如第5节将说明的:

• 高效处理线性整数方程
• 代表可分性约束
• 将集合的合成简化为整数的合成

一般来说,对正确性对于合成值，我们需要对应于的语义条件

这是我们所需要的映射的值令人满意的G的值令人满意的F．这个条件意味着的有效性．注意，如果我们可以表达作为我们逻辑中的一个术语，我们可以选择G与…相同F［: =（，立即保证(2)。

为完整性对于综合，我们还要求公式的有效性

这个完备性条件保证了新的综合问题不消除任何解。

条件(2)和(3)共同暗示了的综合前提条件而且都是一样的。给定这两个条件，我们通过定义变量变换:

公式加强:变量变换的一种特殊情况是加强公式，我们让是恒等函数。这个变换可以简化为找到一个公式G这需要F但是,是有效的。因此G可以减少解的数量，但不能从非零到零。公式强化是综合问题简单变换的自然正确条件。它更一般，而不是等价F而且G．例如，我们可以使用加强来替换变量之间的关系，使用包含顶级等式的更强的公式，实现4.5.2节的一点规则合成，可能是在4.5.3节的DNF转换之后。

去掉存在量词:另一种特殊情况是使用存在量词。这里我们假设F是这样的．G．我们的想法是综合两者的价值而且在G然后忽略．我们因此= (，)和定义（，) =．有了这个选择，(2)和(3)都保证持有。

回到顶部

5.整数算法与集合的综合程序

我们使用上一节描述的通用技术来设计整数线性算法的综合程序(第8章Bradley和Manna)¹)以及它的扩展支持具有基数约束的集合。¹³这些技术支持隐式计算的编译，如第2节和第3节中给出的示例。接下来，我们通过一个简单的示例演示算法的关键步骤，省略了许多更微妙的情况。¹²

5.1.整数线性运算

考虑以下综合问题:

在哪里年代是参数，a, b, d是未知变量。重写的不平等d0到(dld1)将公式转化为DNF。在续集中，我们将阐述一种间断的合成:

线性方程的变量变换我们首先考虑整数方程A + b = s．把它改写成A = s b和消除一个,我们获得s b作为证人一个简化后剩下的约束条件是3b5d = s某人0b0d1.然后我们处理这个方程3b - 5d = s，我们不能直接表示其中一个未知数。我们用欧几里得算法来计算gcd(3,5) = 1。在这个过程中，我们找到了3的一个解b5d= 1,说b= 2,d= 1。将最后一个条件乘以年代我们得到b = 2S d = S作为3的解b5d = s．然后是参数形式的通解b= 2年代+ 5,d＝年代+ 3，其中表示任意整数参数。因此，我们计算出了一个变量变换(第4.5.4节)，它映射到(b, d)，并保留解集。由此产生的变换合成问题只包含未知量，没有更多的方程:

这两个方程没有产生前提条件年代．要了解为什么可以产生一个先决条件，考虑一个不同的约束，6b10d＝年代．计算gcd(6,10) = 2得到一个先决条件& gt;年代是偶数和价值吗b= 2,d= 1，生成这个gcd，具有一般参数解b= 2年代+ 10,d = s+ 6。

更一般的,让米＝为线性方程的合取式，其中只有参数，没有变量。我们可以把处理等式的第一部分看作是寻找一个幺模变换矩阵U这样H = m·u是Hermite范式米．²然后我们用变量变换＝（) =U将约束条件简化为H＝问［: =U］．请注意,H＝是不是三角形矩阵比三角形矩阵更容易解米．解它产生可除性前提在．

解决不等式:考虑我们例子中处理等式的结果(5)。它的价值还有待综合。我们可以把约束条件写成一个上界和两个下界的结合，5s 2s 5 1s 3。考虑到这是一个整数，我们得到

在|x|表示x四舍五入到+和|x|表示x圆形的。作为见证值，我们可以选择，例如，上界，我们完成了第一个间断的综合。合成代码为

通常在量词消去的前提下精准医疗₁下界小于等于上界，也就是，．回想一下，在本节的开始我们有两个分离，由(d1d1)第二间断的合成，包含d1,类似地收益。在这种情况下，前提条件精准医疗₂是．然后，整个生成的代码使用if-else语句，如4.5.3节所示。^一个

虽然我们的例子的综合到这里就结束了，但所有其他类似于量词消去的情况，都可以在一般算法中出现。为了看这个，假设年代不是一个输入变量，但也需要合成。综合问题将继续．然后我们需要代表精准医疗₁在线性算术中通过消除除法和舍入。我们这样做是通过案例分析来提醒的年代求除数的最小公倍数的模，即15。对于这种情况，生成的代码包含从0到14的循环，在这种情况下可以展开并简化为年代= 4作为一个保证有效的解决方案。

使用程序专门化的思想，我们还支持将乘法系数作为参数而不是常数。然后，我们发出(而不是静态执行)代码，对符号系数的符号进行案例分析，并适当地计算最小公倍数和最大公约数。请注意，该扩展表示与单独使用见证术语作为生成的代码不同，因为它将专门的量词消除过程本身的步骤合并到合成代码中。

5.2.具有基数约束的集合

作为对数据结构进行可预测综合计算的一个步骤，我们将说明如何使用整数的综合过程来对有限对象集进行综合计算。为了表达集合上的约束，我们使用布尔代数和Presburger算术(BAPA)。这是整数线性算术支持集的一个严格扩展，，， \以及计算集合大小的基数运算符|·|。一种(无量词)BAPA决策过程通过将对集合变量的约束减少为对维恩区域大小的约束，维恩区域可以用纯线性整数算法表示。¹³baba的一个综合过程的基础是，这些约束的一个解可以解除为集上原始问题的解。例如，考虑分割一个集合的综合问题年代分成所需大小的分区:

我们从标记集合的维恩区域的大小开始A、B,年代通过变量k_我，如下图所示:

我们使用这些新变量重写我们的合成问题:

我们另外需要k_我0为所有我．当变量为0时，我们应用一点规则。如果我们计算年代作为|年代|，然后标识变量一个与k₅而且b与k₆，这个问题归结为5.1节的例子。因此，整数的合成产生生成代码的第一部分，用于计算k₅而且k₆．

我们如何从的解重构出集合变量的解，这还有待说明k₅而且k₆(在第4.5.4节的术语中，我们需要确定)．为此，我们依赖于任何可计算函数pickFrom(我,不)计算大小的子集我一组T(例如,pickFrom (我,不)可以挑最上面的我元素按某种顺序排列¹⁴)．我们重建一个而且B如下:

通过构造，保证选择子集的集合具有足够的大小。

5.3.实现

我们将合成过程实现为Scala编译器扩展，称为Comfusy(完整的功能性合成)。我们使用现成的决策程序^3.处理编译时检查。我们还可以将合成过程用于编译时检查，因为对所有自由变量的合成包含了可满足性检查。

我们的扩展支持通过线性算术谓词(包括参数化线性算术中的谓词)约束的选择函数合成整数值，也支持集合逻辑中带有基数约束的谓词约束的集合值合成。此外，它还可以为整数的模式匹配表达式的子集合成代码，如第2节中介绍的那些。我们的系统及其使用示例可以从网站上公开获得http://lara.epfl.ch．

回到顶部

6.结论

我们提出了将决策过程转化为综合过程的一般思想。我们已经探讨了如何对承认量词消去的理论进行这种转换，特别是线性算术。我们还说明了，即使在潜在的参数化可满足性问题不可判定的情况下(如整数乘法)，只要在参数固定时问题变为可判定的，也可以建立综合过程。我们还将一个BAPA决策程序转换为一个综合程序，在该过程中说明了如何将多个综合程序层层叠放。

结合基于附加可决定约束的综合过程，可以进一步支持所提出方法的有效性。例如，可以使用我们最近确定的有序集合的决策过程来提供对集合所需解决方案的更多控制。¹⁴在对一个集合进行分区的例子中，这种支持将允许我们指定一个分区的所有元素都小于第二个分区的所有元素。除了集合之外，我们希望我们的方法同样适用于多重集合。¹⁸另一个相关的类是代数数据类型的可决定约束。^17，23

量词消除决策过程直接支持参数化问题，因此它们是我们方法特别方便的起点。其他决策程序也适用，但可能需要更多的设计和实现工作，才能变成有趣的综合程序。特别是，另一种自动机理论的方法来综合整数算法与位向量随后被发展⁹；这种方法倾向于生成更大但更有效的代码。

我们已经指出，综合可以看作是一种强大的编程语言扩展。这样的扩展可以作为一种新的表达式和新的模式匹配结构无缝地引入流行的编程语言。我们希望，合成构造的可用性将改变我们思考程序开发的方式。程序属性和断言可以不再是可怕的“注释开销”的一部分，而是成为构建具有所需功能的程序的一种经济有效的方法。

回到顶部

回到顶部

回到顶部

数字图书馆是由计算机协会出版的。版权所有©2012 ACM股份有限公司

---

没有发现记录