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.