SHF: Small: Programming Abstractions for Algorithmic Software Synthesis

该奖项是根据2009年美国复苏和再投资法案（公法111-5）资助的。与软件验证相反，软件合成“编写”程序，而不仅仅是检查它们的错误。 虽然验证最近已经到达程序员手中，但合成的成功仍然掌握在经过正式培训的专家手中。 为了简化综合的采用，这个建议开发了算法综合，这是演绎综合，模型检查是演绎验证：而不是用定理证明器推导程序，算法综合系统地在候选实现的空间中找到程序。剩下的一个关键挑战是如何描述这个候选空间。 每个合成器都必须“编程”，了解该领域及其实现技巧。 在演绎综合中，这种洞察力是由领域理论传达的。 在算法合成中，程序员通常通过编写语法定义候选空间的部分程序来传达他们的见解。 然后由合成器完成部分程序。 由于程序是部分指定的，程序员可以控制候选空间的大小，使算法合成可行，同时将繁琐的程序细节留给合成器。该项目研究算法合成的语言学方面，解决三个问题：（1）如何调试部分程序？ 天使非确定性的预言将用于逐步发展的部分程序。 (2)什么是领域洞察力以及如何传达它？ 编程抽象将被开发用于自然地定义候选空间。(3)如何以帮助合成器可扩展性为目标来细化洞察力？ 程序员和合成器之间的交互式对话将帮助程序员提炼和形式化她的洞察力。

This award is funded under the American Recovery and Reinvestment Act of 2009 (Public Law 111-5).In contrast to software verification, software synthesis "writes" programs rather than merely checks them for errors. While verification has recently reached the programmer, the success of synthesis remains in the hands of formally trained experts. To ease the adoption of synthesis, this proposal develops algorithmic synthesis, which is to deductive synthesis what model checking is to deductive verification: Rather than deducing a program with a theorem prover, algorithmic synthesis systematically finds the program in a space of candidate implementations. A key remaining challenge is how to describe this candidate space. Each synthesizer must be "programmed" with insights about the domain and its implementation tricks. In deductive synthesis, the insight is conveyed by a domain theory. In algorithmic synthesis, programmers typically communicate their insight by writing a partial program that syntactically defines the candidate space. The partial program is then completed by the synthesizer. Since the program is specified partially, programmers can control the candidate space size, making algorithmic synthesis feasible while leaving tedious program details to the synthesizer. This project investigates linguistic aspects of algorithmic synthesis, addressing three issues: (1) How to debug partial programs? Angelically non-deterministic oracles will be used for gradual development of partial programs. (2) What is domain insight and how to communicate it? Programming abstractions will be developed for defining the candidate space naturally. (3) How to refine the insight with the goal of aiding the synthesizer scalability? An interactive dialogue between the programmer and the synthesizer will help the programmer refine and formalize her insight.