SoD-TEAM: Programming by Sketching

SketchingSoftware的编程是以分层的方式设计和实现的：需求被提炼成设计，设计又被低级代码实现。实现差距是导致层之间缺乏正式的正确性连接的原因：功能通常没有正式指定，实现是手工生成的，而不是生成的。该项目建议通过简化编写规范和实现底层代码来弥合实现差距。为了使具有挑战性的问题易于管理，该项目将重点放在科学计算领域。主要的技术方法是草图，这是一种新的软件综合方法，程序员开发部分实现（草图）和所需功能的单独规范。然后合成器完成草图，使其表现得像规范一样。这个探索性项目将(a)研究如何将基于sat的合成器的适用性扩展到越来越大的程序；b)开发目前超出SAT合成器能力的合成程序的技术；(c)为一类科学项目开发了一个健壮的素描合成器。

0613997Rastislav BodikU of Cal - BerkeleyTITLE Programming by SketchingSoftware is designed and implemented in a layered way: requirements are refined into designs, which are in turn implemented with low-level code.The implementation gap is responsible for the lack of a formal correctness connection between the layers: functionality is typically not formally specified and implementations are produced by hand rather than generated. This project proposes to bridge the implementation gap by making it easier both to write specifications and to implement the low-level code. To make the challenging problem manageable, the project focuses on the domain of scientific computing. The chief technical approach is sketching, a new software synthesis approach where the programmer develops a partial implementation --- a sketch --- and a separate specification of the desired functionality. The synthesizer then completes the sketch to behave like thespecification. This exploratory project will (a) investigate how to extend the applicability of a SAT-based synthesizer to increasingly larger programs; b) develop techniques for synthesizing programs that are currently beyond the power of the SAT synthesizer; and (c) develop a robust sketching synthesizer for a class of scientific programs.