SHF: Small: Collaborative Research: Specification Language Foundations for Modular Reasoning Methodologies

该项目扩展了面向对象（OO）语言的语义基础，以涵盖模块化推理的方法。模块化推理意味着假设每个使用的组件的规格来验证软件组件。模块化对于生产力和可伸缩性很重要，但是对于OO软件来说很难实现。为了支持模块化推理，研究人员提出了几种方法来限制程序及其规范。这个项目的目标是提供一个理论基础，以支持证明和使用方法论的实用技术。这个项目为编程和规范语言、验证逻辑和相关工具的设计者提供了指导。结果将提高验证工具的实用性和可扩展性——这是验证软件大挑战的一个关键目标。软件开发人员可以从最佳实践方法的集成和和谐互操作中获益。该项目具有潜在的变革性：它旨在支持工具用户对方法的组合和定制，并可扩展到实际应用程序中。改进的OO编程方法可以极大地改进编程实践，特别是在需要高保证、可靠性和安全性的应用程序中。这将使社会受益，因为社会越来越依赖于使用OO组件构建的计算系统。方法的统一和工具的简化也促进了软件开发人员的教育。

This project extends the semantical foundations of object-oriented (OO) languages to cover methodologies for modular reasoning. Modular reasoning means verifying software components assuming the specification of each used component. Modularity is important for productivity and scalability, but is difficult to achieve for OO software. To support modular reasoning, researchers have proposed several methodologies that restrict programs and their specifications. The goal of this project is to provide a theoretical basis that supports practical techniques for justifying and using methodologies.This project provides guidance for the designers of programming and specification languages, verification logics, and associated tools. The results will improve the utility and extensibility of verification tools --- a key goal of the Verified Software grand challenge. Software developers may benefit from the integration and harmonious interoperation of best-practice methodologies. This project is potentially transformative: it aims to enable combinations and customizations of methodologies by tool users, scalable to real applications.Improved OO programming methodologies may greatly improve programming practice, especially in applications needing high assurance, reliability, and security. This will benefit society, which increasingly depends on computing systems built using OO components. Unification of methodologies and streamlining of tools also facilitates the education of software developers.