CAREER: Lightweight, Blame-aware Contract Checking

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

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.