ACM通信
技术视角:从什么到如何编译
如果程序员幸运的话，她的程序不需要编码:她指定所需的属性，然后现有的算法计算满足她的属性的结果。示例包括查找带有正则表达式的字符串，求解线性方程组，以及确定布尔公式是否可满足。这样的声明性编程重用我们可能称为求解器的算法。只要我们的问题可以表述为求解者所理解的性质，我们就可以自由地说什么不用说应该算吗如何来计算它。
当然，并不是所有的问题都适合声明性编程。对于某些问题，编写程序可能比编写规范更快、更自然。像文档编辑器这样的大型程序永远不会被完全指定。还有一些无法确定的属性是无法构建求解器的。
考虑到这些限制，我们是否应该考虑声明式编程?Viktor Kuncak等人的以下论文将声明式编程集成到一种通用语言中，允许人们在可以声明式解决子问题时避开宿主语言。
它们的第一个贡献是使Scala宿主语言更强大的语言构造，而不会使声明性属性显得突兀。例如，他们的情况下语句几乎隐藏了在运行时解决约束的事实:此代码决定是否我是偶数还是奇数通过确定方程是否存在解2 * j =我而且2 * j + 1 =我，但代码与标准模式匹配非常相似:
在声明式编程中，很容易编写出有bug的属性，即允许太多或不允许令人满意的结果的属性。作为第二篇文章，本文开发了对这两种错误的调试支持。当规范约束不足时，存在允许多个合法结果的输入。为了帮助确定这种自由是否构成了不需要的非确定性，编译器会寻找这样的输入。如果它存在，编译器计算两个不同的结果，这可能提示属性中缺少什么约束。当规范被过度约束时，就会出现不允许任何合法结果的输入。编译器计算这类输入的集合，并用谓词符号地描述该集合。这两个警告都是在程序执行之前传递给程序员的，从而减少了测试的需要。
第三个贡献是将规范编译为高效的求解器代码。对于给定的问题，通用求解器的效率低于手写程序，至少有两个原因:求解器在探索求解空间时可能需要回溯;它们展示了读取属性和维护解决方案的解释开销。为了减少这种开销，作者描述了一种在编译时“预先求解”规范的方法。编译器分析属性并输出代码，这些代码所做的仅仅是基本上不能移动到编译时的内容——仅在运行时可用的值的传播。
为了能够编译规范，作者观察到约束求解器通常基于量词消去，它通过每次消去一个变量，然后反向计算它们的值来求解约束系统，就像基于变量消去的线性方程求解器一样。编译器方法因此要求量词消去也产生一个见证函数，该函数从剩下的变量中计算被消去的变量;然后通过连接见证函数来构造高效求解器。
本文最后鼓励将声明式编程扩展到线性算术约束之外。作者表明，他们也可以使用基数约束声明式地计算集合。他们的方法是一般化的，应该有助于为任何带有量词消除决策过程的约束语言创建编译器。由软件验证所驱动的求解器的最新进展，因此可以转化为更具表达性的声明式编程。
几千年前，随着巴比伦人求解方程的算法，计算机就以声明的方式诞生了2和中国的高斯方法的前身。这些算法允许我们通过思考计算什么来解决问题，将我们从如何操作中解放出来。后来开发了更多的求解器;事实上，20世纪最好的10个算法中有6个，其中包括Simplex，都是求解器。1这些算法可以看作是方便的图灵不完全编程语言的高效解释器。我预测，当我们识别更多这样的受限语言并将它们集成到通用(图灵完备)语言中时，我们将使编程更高效，程序更可靠。
©2012 acm 0001-0782/12/02 $10.00
允许为个人或课堂使用部分或全部作品制作数字或硬拷贝，但不得为盈利或商业利益而复制或分发，且副本在首页上附有本通知和完整的引用。除ACM外，本作品的其他组件的版权必须受到尊重。允许有信用的文摘。以其他方式复制、重新发布、在服务器上发布或重新分发到列表，都需要事先获得特定的许可和/或费用。请求发布的权限permissions@acm.org传真(212)869-0481。
数字图书馆是由计算机协会出版的。版权所有©2012 ACM, Inc.