SoD-TEAM: Programming by Sketching

SoD-TEAM：通过草图进行编程

• 批准号: 0613997
• 负责人: Rastislav Bodik
• 金额: $ 20万
• 依托单位: University of California-Berkeley
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2006
• 资助国家: 美国
• 起止时间: 2006-10-01 至 2009-09-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0613997&HistoricalAwards=false
• 关键词: SoD; TEAM; Programming; Sketching

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.

0613997 Rastislav BodikU of Cal -Berkeley TITLE Programming by SketchingSoftware是以分层的方式设计和实现的：需求被细化到设计中，然后用低级代码实现。实现间隙是层之间缺乏正式正确性连接的原因：功能通常没有正式指定，实现是手工产生的，而不是生成的。该项目建议通过使编写规范和实现低级代码更容易来弥合实现差距。 为了使具有挑战性的问题易于管理，该项目侧重于科学计算领域。 主要的技术方法是草图，这是一种新的软件综合方法，程序员开发部分实现-草图-和所需功能的单独规范。 然后合成器完成草图，使其表现得像指定的那样。 这个探索性项目将（a）研究如何将基于SAT的合成器的适用性扩展到越来越大的程序; B）开发用于合成目前超出SAT合成器能力的程序的技术;以及（c）为一类科学程序开发一个强大的草图合成器。