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.