Software synthesis procedures
Software synthesis procedures
复制标题
软件综合程序
DOI：
--
复制
发表时间：
2012
影响因子：
22.7
通讯作者：
Philippe Suter
中科院分区：
文献类型：
--
作者：
Viktor Kunčak;M. Mayer;R. Piskac;Philippe Suter
从规范中自动合成程序片段可以使程序更容易编写，也更容易推理。为了将合成集成到编程语言中，软件合成算法应该以一种可预测的方式运行：它们应该成功地实现定义良好的规范类。我们建议将决策过程系统地推广到综合过程中，并使用它们来编译嵌入函数式和命令式程序中的隐式指定计算。合成过程是可预测的，因为只要存在这样的代码，它们就能保证找到满足规范的代码。为了说明我们的方法，我们通过扩展整数算术和集合数据结构的量词消除算法来推导综合过程。然后，我们展示了这种综合过程的实现可以扩展编译器以支持隐式值定义和高级模式匹配。
Automated synthesis of program fragments from specifications can make programs easier to write and easier to reason about. To integrate synthesis into programming languages, software synthesis algorithms should behave in a predictable way: they should succeed for a well-defined class of specifications. We propose to systematically generalize decision procedures into synthesis procedures, and use them to compile implicitly specified computations embedded inside functional and imperative programs. Synthesis procedures are predictable, because they are guaranteed to find code that satisfies the specification whenever such code exists. To illustrate our method, we derive synthesis procedures by extending quantifier elimination algorithms for integer arithmetic and set data structures. We then show that an implementation of such synthesis procedures can extend a compiler to support implicit value definitions and advanced pattern matching.