SHF: Small: Behavioral Software Contract Verification

对于许多关键的软件组件来说，正确和可靠是很重要的，但是验证软件满足这些要求是困难的、昂贵的，而且容易出错。一种方法是使用软件合同作为指定和监控软件组件的义务和保证的手段。当在程序运行期间未满足此类合同的协议时，程序停止并发出违反的信号，并指示故障部件。软件合同对于高保证软件非常重要，因为它们识别有故障的程序组件，但它们不能保证组件不会失败。这一研究项目的目标是调查能够证明没有合同故障的提前软件验证的方法，从而对关键软件组件的正确性和可靠性给予高度信任。这项研究将有助于对程序验证、软件合同和现代编程语言之间的相互作用有一个新的理解。此外，它还将导致开发工具，以核实软件组件是否有合同。预计通过提前验证软件合同，可以消除在程序运行期间监控合同协议的开销，这将鼓励程序员比目前更广泛地使用合同。这些工具可以极大地降低开发高保证软件的难度和成本。要实现该项目的目标，必须克服两个最重要的技术障碍：(1)合同的可表现性，尽管对于构建可靠的组件至关重要，但阻碍了对程序的静态推理，并产生了巨大的运行时监控成本；(2)高阶编程语言的可表现性，现代工业软件构造的支柱，阻碍了关于合同的静态推理，尽管有成熟的自动化工具和技术可用。这个研究项目纠正了这种情况，为高级语言中关于行为契约的模块化和组合式自动推理提供了基础。具体地说，该项目将提供：(1)通过合同推理组件的语义方面的基础理论，这使得基于组件的自动合同验证成为可能；(2)用于探索、测试和改进程序和合同的交互式合同验证环境；以及(3)在包含合同的广泛使用的球拍编程语言实现和标准库的背景下对我们的方法和工具的评估。

It is important for many critical software components to be correct and reliable, however verifying that software meets such requirements is difficult, expensive, and error-prone. One approach is to use software contracts as a means to specify and monitor the obligations and guarantees of software components. When the agreements of such contracts are not met during the operation of a program, the program stops and signals a violation and indicates the faulty component. Software contracts have been very important for high-assurance software, since they identify faulty program components, but they offer no guarantees that a component will not fail. The goal of this research project is to investigate approaches to ahead-of-time software verification that can prove the absence of contract failures, thus giving a high level of confidence in the correctness and reliability of critical software components. The research will contribute a new understanding of the interplay between program verification, software contracts, and modern programming languages. Additionally, it will result in the development of tools for verifying software components with contracts. It is expected that by verifying software contracts ahead-of-time, the overhead of monitoring contract agreements during program operation can be eliminated, which will encourage programmers to use contracts far more extensively than they currently do. Such tools can dramatically reduce the difficulty and cost of developing high-assurance software.There are two paramount technical obstacles that must be overcome to achieve the goals of this project: (1) the expressivity of contracts, while crucial for the construction of reliable components, thwarts static reasoning about programs and incurs significant run-time monitoring costs, (2) the expressivity of higher-order programming languages, a mainstay of modern industrial software construction, thwarts static reasoning about contracts, despite the availability of mature automated tools and techniques. This research project rectifies the situation by providing foundations for modular and compositional automated reasoning about behavioral contracts in a higher-order language. Specifically, the project will provide: (1) a foundational theory in terms of a semantics for reasoning about components via their contracts, which enables automated component-based contract verification; (2) an interactive contract verification environment for exploring, testing, and refining programs and contracts; and (3) an evaluation of our approach and tools in the context of the Racket programming language implementation and standard library, which contains extensive use of contracts.