CAREER: Lightweight, Blame-aware Contract Checking

职业：轻量级、具有责备意识的合同检查

• 批准号: 0846012
• 负责人: Robert Findler
• 金额: $ 42.97万
• 依托单位: Northwestern University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2009
• 资助国家: 美国
• 起止时间: 2009-06-01 至 2014-05-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0846012&HistoricalAwards=false
• 关键词: CAREER; Lightweight; Blame; aware; Contract

This award is funded under the American Recovery and Reinvestment Act of 2009(Public Law 111-5).As computers become more powerful, the limiting factor for building software systems is shifting away from the underlying computer's performance limitations to the software's inherent complexity. One way to cope with this complexity is to use software contracts to separate a large system into smaller chunks, thereby enabling programmers to focus their energy on just one small part of the system at a time. A key feature of this separation is the ability to assign blame; that is, when the software system fails, a contract checker can use the contracts to identify a single sub-system as faulty, automatically narrowing the search for the underlying cause of the failure to that one subsystem or possibly its contract; of course, fixing a bug in a contract may yet expose latent bugs in other subsystems but in each case the contract system will help the programmer identify the failure. Even better, software contracts are typically written in a language that is very close to the programming language, meaning that programmers only have to invest a little bit of their time and resources in order to start seeing the benefits of contracts.This work promises to improve the state of the art in contract checking. Specifically, the PI will study the interaction between statically and dynamically verified portions of systems, in a manner similar to hybrid and gradual types. Building on this integration, the PI will also study how to integrate theorem provers into software systems in a way that the theorem prover's scope can be limited to just the most mission-critical parts of the system. The PI will also study how to add contracts to more sophisticated modularity mechanisms like traits and the ML module system, and explore how contracts can help generalize existing techniques for automatic test case and test oracle generation to support higher-order functions and unknown classes. All the while, the PI will ensure that these new techniques are practically viable by using them in a 500,000 line software system that the he maintains, as well as conducting detailed studies of how contracts are used in other settings, including JML and Eiffel.

该奖项是根据2009年美国复苏和再投资法案（公法111-5）资助的。随着计算机变得越来越强大，构建软件系统的限制因素正在从底层计算机的性能限制转向软件的内在复杂性。处理这种复杂性的一种方法是使用软件契约将大系统分成更小的块，从而使程序员一次只将精力集中在系统的一小部分上。这种分离的一个关键特征是推卸责任的能力；也就是说，当软件系统出现故障时，合同检查器可以使用合同来识别单个子系统有故障，自动将搜索故障的潜在原因缩小到该子系统或可能的其合同；当然，修复合约中的错误可能会暴露其他子系统中的潜在错误，但在每种情况下，合约系统都将帮助程序员识别故障。更好的是，软件契约通常是用一种非常接近编程语言的语言编写的，这意味着程序员只需要投入一点时间和资源，就可以开始看到契约的好处。这项工作有望提高合同审核的技术水平。具体地说，PI将以类似于混合和渐进类型的方式研究系统的静态和动态验证部分之间的相互作用。在此集成的基础上，PI还将研究如何将定理证明者集成到软件系统中，使定理证明者的范围仅限于系统中最关键的部分。PI还将研究如何将契约添加到更复杂的模块化机制中，如特征和ML模块系统，并探索契约如何帮助推广现有的自动测试用例和测试oracle生成技术，以支持高阶函数和未知类。与此同时，PI将确保这些新技术在他维护的50万行软件系统中实际可行，并对合同如何在其他环境中使用进行详细研究，包括JML和Eiffel。